linearEqSolver 1.2 → 1.3
raw patch · 3 files changed
+43/−39 lines, 3 filesdep ~sbv
Dependency ranges changed: sbv
Files
- Math/LinearEquationSolver.hs +32/−30
- RELEASENOTES +9/−1
- linearEqSolver.cabal +2/−8
Math/LinearEquationSolver.hs view
@@ -15,7 +15,8 @@ module Math.LinearEquationSolver ( -- * Available SMT solvers- z3, cvc4, Solver(..)+ -- $solverInfo+ Solver(..) -- * Solutions over Integers , solveIntegerLinearEqs , solveIntegerLinearEqsAll@@ -24,21 +25,7 @@ , solveRationalLinearEqsAll ) where -import Data.SBV hiding (z3, cvc4)-import qualified Data.SBV as SBV (z3, cvc4)---- | Interface to the SMT solver, via the SBV library. Unless you need to create--- custom solvers, or tweak the existing ones, you should not need to use this type: Simply--- use the values 'z3' and 'cvc4' to access the respective SMT solvers.-newtype Solver = Solver SMTConfig---- | The Z3 SMT solver from Microsoft: <http://z3.codeplex.com/>.-z3 :: Solver-z3 = Solver SBV.z3---- | The CVC4 SMT solver from New York University and the University of Iowa: <http://cvc4.cs.nyu.edu>.-cvc4 :: Solver-cvc4 = Solver SBV.cvc4+import Data.SBV -- | Solve a system of linear integer equations. The first argument is -- the matrix of coefficients, known as @A@, of size @mxn@. The second argument@@ -54,7 +41,7 @@ -- 2x + z = 8 -- @ ----- >>> solveIntegerLinearEqs z3 [[2, 3, 4],[6, -3, 9],[2, 0, 1]] [20, -6, 8]+-- >>> solveIntegerLinearEqs Z3 [[2, 3, 4],[6, -3, 9],[2, 0, 1]] [20, -6, 8] -- Just [5,6,-2] -- -- The first argument picks the SMT solver to use. Valid values are 'z3' and@@ -62,16 +49,16 @@ -- -- In case there are no solutions, we will get `Nothing`: ----- >>> solveIntegerLinearEqs z3 [[1], [1]] [2, 3]+-- >>> solveIntegerLinearEqs Z3 [[1], [1]] [2, 3] -- Nothing -- -- Note that there are no solutions to this second system as it stipulates the unknown is -- equal to both 2 and 3. (Overspecified.)-solveIntegerLinearEqs :: Solver -- ^ SMT Solver to use, pass one of 'z3' or 'cvc4'+solveIntegerLinearEqs :: Solver -- ^ SMT Solver to use -> [[Integer]] -- ^ Coefficient matrix (A) -> [Integer] -- ^ Result vector (b) -> IO (Maybe [Integer]) -- ^ A solution to @Ax = b@, if any-solveIntegerLinearEqs (Solver cfg) coeffs res = extractModel `fmap` satWith cfg cs+solveIntegerLinearEqs cfg coeffs res = extractModel `fmap` satWith (getSolver cfg) cs where cs = buildConstraints "solveIntegerLinearEqs" coeffs res -- | Similar to `solveIntegerLinearEqs`, except returns all possible solutions.@@ -90,13 +77,13 @@ -- -- We have: ----- >>> take 3 `fmap` solveIntegerLinearEqsAll z3 [[2, 3, 4],[6, -3, 9]] [20, -6]+-- >>> take 3 `fmap` solveIntegerLinearEqsAll Z3 [[2, 3, 4],[6, -3, 9]] [20, -6] -- [[5,6,-2],[-8,4,6],[18,8,-10]]-solveIntegerLinearEqsAll :: Solver -- ^ SMT Solver to use, pass one of 'z3' or 'cvc4'+solveIntegerLinearEqsAll :: Solver -- ^ SMT Solver to use -> [[Integer]] -- ^ Coefficient matrix (A) -> [Integer] -- ^ Result vector (b) -> IO [[Integer]] -- ^ All solutions to @Ax = b@-solveIntegerLinearEqsAll (Solver cfg) coeffs res = extractModels `fmap` allSatWith cfg cs+solveIntegerLinearEqsAll cfg coeffs res = extractModels `fmap` allSatWith (getSolver cfg) cs where cs = buildConstraints "solveIntegerLinearEqsAll" coeffs res -- | Solve a system of linear equations over rationals. Same as the integer@@ -110,13 +97,13 @@ -- 7.2x - 5y = -8.5 -- @ ----- >>> solveRationalLinearEqs z3 [[2.4, 3.6],[7.2, -5]] [12, -8.5]+-- >>> solveRationalLinearEqs Z3 [[2.4, 3.6],[7.2, -5]] [12, -8.5] -- Just [245 % 316,445 % 158]-solveRationalLinearEqs :: Solver -- ^ SMT Solver to use, pass one of 'z3' or 'cvc4'+solveRationalLinearEqs :: Solver -- ^ SMT Solver to use -> [[Rational]] -- ^ Coefficient matrix (A) -> [Rational] -- ^ Result vector (b) -> IO (Maybe [Rational]) -- ^ A solution to @Ax = b@, if any-solveRationalLinearEqs (Solver cfg) coeffs res = (fmap from . extractModel) `fmap` satWith cfg cs+solveRationalLinearEqs cfg coeffs res = (fmap from . extractModel) `fmap` satWith (getSolver cfg) cs where to = map (fromRational :: Rational -> AlgReal) from = map (toRational :: AlgReal -> Rational) cs = buildConstraints "solveRationalLinearEqs" (map to coeffs) (to res)@@ -132,13 +119,13 @@ -- -- 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]--- [[5 % 1,0 % 1],[0 % 1,10 % 3],[3 % 2,7 % 3]]-solveRationalLinearEqsAll :: Solver -- ^ SMT Solver to use, pass one of 'z3' or 'cvc4'+-- >>> take 3 `fmap` solveRationalLinearEqsAll Z3 [[2.4, 3.6]] [12]+-- [[0 % 1,10 % 3],[(-3) % 2,13 % 3],[(-3) % 4,23 % 6]]+solveRationalLinearEqsAll :: Solver -- ^ SMT Solver to use -> [[Rational]] -- ^ Coefficient matrix (A) -> [Rational] -- ^ Result vector (b) -> IO [[Rational]] -- ^ All solutions to @Ax = b@-solveRationalLinearEqsAll (Solver cfg) coeffs res = (map from . extractModels) `fmap` allSatWith cfg cs+solveRationalLinearEqsAll cfg coeffs res = (map from . extractModels) `fmap` allSatWith (getSolver cfg) cs where to = map (fromRational :: Rational -> AlgReal) from = map (toRational :: AlgReal -> Rational) cs = buildConstraints "solveRationalLinearEqsAll" (map to coeffs) (to res)@@ -154,3 +141,18 @@ 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,+the backend solver will need to understand unbounded integers and rationals. Currently, the following+solvers provide the required capability: 'Z3', 'CVC4', and 'MathSAT'. Passing other instances will result+in an "unsupported" error, though this can of course change as the SBV package itself evolves.+-}
RELEASENOTES view
@@ -1,7 +1,15 @@ Hackage: <http://hackage.haskell.org/package/linearEqSolver> GitHub: <http://github.com/LeventErkok/linearEqSolver> -Latest Hackage released version: 1.2+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
linearEqSolver.cabal view
@@ -1,15 +1,9 @@ Name: linearEqSolver-Version: 1.2+Version: 1.3 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. .- Currently, the following SMT solvers are supported:- .- * Z3 from Microsoft (<http://z3.codeplex.com/>).- .- * CVC4 from New York University and the University of Iowa (<http://cvc4.cs.nyu.edu>) - linearEqSolver is hosted at GitHub: <http://github.com/LeventErkok/linearEqSolver>. Comments, bug reports, and patches are always welcome. .@@ -36,5 +30,5 @@ default-language: Haskell2010 ghc-options : -Wall Build-Depends : base >= 4 && < 5- , sbv >= 2.9+ , sbv >= 3.1 Exposed-modules : Math.LinearEquationSolver