linearEqSolver 1.1 → 1.2

raw patch · 6 files changed

+73/−28 lines, 6 filesdep ~sbvPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: sbv

API changes (from Hackage documentation)

Files

• COPYRIGHT +1/−1
• LICENSE +1/−1
• Math/LinearEquationSolver.hs +48/−17
• README +5/−2
• RELEASENOTES +7/−1
• linearEqSolver.cabal +11/−6

@@ -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

@@ -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

@@ -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: <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+ -- | 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)

@@ -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 ============

@@ -1,7 +1,13 @@ Hackage: <http://hackage.haskell.org/package/linearEqSolver> GitHub:  <http://github.com/LeventErkok/linearEqSolver> -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

@@ -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 (<http://research.microsoft.com/en-us/um/redmond/projects/z3/>).+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.                .                .                Release notes can be seen at: <http://github.com/LeventErkok/linearEqSolver/blob/master/RELEASENOTES>. -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