Home

Awesome

smt2coral

smt2coral is a small python module and set of command line tools that take constraints in the SMT-LIBv2 format and converts them into the constraint language understood by the Coral constraint solver.

Note that the constraint langauges of Coral and SMT-LIBv2 only partially overlap in terms of capability. Therefore only a subset of SMT-LIBv2 is supported.

There are several known restrictions due Coral's language constraint being very crude.

In addition to the above issues, coral itself (well at least version 0.7) is very buggy and frequently crashes. This will likely limit the use of this project, however it was quite fun to write so I can't complain too much ;).

Tools

dump.py

This tool parses SMT-LIBv2 constraints and then dumps the converted constraints as text. This is useful for debugging/testing. An error will be raised if the translation cannot be performed.

coral.py

This is a wrapper for Coral that parses SMT-LIBv2 constraints, invokes coral and responds in a "mostly" SMT-LIBv2 compliant manner.

Note you need to place coral.jar in the same directory as coral.py. coral.jar is available at http://pan.cin.ufpe.br/coral/Download.html .

Note that the coral.py script will ignore command line arguments it doesn't recognise and will pass them directly to Coral. This is for using Coral's various solver options.

Dependencies

For testing

Testing

Run

lit -vs tests/