-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Use SMT solvers to solve linear systems over integers and rationals
--   
--   Solve linear systems of equations over integers and rationals, using
--   an SMT solver.
--   
--   Currently, the following SMT solvers are supported:
--   
--   <ul>
--   <li>Z3 from Microsoft (<a>http://z3.codeplex.com/</a>).</li>
--   <li>CVC4 from New York University and the University of Iowa
--   (<a>http://cvc4.cs.nyu.edu</a>) linearEqSolver is hosted at GitHub:
--   <a>http://github.com/LeventErkok/linearEqSolver</a>. Comments, bug
--   reports, and patches are always welcome.</li>
--   </ul>
--   
--   Release notes can be seen at:
--   <a>http://github.com/LeventErkok/linearEqSolver/blob/master/RELEASENOTES</a>.
@package linearEqSolver
@version 1.2


-- | (The linear equation solver library is hosted at
--   <a>http://github.com/LeventErkok/linearEqSolver</a>. Comments, bug
--   reports, and patches are always welcome.)
--   
--   Solvers for linear equations over integers and rationals. Both single
--   solution and all solution variants are supported.
module Math.LinearEquationSolver

-- | The Z3 SMT solver from Microsoft: <a>http://z3.codeplex.com/</a>.
z3 :: Solver

-- | The CVC4 SMT solver from New York University and the University of
--   Iowa: <a>http://cvc4.cs.nyu.edu</a>.
cvc4 :: Solver

-- | 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 <a>z3</a> and <a>cvc4</a> to
--   access the respective SMT solvers.
newtype Solver
Solver :: SMTConfig -> Solver

-- | Solve a system of linear integer equations. The first argument is the
--   matrix of coefficients, known as <tt>A</tt>, of size <tt>mxn</tt>. The
--   second argument is the vector of results, known as <tt>b</tt>, of size
--   <tt>mx1</tt>. The result will be either <a>Nothing</a>, if there is no
--   solution, or <tt>Just x</tt> -- such that <tt>Ax = b</tt> holds.
--   (Naturally, the result <tt>x</tt> will be a vector of size
--   <tt>nx1</tt> in this case.)
--   
--   Here's an example call, to solve the following system of equations:
--   
--   <pre>
--   2x + 3y + 4z = 20
--   6x - 3y + 9z = -6
--   2x      +  z = 8
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; solveIntegerLinearEqs z3 [[2, 3, 4],[6, -3, 9],[2, 0, 1]] [20, -6, 8]
--   Just [5,6,-2]
--   </pre>
--   
--   The first argument picks the SMT solver to use. Valid values are
--   <a>z3</a> and <a>cvc4</a>. Naturally, you should have the chosen
--   solver installed on your system.
--   
--   In case there are no solutions, we will get <a>Nothing</a>:
--   
--   <pre>
--   &gt;&gt;&gt; solveIntegerLinearEqs z3 [[1], [1]] [2, 3]
--   Nothing
--   </pre>
--   
--   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 -> [[Integer]] -> [Integer] -> IO (Maybe [Integer])

-- | Similar to <a>solveIntegerLinearEqs</a>, 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:
--   
--   <pre>
--   2x + 3y + 4z = 20
--   6x - 3y + 9z = -6
--   </pre>
--   
--   We have:
--   
--   <pre>
--   &gt;&gt;&gt; take 3 `fmap` solveIntegerLinearEqsAll z3 [[2, 3, 4],[6, -3, 9]] [20, -6]
--   [[5,6,-2],[-8,4,6],[18,8,-10]]
--   </pre>
solveIntegerLinearEqsAll :: Solver -> [[Integer]] -> [Integer] -> IO [[Integer]]

-- | Solve a system of linear equations over rationals. Same as the integer
--   version <a>solveIntegerLinearEqs</a>, except it takes rational
--   coefficients and returns rational results.
--   
--   Here's an example call, to solve the following system of equations:
--   
--   <pre>
--   2.4x + 3.6y = 12
--   7.2x - 5y   = -8.5
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; solveRationalLinearEqs z3 [[2.4, 3.6],[7.2, -5]] [12, -8.5]
--   Just [245 % 316,445 % 158]
--   </pre>
solveRationalLinearEqs :: Solver -> [[Rational]] -> [Rational] -> IO (Maybe [Rational])

-- | Solve a system of linear equations over rationals. Similar to
--   <a>solveRationalLinearEqs</a>, except it returns all solutions lazily.
--   
--   Example system:
--   
--   <pre>
--   2.4x + 3.6y = 12
--   </pre>
--   
--   In this case, the system has infinitely many solutions. We can compute
--   three of them as follows:
--   
--   <pre>
--   &gt;&gt;&gt; take 3 `fmap` solveRationalLinearEqsAll z3 [[2.4, 3.6]] [12]
--   [[5 % 1,0 % 1],[0 % 1,10 % 3],[3 % 2,7 % 3]]
--   </pre>
solveRationalLinearEqsAll :: Solver -> [[Rational]] -> [Rational] -> IO [[Rational]]