================================================================================ Solving Quantified Bit-Vectors using Invertibility Conditions Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli ================================================================================ -------------------------------------------------------------------------------- Structure of the artifact: -------------------------------------------------------------------------------- Directories: ------------------------------------------------------------------------------ ** benchmarks/ ------------- - benchmarks-35/ Contains a subset of benchmarks from directory BV/ that finishes in a reasonable amount of time. Will be run with ./run-experiments.sh. All benchmarks of this set can be solved by all configurations in Table 4 within 5 seconds. - benchmarks-sygus/ Contains the SyGuS benchmarks to synthesize invertibility conditions with CVC4 (solvers/cvc4) as described in Section 3.1 of our paper. - benchmarks-verification/ Contains all benchmarks for verifying the synthesized invertibility conditions as described in Section 3.2 of our paper. - BV/ Contains all benchmarks from the quantified bit-vector (BV) logic of SMT-LIB. These are the benchmarks that we used in our evaluation in Section 5, Table 4. ** raw-data/ ----------- Contains Job26995_info.csv with the raw data as extracted from StarExec from our evaluation in Section 5. The script convert-starexec.sh was used to convert this data into result files (directory results/) that can be used with scripts/compare-smt-runs.py. ** results/ ----------- Contains the results files generated with raw-data/convert-starexec.sh. ** results-sygus/ ----------------- Contains the log files of CVC4 runs for synthesizing invertibility conditions with the general and restricted SyGuS grammar. ** results-verification/ ----------------------- Contains the log files of the Boolector, CVC4, Q3B, and Z3 runs for verifying the invertibility conditions. ** scripts/ ---------- Contains helper scripts. ** solvers/ ---------- Contains all solver versions that were used for our experiments. - Boolector/bin/starexec_run_boolector: Configuration Boolector in Table 4. - CVC4/bin/starexec_run_default: Configuration CVC4 in Table 4. - CVC4-cegqi/bin/starexec_run_cegqi_m: Configuration cegqi_m in Table 4. - CVC4-cegqi/bin/starexec_run_cegqi_k: Configuration cegqi_k in Table 4. - CVC4-cegqi/bin/starexec_run_cegqi_s: Configuration cegqi_s in Table 4. - CVC4-cegqi/bin/starexec_run_cegqi_b: Configuration cegqi_b in Table 4. - Q3B/bin/starexec_run_default: Configuration Q3b in Table 4. - Z3/bin/starexec_run_default: Configuration Z3 in Table 4. - cvc4: The version of CVC4 that was used for synthesizing invertibility conditions in Section 3.1. Note that configurations Boolector, CVC4, Q3B and Z3 were also used for verifying synthesized invertibility conditions in Section 3.2. Files: ------------------------------------------------------------------------------ ** benchmark-set-BV-35 ** benchmark-set-BV-all ** benchmark-set-verify-4bit ** benchmark-set-verify-4bit-boolector ** benchmark-set-verify-all ** benchmark-set-verify-all-boolector ---------------------------------------- These files define benchmark sets for run-{experiments,verification}.sh. ** compare-results.sh ---------------------- Script to generate the results from Section 3.2. ** run-experiments.sh ---------------------- Script to print and re-run the experiments from Section 5, Table 4. ** run-verification.sh ----------------------- Script to re-run the verification experiments from Section 3.2. ** synth-benchmarks ----------------------- Helper script for synthesize-ic.sh to define benchmark sets. ** synthesize-ic.sh ----------------------- Script to re-run the synthesis of invertibility conditions from Section 3.1. -------------------------------------------------------------------------------- Hardware description -------------------------------------------------------------------------------- This artifact has been tested on an Intel i7 8550U with 4GHz and 16GB RAM. The VM is based on the default VM provided by the CAV AEC. User: cav Pw: ae -------------------------------------------------------------------------------- 1) Run experiments from Table 4 (Section 5 - Evaluation) -------------------------------------------------------------------------------- To run a subset of the benchmarks from the evaluation execute the script: ./run-experiments.sh This script will first reproduce the results from Table 4 from the provided log files. It will then run all configurations from Table 4 on a subset of 35 benchmarks from set BV and compare the results against the provided log files. Running all configurations on these 35 benchmarks will take <5 minutes. The complete benchmark set can be run with ./run-experiments.sh -a Running the complete benchmark set with all configurations will take approx. 12 days of CPU time. -------------------------------------------------------------------------------- 2) Generate invertibility conditions with SyGuS (Section 3.1 - Synthesizing ICs) -------------------------------------------------------------------------------- The SyGuS benchmarks that were used in the paper to synthesize invertibility conditions are located in the directories benchmarks/benchmarks-sygus/grammar_{g,r}. Directory 'grammar_g' contains the SyGuS benchmarks with the general grammar. Directory 'grammar_r' contains all benchmarks with the restricted grammar. To run a subset of the benchmarks execute the script: ./synthesize-ic.sh The script will require <5 minutes to finish and runs a subset of benchmarks with the restricted and general grammar. The script prints the currently synthesized invertibility conditions and the results from the paper. To change the set of benchmarks follow the instructions in synthesize-ic.sh. Note that the benchmarks are divided into 3 sets for each grammar: * BENCHMARKS_{R,G}_10 ... solved within 10 seconds each * BENCHMARKS_{R,G}_100 ... solved within 100 seconds each * BENCHMARKS_{R,G}_OTHERS ... need > 100 seconds each -------------------------------------------------------------------------------- 3) Verification of invertibility conditions (Section 3.2 - Verifying ICs) -------------------------------------------------------------------------------- The verification of the invertibility conditions requires a considerable amount of time (12980 benchmarks with 4 solvers and a time limit of 1 hour for each solver/benchmark pair - in total it required approx. 275 days of CPU time). Hence, we provide the log files of the cluster run and a script to easily extract the numbers that were used in section 3.2 of the paper. ./compare-results.sh The benchmarks for the verification problems are located in directories benchmarks/benchmarks-verification. Note that Boolector required a different encoding since the competition version of 2017 does not support define-fun in combination with quantified bit-vectors. These benchmarks are located in directory benchmarks/benchmarks-verification/verify-ic-boolector. To re-run a subset of the verification experiment run: ./run-verification.sh This runs the verification benchmarks on all solvers for bit-width 4, which will take approx. 1 minute. The complete benchmark set can be run with ./run-verification.sh -a However, this will take 275 days of CPU time. -------------------------------------------------------------------------------- 4) Source Code -------------------------------------------------------------------------------- The source code of CVC4 relevant to our paper can be found at: https://github.com/CVC4/CVC4/tree/cav18bv The central piece of code for our approach implements the generation of invertibility conditions as class BvInverter: https://github.com/CVC4/CVC4/blob/cav18bv/src/theory/quantifiers/bv_inverter.cpp It is integrated into CVC4's CEGQI framework: https://github.com/CVC4/CVC4/blob/cav18bv/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp