metaSMT-toolbox-smt2eval

metaSMT-toolbox-smt2eval is a metaSMT toolbox project that allows a user to read and evaluate SMT-LIB2 instances utilizing a varity of different solving engines. The project leverages Z3's parser to read files in SMT-LIB2 format and metaSMT to evaluate them.

Requirements

The following software is required in order to build metaSMT-toolbox-smt2eval

metaSMT
Z3

Build metaSMT-toolbox-smt2eval

metaSMT-toolbox-smt2eval is not a standalone application but a toolbox project for metaSMT. The metaSMT source code has to be installed first. The Z3 library is automatically installed as a part of metaSMT.

Install metaSMT to directory <metaSMT_DIRECTORY>.
Clone metaSMT-toolbox-smt2eval in directory <metaSMT_DIRECTORY>/toolbox.
Build metaSMT following the normal build instructions. metaSMT will build in the usual way with the additional executables to check satisfiability and consistency of SMT-LIB2 instances. The additional executables follow the naming scheme smt2_sat_check_* and smt2_consistency_check_*.

Name		Name	Last commit message	Last commit date
Latest commit History 4 Commits
CMakeLists.txt		CMakeLists.txt
LICENSE		LICENSE
README.md		README.md
consistency_check.hpp		consistency_check.hpp
conversion_utils.cpp		conversion_utils.cpp
conversion_utils.hpp		conversion_utils.hpp
sat_check.hpp		sat_check.hpp
smt2_consistency_check_Boolector.cpp		smt2_consistency_check_Boolector.cpp
smt2_consistency_check_CVC4.cpp		smt2_consistency_check_CVC4.cpp
smt2_consistency_check_MiniSat.cpp		smt2_consistency_check_MiniSat.cpp
smt2_consistency_check_SMT2.cpp		smt2_consistency_check_SMT2.cpp
smt2_consistency_check_STP.cpp		smt2_consistency_check_STP.cpp
smt2_consistency_check_Z3.cpp		smt2_consistency_check_Z3.cpp
smt2_consistency_check_lingeling.cpp		smt2_consistency_check_lingeling.cpp
smt2_consistency_check_picosat.cpp		smt2_consistency_check_picosat.cpp
smt2_sat_check_Boolector.cpp		smt2_sat_check_Boolector.cpp
smt2_sat_check_CVC4.cpp		smt2_sat_check_CVC4.cpp
smt2_sat_check_MiniSat.cpp		smt2_sat_check_MiniSat.cpp
smt2_sat_check_SMT2.cpp		smt2_sat_check_SMT2.cpp
smt2_sat_check_STP.cpp		smt2_sat_check_STP.cpp
smt2_sat_check_Z3.cpp		smt2_sat_check_Z3.cpp
smt2_sat_check_lingeling.cpp		smt2_sat_check_lingeling.cpp
smt2_sat_check_picosat.cpp		smt2_sat_check_picosat.cpp
z3_expr_visitor.hpp		z3_expr_visitor.hpp
z3_utils.cpp		z3_utils.cpp
z3_utils.hpp		z3_utils.hpp

License

hriener/metaSMT-toolbox-smt2eval

Folders and files

Latest commit

History

Repository files navigation

metaSMT-toolbox-smt2eval

Requirements

Build metaSMT-toolbox-smt2eval

About

Topics

Resources

License

Stars

Watchers

Forks

Languages