linearEqSolver 1.3 → 2.0

raw patch · 8 files changed

+85/−67 lines, 8 filesdep ~basedep ~sbvsetup-changed

Dependency ranges changed: base, sbv

Files

• CHANGES.md +33/−0
• COPYRIGHT +1/−1
• LICENSE +1/−1
• Math/LinearEquationSolver.hs +24/−23
• README +4/−6
• RELEASENOTES +0/−30
• Setup.hs +16/−0
• linearEqSolver.cabal +6/−6

@@ -0,0 +1,33 @@+* Hackage: <http://hackage.haskell.org/package/linearEqSolver>+* GitHub:  <http://github.com/LeventErkok/linearEqSolver>++* Latest Hackage released version: 2.0++### Version 2.0, 2017-10-25++  * Use defaultSMTConfig exported from SBV+  * All-solution variants now take the max-number of solutions requested,+    following the corresponding changes in SBV itself. Thanks to Mitchell Rosen+    for reporting.++### Version 1.3, 2014-08-27++  * Use the Solver type from SBV directly for picking the solver,+    avoiding bit-rot.+  * Adjust SBV dependency to >= 3.1, to get proper access to+    Solver type++### Version 1.2, 2013-01-02++  * Allow both CVC4 and Z3 to be used as the SMT solver.+  * Adjust SBV dependency to >= 2.9, to get access to CVC4.++### Version 1.1, 2012-10-22++  * Add solvers over rationals, in addition to just integers.+  * Adjust SBV dependency to >= 2.7 as we depend on the new Real+    instance for the AlgReal type.++### Version 1.0, 2012-10-18++  * Initial release, contains solver for integer linear equations.

@@ -1,4 +1,4 @@-Copyright (c) 2012-2013, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2012-2017, Levent Erkok (erkokl@gmail.com) All rights reserved.  The linearEqSolver library is distributed with the BSD3 license. See the LICENSE file

@@ -1,6 +1,6 @@ linearEqSolver: Solves linear systems of equations, using SMT solving. -Copyright (c) 2012-2013, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2012-2017, Levent Erkok (erkokl@gmail.com) All rights reserved.  Redistribution and use in source and binary forms, with or without

