A simple wrapper to run multiple SMT solvers in parallel.
Project description
smt-portfolio
A simple wrapper to run multiple SMT solvers in parallel (currently supporting Z3 and CVC5).
Requirements
- Z3
- CVC5
- Vampire
Installation
pip install smt-portfolio
Usage
smt-portfolio --help
smt-portfolio --file examples/ex1.smt2 --z3 "-smt2 -T:5" --cvc5 "--quiet --lang smt --dag-thresh=0 --enum-inst --tlimit 5000" --vampire "--input_syntax smtlib2 --output_mode smtcomp --time_limit 5"
cat examples/ex1.smt2 | smt-portfolio --z3 "-smt2 -T:5" --cvc5 "--quiet --lang smt --dag-thresh=0 --enum-inst --tlimit 5000" --vampire "--input_syntax smtlib2 --output_mode smtcomp --time_limit 5"
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
smt_portfolio-0.3.3.tar.gz
(4.9 kB
view hashes)
Built Distribution
Close
Hashes for smt_portfolio-0.3.3-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 49cf9cca704d4f74389202e6965ff2cd85ba566aa6753dab7f1d161585488af9 |
|
MD5 | c2dc40f8769de40ff97a1e6b38f82e0b |
|
BLAKE2b-256 | e8caa90027fa5981a2de1516073f633b3995f29d654471b4a05c71a551e01d42 |