© 2017 John Abbott, Anna Bigatti
GNU Free Documentation License, Version 1.2

CoCoALib Documentation Index

User documentation

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);


Download and compile MathSAT

**MathSAT** website

CoCoALib requires MathSAT release 5 or later. Download MathSAT from the website.

  mkdir BUILD
  cd BUILD
  cmake ..

then the library is libmathsat.a in dir BUILD.

Configure and compile CoCoALib with MathSAT

Look to see where the library file libmathsat.a is -- on my computer it was inside the MathSAT subdirectory BUILD/. Note the full path to the library file as you will need it when configuring CoCoALib!

Then configure and compile CoCoALib typing

  cd CoCoALib-0.99
  ./configure --with-libmathsat=<your_path_to>/libmathsat.a

Maintainer documentation

Bugs, shortcomings and other ideas

Main changes