MathSAT is a Satisfiability modulo theories (SMT) solver. MathSAT is free software. The joint reasearch between CoCoA and MathSAT has been supported by European Union's Horizon 2020 research and innovation programme under grant agreement No H2020-FETOPEN-2015-CSA 712689: **SC-square** website
Available functions:
MathSAT::env E; // constructor (wrapper for MathSAT ``env``)
MathSAT::AddEq0(E, linear-poly or matrix);
MathSAT::AddNeq0(E, linear-poly or matrix);
MathSAT::AddLeq0(E, linear-poly or matrix);
MathSAT::AddLt0(E, linear-poly or matrix);
MathSAT::LinSolve(E);
| **MathSAT** website |
CoCoALib requires MathSAT release 5 or later. Download MathSAT from the website (binary only).
Look to see where the library file libmathsat.a is.
Then configure and compile CoCoALib typing
cd CoCoALib-0.99 ./configure --with-libmathsat=<your_path_to>/libmathsat.a make
2018