@@ -58,17 +58,18 @@                       -> [[Integer]]           -- ^ Coefficient matrix (A)                       -> [Integer]             -- ^ Result vector (b)                       -> IO (Maybe [Integer])  -- ^ A solution to @Ax = b@, if any-solveIntegerLinearEqs cfg coeffs res = extractModel `fmap` satWith (getSolver cfg) cs+solveIntegerLinearEqs cfg coeffs res = extractModel `fmap` satWith (defaultSolverConfig cfg) cs   where cs = buildConstraints "solveIntegerLinearEqs" coeffs res --- | Similar to `solveIntegerLinearEqs`, except returns all possible solutions.--- Note that there might be an infinite number of solutions if the system--- is underspecified, in which case the result will be a lazy list of solutions--- that the caller can consume as much as needed.+-- | Similar to `solveIntegerLinearEqs`, except in case the system has an infinite+-- number of solutions, then it will return the number of solutions requested. (Note+-- that if the system is underspecified, then there are an infinite number of+-- solutions.) So, the result can be empty, a singleton, or precisely the number requested, last of+-- which indicates there are an infinite number of solutions. -- -- Here's an example call, where we underspecify the system and hence there are--- multiple (in this case an infinite number of) solutions. Here, we only take the first 3 elements,--- for testing purposes, but all such results can be computed lazily. Our system is:+-- multiple (in this case an infinite number of) solutions. Here, we ask for the first+-- 3 elements for testing purposes. -- -- @ --     2x + 3y + 4z = 20@@ -77,14 +78,18 @@ -- -- We have: ----- >>> take 3 `fmap` solveIntegerLinearEqsAll Z3 [[2, 3, 4],[6, -3, 9]] [20, -6]--- [[5,6,-2],[-8,4,6],[18,8,-10]]+-- >>> solveIntegerLinearEqsAll Z3 3 [[2, 3, 4],[6, -3, 9]] [20, -6]+-- [[-8,4,6],[-21,2,14],[-34,0,22]]+--+-- The solutions you get might differ, depending on what the solver returns. (Though they'll be correct!) solveIntegerLinearEqsAll :: Solver          -- ^ SMT Solver to use+                          -> Int                -- ^ Maximum number of solutions to return, in case infinite                          -> [[Integer]]     -- ^ Coefficient matrix (A)                          -> [Integer]       -- ^ Result vector (b)                          -> IO [[Integer]]  -- ^ All solutions to @Ax = b@-solveIntegerLinearEqsAll cfg coeffs res = extractModels `fmap` allSatWith (getSolver cfg) cs+solveIntegerLinearEqsAll s maxNo coeffs res = extractModels `fmap` allSatWith cfg cs   where cs = buildConstraints "solveIntegerLinearEqsAll" coeffs res+        cfg = (defaultSolverConfig s) {allSatMaxModelCount = Just maxNo}  -- | Solve a system of linear equations over rationals. Same as the integer -- version `solveIntegerLinearEqs`, except it takes rational coefficients@@ -103,13 +108,13 @@                        -> [[Rational]]            -- ^ Coefficient matrix (A)                        -> [Rational]              -- ^ Result vector (b)                        -> IO (Maybe [Rational])   -- ^ A solution to @Ax = b@, if any-solveRationalLinearEqs cfg coeffs res = (fmap from . extractModel) `fmap` satWith (getSolver cfg) cs+solveRationalLinearEqs cfg coeffs res = (fmap from . extractModel) `fmap` satWith (defaultSolverConfig cfg) cs   where to   = map (fromRational :: Rational -> AlgReal)         from = map (toRational   :: AlgReal -> Rational)         cs   = buildConstraints "solveRationalLinearEqs" (map to coeffs) (to res)  -- | Solve a system of linear equations over rationals.  Similar to `solveRationalLinearEqs`,--- except it returns all solutions lazily.+-- except if the system is underspecified, then returns the number of solutions requested. -- -- Example system: --@@ -119,16 +124,20 @@ -- -- In this case, the system has infinitely many solutions. We can compute three of them as follows: ----- >>> take 3 `fmap` solveRationalLinearEqsAll Z3 [[2.4, 3.6]] [12]--- [[0 % 1,10 % 3],[(-3) % 2,13 % 3],[(-3) % 4,23 % 6]]+-- >>> solveRationalLinearEqsAll Z3 3 [[2.4, 3.6]] [12]+-- [[5 % 1,0 % 1],[13 % 2,(-1) % 1],[8 % 1,(-2) % 1]]+--+-- The solutions you get might differ, depending on what the solver returns. (Though they'll be correct!) solveRationalLinearEqsAll :: Solver             -- ^ SMT Solver to use+                          -> Int                -- ^ Maximum number of solutions to return, in case infinite                           -> [[Rational]]       -- ^ Coefficient matrix (A)                           -> [Rational]         -- ^ Result vector (b)                           -> IO [[Rational]]    -- ^ All solutions to @Ax = b@-solveRationalLinearEqsAll cfg coeffs res = (map from . extractModels) `fmap` allSatWith (getSolver cfg) cs+solveRationalLinearEqsAll s maxNo coeffs res = (map from . extractModels) `fmap` allSatWith cfg cs   where to   = map (fromRational :: Rational -> AlgReal)         from = map (toRational   :: AlgReal -> Rational)         cs   = buildConstraints "solveRationalLinearEqsAll" (map to coeffs) (to res)+        cfg  = (defaultSolverConfig s) {allSatMaxModelCount = Just maxNo}  -- | Build the constraints as given by the coefficient matrix and the resulting vector buildConstraints :: (Num a, SymWord a) => String -> [[a]] -> [a] -> Symbolic SBool@@ -141,14 +150,6 @@        solve $ zipWith rowEq (map (map literal) coeffs) (map literal res)  where m    = length coeffs        n:ns = map length coeffs---- | Determine the solver config.-getSolver :: Solver -> SMTConfig-getSolver Z3        = z3-getSolver Yices     = yices-getSolver Boolector = boolector-getSolver CVC4      = cvc4-getSolver MathSAT   = mathSAT  {- $solverInfo Note that while we allow all SMT-solvers supported by SBV to be used, not all will work. In particular,

@@ -1,13 +1,11 @@-linearEqSolver-==============+## linearEqSolver  Solve systems of linear equations, using SMT solvers. Both integer only solutions and solutions-over rationals are supported. Either single solutions, or (a lazy list of) all solutions can-be computed.+over rationals are supported. Either single solutions, or all solutions can be computed.  The hackage site http://hackage.haskell.org/package/linearEqSolver is the best place for details on the API and the example use cases. -Build Status-============+### Build Status+ We use Travis-CI's automated build infrastructure, making a build for each commit. Current build status: [![Build Status](https://secure.travis-ci.org/LeventErkok/linearEqSolver.png?branch=master)](http://travis-ci.org/LeventErkok/linearEqSolver)

@@ -1,30 +0,0 @@-Hackage: <http://hackage.haskell.org/package/linearEqSolver>-GitHub:  <http://github.com/LeventErkok/linearEqSolver>--Latest Hackage released version: 1.3--======================================================================-Version 1.3, 2014-08-27--  - Use the Solver type from SBV directly for picking the solver,-    avoiding bit-rot.-  - Adjust SBV dependency to >= 3.1, to get proper access to-    Solver type--======================================================================-Version 1.2, 2013-01-02--  - Allow both CVC4 and Z3 to be used as the SMT solver.-  - Adjust SBV dependency to >= 2.9, to get access to CVC4.--======================================================================-Version 1.1, 2012-10-22--  - Add solvers over rationals, in addition to just integers.-  - Adjust SBV dependency to >= 2.7 as we depend on the new Real-    instance for the AlgReal type.--======================================================================-Version 1.0, 2012-10-18--  - Initial release, contains solver for integer linear equations.

@@ -1,2 +1,18 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Main+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- Setup module for the linearEqSolver library+-----------------------------------------------------------------------------++{-# OPTIONS_GHC -Wall #-}+module Main(main) where+ import Distribution.Simple++main :: IO () main = defaultMain

@@ -1,5 +1,5 @@ Name:          linearEqSolver-Version:       1.3+Version:       2.0 Category:      Math, SMT Synopsis:      Use SMT solvers to solve linear systems over integers and rationals Description:   Solve linear systems of equations over integers and rationals, using an SMT solver.@@ -8,9 +8,9 @@                bug reports, and patches are always welcome.                .                .-               Release notes can be seen at: <http://github.com/LeventErkok/linearEqSolver/blob/master/RELEASENOTES>.+               Release notes can be seen at: <http://github.com/LeventErkok/linearEqSolver/blob/master/CHANGES.md> -Copyright:     Levent Erkok, 2012-2013+Copyright:     Levent Erkok, 2012-2017 License:       BSD3 License-file:  LICENSE Stability:     Experimental@@ -20,7 +20,7 @@ Maintainer:    Levent Erkok (erkokl@gmail.com) Build-Type:    Simple Cabal-Version: >= 1.14-Extra-Source-Files: INSTALL, README, COPYRIGHT, RELEASENOTES+Extra-Source-Files: INSTALL, README, COPYRIGHT, CHANGES.md  source-repository head     type:       git@@ -29,6 +29,6 @@ Library   default-language: Haskell2010   ghc-options     : -Wall-  Build-Depends   : base >= 4 && < 5-                  , sbv >= 3.1+  Build-Depends   : base >= 4.9 && < 5+                  , sbv >= 7.3   Exposed-modules : Math.LinearEquationSolver