Skip to content
OMT Examples using OptiMathSAT's python API
SMT Python
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
include
optimathsat
unit-tests
.gitignore
LICENSE
README.md
build.py
run.py

README.md

DESCRIPTION

This is a collection of Optimization Modulo Theories examples using the Python API interface of OptiMathSAT.

REQUIREMENTS

This project requires Python 3.X and gmplib.

BUILDING

Download the package of the latest version of OptiMathSAT (v. 1.6.2 or superior) inside the directory optimathsat, and unpack it. Then, run the build.py script as follows:

~$ python3 build.py

This command builds the Python API of OptiMathSAT, and places the generated mathsat.py file in the include directory and the generated _mathsat.so file in the lib directory.

For convenience, you may want to permanently add both of these locations to your PYTHONPATH environment variable:

export PYTHONPATH=${PYTHONPATH}:.../omt_python_examples/include
export PYTHONPATH=${PYTHONPATH}:.../omt_python_examples/lib

This step is useful to avoid import complaints with pylint3. The unit-test scripts, however, are expected to work even without performing this step.

USAGE

Run all unit-test examples with

~$ python3 run.py

Each unit-test can also be executed on its own. For instance, the unit-test simple_omt.py can be run with

~$ ./unit-tests/simple_omt.py

or with

~$ python3 unit-tests/simple_omt.py

NOTES

Please contact the author of this repository, or the current maintainer of the OptiMathSAT, in the case that there is still any persisting issue with these unit-tests.

Contributors

This project is authored by Patrick Trentin (patrick.trentin.88@gmail.com).

You can’t perform that action at this time.