shabesoglu / smtrat Goto Github PK

Project name: SMT-RAT - Satisfiability-Modulo-Theories Real Algebra Toolbox
Contact: Florian Corzilius <[email protected]>, 
         Gereon Kremer <[email protected]>, 
         Sebastian Junges <[email protected]>, 
         Stefan Schupp <[email protected]>
Project sourceforge page: https://github.com/smtrat/smtrat

* Prerequisites
 - A C++ Compiler with c++11x capabilities. We assume GCC 4.8 or higher.
 - The build system CMake: http://www.cmake.org/ (only for building the library)
 - The library CArL: https://github.com/smtrat/carl (formula and polynomial data structures and basic operation)

* Optional dependencies
 - The library GiNaC: http://www.ginac.de/ (if usage of polynomial factorization is enabled, which is recommended for NIA and NRA)
 - The documentation build system Doxygen: http://www.stack.nl/~dimitri/doxygen/ 
 - The build system Ant: http://ant.apache.org/ (only for building the gui)
 - A Java development environment >= 1.6: http://www.oracle.com/technetwork/java/index.html (only for building the gui)


* How to build the project including library and the binary (solver)
mkdir build   // Create a separate build directory.
cd build
cmake ..      // Configure using cmake. Use "ccmake .." in order for an 
              // interactive user interface with more options.
make          // Build the project, in particular, build the solver smtrat

* Other targets to build

make help      // Show a list of possible targets.
make clean     // Force the build system to re-build everything.
make install   // Install library to the specified (adjust via ccmake) system directory.
make build-gui // Make the java-based GUI.
make run-gui   // Make/run the java-based GUI.
make package   // Construct a package of the project.
make doc       // Build the project API documentation.

* Run the solver
The excecutable solver smtrat can be found in the build directory. It accepts .smt2 files as described by the smtlib (http://www.smtlib.org/).
For more information, run './smtrat --help'. To run the solver on an inputfile 'input.smt2' run './smtrat input.smt2'.

* Documentation
For further understanding of the design of SMT-RAT we refer to our manual (https://github.com/smtrat/smtrat/blob/master/manual/manual_smtrat-2.0.0.pdf). It addresses both, developer of further procedures in SMT-RAT
and those who use SMT-RAT for solving formulas of the supported logics. For the latter it is possible to use SMT-RAT as a library via API
or directly via command line. The user can in both cases define a solving strategy with the provided GUI. 

* How to build the API documentation

Required: Doxygen: http://www.stack.nl/~dimitri/doxygen/

make doc

* Troubleshooting

  This list can grow - with your help! Just contact one of the authors.