linearEqSolver (empty) → 1.0

raw patch · 8 files changed

+214/−0 lines, 8 filesdep +basedep +sbvsetup-changed

Dependencies added: base, sbv

Files

• COPYRIGHT +5/−0
• INSTALL +10/−0
• LICENSE +26/−0
• Math/LinearEquationSolver.hs +99/−0
• README +9/−0
• RELEASENOTES +9/−0
• Setup.hs +18/−0
• linearEqSolver.cabal +38/−0

@@ -0,0 +1,5 @@+Copyright (c) 2012, Levent Erkok (erkokl@gmail.com)+All rights reserved.++The linearEqSolver library is distributed with the BSD3 license. See the LICENSE file+for details.

@@ -0,0 +1,10 @@+The linearEqSolver library can be installed simply by issuing cabal install+like this:++     cabal install linearEqSolver++The library uses the sbv package on hackage, which will automatically be+installed if you do not have it already. You should also install+Z3, the default SMT solver used by sbv, from Microsoft. (You can get it+from http://research.microsoft.com/en-us/um/redmond/projects/z3/.)+Please make sure that the "z3" executable is in your path.

@@ -0,0 +1,26 @@+linearEqSolver: Solves linear systems of equations over integers, using SMT solving.++Copyright (c) 2012, Levent Erkok (erkokl@gmail.com)+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:+    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.+    * Redistributions in binary form must reproduce the above copyright+      notice, this list of conditions and the following disclaimer in the+      documentation and/or other materials provided with the distribution.+    * Neither the name of the developer (Levent Erkok) nor the+      names of its contributors may be used to endorse or promote products+      derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL LEVENT ERKOK BE LIABLE FOR ANY+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,99 @@+---------------------------------------------------------------------------------+-- |+-- Module      :  Math.LinearEquationSolver+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- (The linear equation solver library is hosted at <http://github.com/LeventErkok/linearEqSolver>.+-- Comments, bug reports, and patches are always welcome.)+--+-- Solvers for linear equations over integers. Both single solution and all+-- solution variants are supported.+---------------------------------------------------------------------------------++module Math.LinearEquationSolver (+       -- * Finding a solution+       solveIntegerLinearEqs+       -- * Finding all solutions+    ,  solveIntegerLinearEqsAll+    ) where++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+-- 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:+--+-- @+--     2x + 3y + 4z = 20+--     6x - 3y + 9z = -6+--     2x      +  z = 8+-- @+--+-- >>> solveIntegerLinearEqs [[2,3,4],[6,-3,9],[2,0,1]] [20,-6,8]+-- Just [5,6,-2]+--+-- In case there are no solutions, we will get `Nothing`:+--+-- >>> solveIntegerLinearEqs [[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+  | Just n <- check coeffs res+  = extractModel `fmap` sat (buildConstraints n coeffs res)+  | True+  = error "solveIntegerLinearEqs: Received ill-formed input"++-- | 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.+--+-- 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:+--+-- @+--     2x + 3y + 4z = 20+--     6x - 3y + 9z = -6+-- @+--+-- We have:+--+-- >>> take 3 `fmap` solveIntegerLinearEqsAll [[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+  | Just n <- check coeffs res+  = extractModels `fmap` allSat (buildConstraints n coeffs res)+  | True+  = error "solveIntegerLinearEqsAll: Received ill-formed input"++-- | Check that the arguments are well-formed. Returns Just the number of variables needed+-- if the arguments are well formed, otherwise Nothing.+check :: [[Integer]] -> [Integer] -> Maybe Int+check a b+  | m > 0 && not (null ns) && all (== n) ns && m == lb+  = Just n+  | True+  = Nothing+  where m  = length a+        ns = map length a+        n  = head ns+        lb = length b++-- | Build the constraints corresponding to the system given+buildConstraints :: Int -> [[Integer]] -> [Integer] -> Symbolic SBool+buildConstraints n coeffs res = do+        xs <- mkFreeVars n+        let rowEq row r = sum (zipWith (*) xs row) .== r+        solve $ zipWith rowEq (map (map literal) coeffs) (map literal res)

@@ -0,0 +1,9 @@+linearEqSolver+==============++Solve systems of linear equations of many unknowns, using SMT solvers.++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)

@@ -0,0 +1,9 @@+Hackage: <http://hackage.haskell.org/package/linearEqSolver>+GitHub:  <http://github.com/LeventErkok/linearEqSolver>++Latest Hackage released version: 1.0++======================================================================+Version 1.0, Not yet released++  - Initial release, contains solver for integer linear equations.

@@ -0,0 +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

@@ -0,0 +1,38 @@+Name:          linearEqSolver+Version:       1.0+Category:      Math, SMT+Synopsis:      Solve linear systems of equations over integers.+Description:   Express and solve linear systems of equations over integers, 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/>).+               .+               You can get a single solution if it exists. Or ask for all possible solutions for underspecified+               systems, which will be lazily returned in a list.+               .+               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+License:       BSD3+License-file:  LICENSE+Stability:     Experimental+Author:        Levent Erkok+Homepage:      http://github.com/LeventErkok/linearEqSolver+Bug-reports:   http://github.com/LeventErkok/linearEqSolver/issues+Maintainer:    Levent Erkok (erkokl@gmail.com)+Build-Type:    Simple+Cabal-Version: >= 1.14+Extra-Source-Files: INSTALL, README, COPYRIGHT, RELEASENOTES++source-repository head+    type:       git+    location:   git://github.com/LeventErkok/linearEqSolver.git++Library+  default-language: Haskell2010+  ghc-options     : -Wall+  Build-Depends   : base >= 4 && < 5+                  , sbv+  Exposed-modules : Math.LinearEquationSolver