MSatLinSolve

MSatLinSolve --

Syntax

MSatLinSolve(Env: RECORD): MATRIX

Description

This function calls the MathSAT implementation of the simplex method. The argument Env may contain the following fields: leq0, neq0, eq0, lt0; each field must have as value a matrix with rational entries, where each row of the matrix corresponds to a linear condition. The matrices must all have the same number of columns.

The work for this communication has been partly supported by the European Union Horizon 2020 research and innovation programme under grant agreement No H2020-FETOPEN-2015-CSA 712689: SC-square http://www.sc-square.org.

Example

/**/ LinSys :=
/**/   record[leq0 := matrix([[1,2,3, 4],  //   x +2*y +3*z +4 <= 0
/**/                          [9,8,7, 0]]),// 9*x +8*y +7*z    <= 0
/**/          neq0 := matrix([[1,0,0, 0]]) //   x              <> 0
/**/         ];
/**/ soln := MSatLinSolve(LinSys);  soln;
matrix(QQ,
 [[1],
  [4/5],
  [-11/5]])
/**/ // verify:
/**/ soln1 := ConcatVer(soln, matrix([[1]])); //-->  [[1], [4/5], [-11/5], [1]]
/**/ LinSys.leq0 * soln1;  // is <= 0
matrix(QQ,
 [[0],
  [0]])
/**/ LinSys.neq0 * soln1;  // is <> 0
matrix(QQ,
 [[1]])
/**/ // now we add new contraints:
/**/ LinSys.eq0 := RowMat([1,1,0, 4]);   //  x +y +4 = 0
/**/ LinSys.lt0 := RowMat([0,1,0, 0]);   //     y    < 0
/**/ soln := MSatLinSolve(LinSys);  soln;
matrix(QQ,
 [[-2],
  [-2],
  [-2/7]])
/**/ // verify:
/**/ soln1 := ConcatVer(soln, RowMat([1]));  //-->  [[-2], [-2], [-2/7], [1]]
/**/ LinSys.leq0 * soln1;  // <= 0
matrix(QQ,
 [[-20/7],
  [-36]])
/**/ LinSys.neq0 * soln1;  // <> 0
matrix(QQ,
 [[-2]])
/**/ LinSys.eq0  * soln1;  //  = 0
matrix(QQ,
 [[0]])
/**/ LinSys.lt0  * soln1;  //  < 0
matrix(QQ,
 [[-2]])

See Also