diff --git a/Math/LinearEquationSolver.hs b/Math/LinearEquationSolver.hs --- a/Math/LinearEquationSolver.hs +++ b/Math/LinearEquationSolver.hs @@ -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: . -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 +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. +-} diff --git a/RELEASENOTES b/RELEASENOTES --- a/RELEASENOTES +++ b/RELEASENOTES @@ -1,7 +1,15 @@ Hackage: GitHub: -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 diff --git a/linearEqSolver.cabal b/linearEqSolver.cabal --- a/linearEqSolver.cabal +++ b/linearEqSolver.cabal @@ -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 (). - . - * CVC4 from New York University and the University of Iowa () - linearEqSolver is hosted at GitHub: . 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