diff --git a/CHANGES.md b/CHANGES.md new file mode 100644 --- /dev/null +++ b/CHANGES.md @@ -0,0 +1,33 @@ +* Hackage: +* GitHub: + +* 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. diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -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 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-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 diff --git a/Math/LinearEquationSolver.hs b/Math/LinearEquationSolver.hs --- a/Math/LinearEquationSolver.hs +++ b/Math/LinearEquationSolver.hs @@ -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, diff --git a/README b/README --- a/README +++ b/README @@ -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) diff --git a/RELEASENOTES b/RELEASENOTES deleted file mode 100644 --- a/RELEASENOTES +++ /dev/null @@ -1,30 +0,0 @@ -Hackage: -GitHub: - -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. diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -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 diff --git a/linearEqSolver.cabal b/linearEqSolver.cabal --- a/linearEqSolver.cabal +++ b/linearEqSolver.cabal @@ -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: . + Release notes can be seen at: -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