---
# Invertibility Conditions for Floating-Point Formulas


Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds,
Clark Barrett and Cesare Tinelli

---

### IMPORTANT NOTICE:

The original submission was anonymized for reviewing purposes (we used a generic
tool name for our SMT solver CVC4). Further, some of the numbers in Section 5
needed updating due to inconsistent use of solver versions for Z3.

Find an updated version of the paper [CAV19-submission-132.pdf](CAV19-submission-132.pdf)
in the top-level directory of the artifact.

---


First Step: Setup Artifact
--------------------------------------------------------------------------------

To setup the artifact execute:

```
./setup-directories.sh
```


Structure of the Artifact:
--------------------------------------------------------------------------------

### Directories:

* **eval-sec5/**
  - `benchmarks/`
    - `FP/`
        Contains all benchmarks from the quantified floating-point (FP) logic
        of SMT-LIB.  These are the benchmarks that we used in our evaluation
        in Section 5.
        able 4 within 5 seconds.

    - `FP-25/`
        Contains a subset of 25 benchmarks from directory FP that finishes
        in a reasonable amount of time (5-7 minutes).  Will be run with
        ./run-experiments.sh.  All benchmarks of this set can be solved by
        all solvers in the evaluation of Section 5 within 60s.

  - `results-eval/`  
      Contains the original log files of CVC4-base, CVC4-ext and Z3 runs of the
      evaluation paragraph in Section 5.

  - `run-experiments.sh`  
    Script to print and re-run the experiments from Section 5.

  - `benchmark-set-FP-25` and `benchmark-set-FP-all`  
    These files define benchmark sets for run-experiments.sh.

* **scripts/**  
    Contains helper scripts.

* **solvers/**  
    Contains all solver versions that were used for our experiments.
    - CVC4-base/bin/run:
        Configuration CVC4-base in Section 5.

    - CVC4-ext/bin/run:
        Configuration CVC4-ext in Section 5.

    - Z3/bin/starexec_run_default:
        Configuration Z3 in Section 5.

* **synthesis/**  
  See [synthesis/README.md](synthesis/README.md).

* **verifiction/**  
  See [verification/README.md](verification/README.md).

### Files:

* [**CAV19-submission-132.pdf**](CAV19-submission-132.pdf)  
  The updated version of our paper.

* **generate-plots.sh**  
  Script to generate the plots from Figures 1-4.

* **run_gen_ic**
  The main script used for synthesizing invertibility conditions.
  See [synthesis/README.md](synthesis/README.md) for more details.


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) Regenerate plots in Figures 1-4
--------------------------------------------------------------------------------

  To generate the plots in Figures 1-4, execute the script:

  ```
  ./generate-plots.sh
  ```

  This script creates a directory `plots` with .jpg files named corresponding
  to the placement in the figures:

  ```
  plots/fig1a.jpg     # Figure 1 a)
  plots/fig1b.jpg     # Figure 1 b)
  plots/fig1c.jpg     # Figure 1 c)
  plots/fig1d.jpg     # Figure 1 d)
  plots/fig2a.jpg     # Figure 2 a)
  plots/fig2b.jpg     # Figure 2 b)
  plots/fig3a.jpg     # Figure 3 a)
  plots/fig3b.jpg     # Figure 3 b)
  plots/fig3c.jpg     # Figure 3 c)
  plots/fig3d.jpg     # Figure 3 d)
  plots/fig4a.jpg     # Figure 4 a)
  plots/fig4b.jpg     # Figure 4 b)
  plots/fig4c.jpg     # Figure 4 c)
  plots/fig4d.jpg     # Figure 4 d)
  ```

  Use `for f in plots/*.jpg; do echo $f; eog $f; done` to loop through
  the plots for comparison with the paper.


2) Synthesis of FP Invertibility Conditions (Section 4)
--------------------------------------------------------------------------------

  See [synthesis/README.md](synthesis/README.md).


3) Verification of Invertibility Conditions (Section 4.1)
--------------------------------------------------------------------------------

  See [verification/README.md](synthesis/README.md).


4) Evaluation of Prototype Extension of CVC4 with FP QE (Section 5)
--------------------------------------------------------------------------------

  To run a subset of the benchmarks from the evaluation, enter directory
  `eval-sec5` and execute the script:

  ```
  ./run-experiments.sh
  ```

  This script will first reproduce the results from the provided log files.
  It will then run all configurations on a subset of 25 benchmarks from set FP
  and compare the results against the provided log files.

  Running all configurations on these 35 benchmarks will take 5-7 minutes.

  The complete benchmark set can be run with

  ```
  ./run-experiments.sh -a
  ```

  Running the complete benchmark set with all configurations will take approx.
  1 day of CPU time.

  Single benchmarks can be run as follows:

  ```
  ../scripts/runlim --time-limit=1800 --space-limit=8000 ../solvers/CVC4-base/bin/run benchmarks/FP/20170501-Heizmann-UltimateAutomizer/<benchmark>
  ../scripts/runlim --time-limit=1800 --space-limit=8000 ../solvers/CVC4-ext/bin/run benchmarks/FP/20170501-Heizmann-UltimateAutomizer/<benchmark>
  ../scripts/runlim --time-limit=1800 --space-limit=8000 ../solvers/Z3/bin/run benchmarks/FP/20170501-Heizmann-UltimateAutomizer/<benchmark>

  ```

5) Source Code
--------------------------------------------------------------------------------

  The source code of CVC4 relevant to Section 5 of our paper can be found at:
  https://github.com/CVC4/CVC4/tree/cav19fp

  The central piece of code for this section is the preprocessing pass
  implemented in
  https://github.com/CVC4/CVC4/blob/9b5acd74b7280c30b56b2bba676a1c39c6db778e/src/preprocessing/passes/fp_ic_pass.cpp