úÎ4ý42   (c) Levent ErkokBSD3erkokl@gmail.comstableNonehSolve 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.)CHere's an example call, to solve the following system of equations: A 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  H. 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]NothingNote that there are no solutions to this second system as it stipulates the unknown is equal to both 2 and 3. (Overspecified.) Similar to ÿh, 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 ask for the first 3 elements for testing purposes. , 2x + 3y + 4z = 20 6x - 3y + 9z = -6 We have:=solveIntegerLinearEqsAll Z3 3 [[2, 3, 4],[6, -3, 9]] [20, -6] [[-8,4,6],[-21,2,14],[-34,0,22]]fThe solutions you get might differ, depending on what the solver returns. (Though they'll be correct!) PSolve a system of linear equations over rationals. Same as the integer version F, except it takes rational coefficients and returns rational results.CHere'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  Z, except if the system is underspecified, then returns the number of solutions requested.Example system:  2.4x + 3.6y = 12 `In this case, the system has infinitely many solutions. We can compute three of them as follows:0solveRationalLinearEqsAll Z3 3 [[2.4, 3.6]] [12]2[[5 % 1,0 % 1],[13 % 2,(-1) % 1],[8 % 1,(-2) % 1]]fThe solutions you get might differ, depending on what the solver returns. (Though they'll be correct!)QBuild the constraints as given by the coefficient matrix and the resulting vectorSMT Solver to useCoefficient matrix (A)Result vector (b)A solution to Ax = b, if anySMT Solver to use7Maximum number of solutions to return, in case infiniteCoefficient matrix (A)Result vector (b)All solutions to Ax = b SMT Solver to useCoefficient matrix (A)Result vector (b)A solution to Ax = b, if any SMT Solver to use7Maximum number of solutions to return, in case infiniteCoefficient matrix (A)Result vector (b)All solutions to Ax = b         )linearEqSolver-2.0-HGKQcpCQUVMBL9uX2AkzhVMath.LinearEquationSolversbv-7.3-BWruDmkFkY464YFc9btlI5Data.SBV.Core.SymbolicABCMathSATCVC4 BoolectorYicesZ3SolversolveIntegerLinearEqssolveIntegerLinearEqsAllsolveRationalLinearEqssolveRationalLinearEqsAllbaseGHC.BaseNothingData.SBV.Provers.Proverz3cvc4buildConstraints