diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -1,4 +1,4 @@ -Copyright (c) 2012, Levent Erkok (erkokl@gmail.com) +Copyright (c) 2012-2013, Levent Erkok (erkokl@gmail.com) All rights reserved. The linearEqSolver library is distributed with the BSD3 license. See the LICENSE file diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,6 +1,6 @@ linearEqSolver: Solves linear systems of equations, using SMT solving. -Copyright (c) 2012, Levent Erkok (erkokl@gmail.com) +Copyright (c) 2012-2013, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without diff --git a/Math/LinearEquationSolver.hs b/Math/LinearEquationSolver.hs --- a/Math/LinearEquationSolver.hs +++ b/Math/LinearEquationSolver.hs @@ -14,20 +14,36 @@ --------------------------------------------------------------------------------- module Math.LinearEquationSolver ( + -- * Available SMT solvers + z3, cvc4, Solver(..) -- * Solutions over Integers - solveIntegerLinearEqs + , solveIntegerLinearEqs , solveIntegerLinearEqsAll -- * Solutions over Rationals , solveRationalLinearEqs , solveRationalLinearEqsAll ) where -import Data.SBV +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: . +z3 :: Solver +z3 = Solver SBV.z3 + +-- | The CVC4 SMT solver from New York University and the University of Iowa: . +cvc4 :: Solver +cvc4 = Solver SBV.cvc4 + -- | Solve a system of linear integer equations. The first argument is -- the matrix of coefficients, known as @A@, of size @mxn@. The second argument --- is the vector of results, known as @B@, of size @mx1@. The result will be --- either `Nothing`, if there is no solution, or @Just x@ -- such that @Ax = B@ holds. +-- is the vector of results, known as @b@, of size @mx1@. The result will be +-- either `Nothing`, if there is no solution, or @Just x@ -- such that @Ax = b@ holds. -- (Naturally, the result @x@ will be a vector of size @nx1@ in this case.) -- -- Here's an example call, to solve the following system of equations: @@ -38,18 +54,24 @@ -- 2x + z = 8 -- @ -- --- >>> solveIntegerLinearEqs [[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 +-- 'cvc4'. Naturally, you should have the chosen solver installed on your system. +-- -- In case there are no solutions, we will get `Nothing`: -- --- >>> solveIntegerLinearEqs [[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 :: [[Integer]] -> [Integer] -> IO (Maybe [Integer]) -solveIntegerLinearEqs coeffs res = extractModel `fmap` sat cs +solveIntegerLinearEqs :: Solver -- ^ SMT Solver to use, pass one of 'z3' or 'cvc4' + -> [[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 where cs = buildConstraints "solveIntegerLinearEqs" coeffs res -- | Similar to `solveIntegerLinearEqs`, except returns all possible solutions. @@ -68,10 +90,13 @@ -- -- We have: -- --- >>> take 3 `fmap` solveIntegerLinearEqsAll [[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 :: [[Integer]] -> [Integer] -> IO [[Integer]] -solveIntegerLinearEqsAll coeffs res = extractModels `fmap` allSat cs +solveIntegerLinearEqsAll :: Solver -- ^ SMT Solver to use, pass one of 'z3' or 'cvc4' + -> [[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 where cs = buildConstraints "solveIntegerLinearEqsAll" coeffs res -- | Solve a system of linear equations over rationals. Same as the integer @@ -85,10 +110,13 @@ -- 7.2x - 5y = -8.5 -- @ -- --- >>> solveRationalLinearEqs [[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 :: [[Rational]] -> [Rational] -> IO (Maybe [Rational]) -solveRationalLinearEqs coeffs res = (fmap from . extractModel) `fmap` sat cs +solveRationalLinearEqs :: Solver -- ^ SMT Solver to use, pass one of 'z3' or 'cvc4' + -> [[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 where to = map (fromRational :: Rational -> AlgReal) from = map (toRational :: AlgReal -> Rational) cs = buildConstraints "solveRationalLinearEqs" (map to coeffs) (to res) @@ -104,10 +132,13 @@ -- -- In this case, the system has infinitely many solutions. We can compute three of them as follows: -- --- >>> take 3 `fmap` solveRationalLinearEqsAll [[2.4, 3.6]] [12] +-- >>> take 3 `fmap` solveRationalLinearEqsAll z3 [[2.4, 3.6]] [12] -- [[5 % 1,0 % 1],[0 % 1,10 % 3],[3 % 2,7 % 3]] -solveRationalLinearEqsAll :: [[Rational]] -> [Rational] -> IO [[Rational]] -solveRationalLinearEqsAll coeffs res = (map from . extractModels) `fmap` allSat cs +solveRationalLinearEqsAll :: Solver -- ^ SMT Solver to use, pass one of 'z3' or 'cvc4' + -> [[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 where to = map (fromRational :: Rational -> AlgReal) from = map (toRational :: AlgReal -> Rational) cs = buildConstraints "solveRationalLinearEqsAll" (map to coeffs) (to res) diff --git a/README b/README --- a/README +++ b/README @@ -1,8 +1,11 @@ linearEqSolver ============== -Solve systems of linear equations, using SMT solvers. Both integer only solutions, and solutions -over rationals are supported. +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. + +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 ============ diff --git a/RELEASENOTES b/RELEASENOTES --- a/RELEASENOTES +++ b/RELEASENOTES @@ -1,7 +1,13 @@ Hackage: GitHub: -Latest Hackage released version: 1.1 +Latest Hackage released version: 1.2 + +====================================================================== +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 diff --git a/linearEqSolver.cabal b/linearEqSolver.cabal --- a/linearEqSolver.cabal +++ b/linearEqSolver.cabal @@ -1,17 +1,22 @@ Name: linearEqSolver -Version: 1.1 +Version: 1.2 Category: Math, SMT -Synopsis: Use SMT solvers to solve linear systems of equations over integers and rationals. -Description: Express and solve linear systems of equations over integers and rationals, using an SMT solver to do the actual solving. - By default, we use Microsoft's Z3 SMT solver (). +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 (). + . + * CVC4 from New York University and the University of Iowa () + linearEqSolver is hosted at GitHub: . Comments, bug reports, and patches are always welcome. . . Release notes can be seen at: . -Copyright: Levent Erkok, 2012 +Copyright: Levent Erkok, 2012-2013 License: BSD3 License-file: LICENSE Stability: Experimental @@ -31,5 +36,5 @@ default-language: Haskell2010 ghc-options : -Wall Build-Depends : base >= 4 && < 5 - , sbv >= 2.7 + , sbv >= 2.9 Exposed-modules : Math.LinearEquationSolver