HighDiv is a bidirectionally guided iterative sampling framework that combines CDCL(T) and local search to enable high-diversity sampling for SMT(LIA) formulas. This repository contains the implementation of HighDiv, the benchmark instances used in the experiments, and the corresponding experimental results.
The instructions of seting up HighDiv and validate its general functionality are described in the INSTALL.md file.
After building HighDiv, users may run it with the following command:
./HighDiv -i [INSTANCE_PATH] -o [OUTPUT_TESTCASE_PATH] -n [NUMBER_OF_SAMPLES] -t [TIME_LIMIT] -s [RANDOM SEED] -l [HIGH_FREQUENCY_THRESHOLD]For the required parameters, we list them as follows.
| Parameter | Allowed Values | Description |
|---|---|---|
-i |
String | Path to the input SMT instance |
-o |
String | Path to the output solutions generated by HighDiv |
As mentioned above, -i is one of the required parameter and the input file for HighDiv must be in SMTLIB2. The directory named LIA_bench contains 7 testing instances, which can be taken as input.
For the optional parameters, we list them as follows.
| Parameter | Allowed Values | Default Value | Description |
|---|---|---|---|
-s |
Integer | 0 | Random seed |
-n |
Positive integer | 1000 | Required Number of Samples |
-l |
Positive integer | 50 | High-frequency variable threshold |
-t |
Float (in seconds) | 900 | Time limit |
./HighDiv -i LIA_bench/LIA_Bromberger_CAV_2009_30-vars_problem__026.smt2.slack.smt2 -o samplesThe HighDiv/src/ directory contains the core implementation and structural overview of HighDiv, while z3/src/sampler/ contains the implementation of Context-Constrained Stochastic Search (CCSS).
The directory named benchmarks/ contains all 345 instances.
The directory results/ contains 3 sub-directories for presenting the experimental results.