úÎ6d5Ústableerkokl@gmail.comNoneLInterface to the SMT solver, via the SBV library. Unless you need to create Z custom solvers, or tweak the existing ones, you should not need to use this type: Simply  use the values  and ' to access the respective SMT solvers. "The Z3 SMT solver from Microsoft:  http://z3.codeplex.com/. IThe CVC4 SMT solver from New York University and the University of Iowa:  http://cvc4.cs.nyu.edu. BSolve 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 , 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 EsolveIntegerLinearEqs z3 [[2, 3, 4],[6, -3, 9],[2, 0, 1]] [20, -6, 8] Just [5,6,-2]AThe first argument picks the SMT solver to use. Valid values are  and  I. Naturally, you should have the chosen solver installed on your system. ,In case there are no solutions, we will get : *solveIntegerLinearEqs z3 [[1], [1]] [2, 3]NothingWNote that there are no solutions to this second system as it stipulates the unknown is ) equal to both 2 and 3. (Overspecified.)  Similar to ), except returns all possible solutions. H Note that there might be an infinite number of solutions if the system N is underspecified, in which case the result will be a lazy list of solutions 0 that the caller can consume as much as needed. Here'Hs an example call, where we underspecify the system and hence there are c multiple (in this case an infinite number of) solutions. Here, we only take the first 3 elements, S for testing purposes, but all such results can be computed lazily. Our system is:    2x + 3y + 4z = 20  6x - 3y + 9z = -6  We have: Itake 3 `fmap` solveIntegerLinearEqsAll z3 [[2, 3, 4],[6, -3, 9]] [20, -6][[5,6,-2],[-8,4,6],[18,8,-10]]GSolve a system of linear equations over rationals. Same as the integer  version (, except it takes rational coefficients  and returns rational results. Here'?s an example call, to solve the following system of equations:    2.4x + 3.6y = 12  7.2x - 5y = -8.5 ;solveRationalLinearEqs z3 [[2.4, 3.6],[7.2, -5]] [12, -8.5]Just [245 % 316,445 % 158]?Solve a system of linear equations over rationals. Similar to , ) except it returns all solutions lazily. Example system:    2.4x + 3.6y = 12 aIn 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]] RBuild the constraints as given by the coefficient matrix and the resulting vector SMT Solver to use, pass one of  or  Coefficient matrix (A) Result vector (b) A solution to Ax = b , if any SMT Solver to use, pass one of  or  Coefficient matrix (A) Result vector (b) All solutions to Ax = b SMT Solver to use, pass one of  or  Coefficient matrix (A) Result vector (b) A solution to Ax = b , if any SMT Solver to use, pass one of  or  Coefficient matrix (A) Result vector (b) All solutions to Ax = b     linearEqSolver-1.2Math.LinearEquationSolverSolverz3cvc4solveIntegerLinearEqssolveIntegerLinearEqsAllsolveRationalLinearEqssolveRationalLinearEqsAllbase Data.MaybeNothingbuildConstraints