up previous next
MSatLinSolve



Syntax
MSatLinSolve(Env: RECORD): MATRIX

Description
This function calls MathSAT implementation of the symplex method.

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

Example
/**/ system := 
/**/   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
/**/         ];
/**/ sol := MSatLinSolve(system);  sol;
matrix(QQ,
 [[1],
  [4/5],
  [-11/5]])
/**/ // verify:
/**/ sol1 := ConcatVer(sol, matrix([[1]])); //-->  [[1], [4/5], [-11/5], [1]]
/**/ system.leq0 * sol1;  // is <= 0
matrix(QQ,
 [[0],
  [0]])
/**/ system.neq0 * sol1;  // is <> 0
matrix(QQ,
 [[1]])
/**/ // now we add new contraints:
/**/ system.eq0 := RowMat([1,1,0, 4]);   //  x +y +4 = 0
/**/ system.lt0 := RowMat([0,1,0, 0]);   //     y    < 0
/**/ sol := MSatLinSolve(system);  sol;
matrix(QQ,
 [[-2],
  [-2],
  [-2/7]])
/**/ // verify:
/**/ sol1 := ConcatVer(sol, RowMat([1]));  //-->  [[-2], [-2], [-2/7], [1]]
/**/ system.leq0 * sol1;  // <= 0
matrix(QQ,
 [[-20/7],
  [-36]])
/**/ system.neq0 * sol1;  // <> 0
matrix(QQ,
 [[-2]])
/**/ system.eq0  * sol1;  //  = 0
matrix(QQ,
 [[0]])
/**/ system.lt0  * sol1;  //  < 0
matrix(QQ,
 [[-2]])

See Also