===============================================================================
A Decision Procedure for String to Code Point Conversion
===============================================================================
Andrew Reynolds, Andres Noetzli, Clark Barrett, Cesare Tinelli

# Introduction

This is the artifact for our IJCAR 20 submission "A Decision Procedure for
String to Code Point Conversion." The artifact contains copies of the
benchmarks, solvers, and scripts used to generate the table and the scatter
plot in the paper.

# Structure

- `benchmarks/full_str_int/`: The benchmarks used in our evaluation
- `csv/results.csv`: CSV with the results, used to generate the table and plot
- `logs/`: The logs of the runs that we did for the evaluation
- `results/`: The table and plot generated by this artifact
- `solvers/`: Copies of the solvers used in our evaluation (CVC4, Z3, Z3-Trau)
- `src/`: Source code of the CVC4 implementation used in the evaluation
- `utils/`: Scripts used to generate the CSV, table, and plot

# Solvers

We used the binaries in the `solvers/` folder in our evaluation:

- `solvers/cvc4`: This is the compiled version of CVC4 used in the evaluation.
  It is compiled from the following branch (and the same as the source code
  that we provide in `src/`):
  https://github.com/4tXJ7f/CVC4/tree/ijcar2020 (commit 7abcfca1).
- `solvers/z3-4.8.7-x64-ubuntu-16.04/bin/z3`: This is pre-compiled release of
  Z3 4.8.7.
- `solvers/z3_trau`: The compiled version of Z3-Trau used in the evaluation. It
  is compiled from the following branch:
  https://github.com/guluchen/z3/tree/new_trau (commit 0d81a92).

We invoked the solvers with the following command line arguments:

- CVC4:
  - cvc4+c:
    `--strings-exp --force-logic=QF_SLIA --no-strings-lazy-pp --produce-models`
  - cvc4:
    `--strings-exp --force-logic=QF_SLIA --no-strings-lazy-pp --produce-models --no-use-code`
- Z3: No additional arguments
- Z3str3 (using the Z3 binary): `smt.string_solver=z3str3`
- Z3-Trau: `smt.string_solver=trau`

# Reproducing the results

The following steps are intended to be executed from the base directory of this
artifact.

1. Generate `csv/results.csv` from the logs:
   `$ utils/compare-smt-runs.py --csv --full-path logs/full_str_int300/ logs/full_str_int_nc300/ logs/z3_4.8.7_300/ > csv/results.csv`
2. Generate the table from `csv/results.csv`:
   `$ utils/gen_table.py > results/table.tex`
3. Generate the scatter plot from `csv/results.csv`:
   `$ utils/gen_scatter.py "cvc4" "cvc4+c" results/scatter_d_nc.pdf`

# Discrepancies between solvers

In our evaluation, we report that there were discrepancies between CVC4 and
Z3str3 as well as Z3-Trau.

To get a summary of the discrepancies between CVC4 and Z3str3:
`$ utils/compare-smt-runs.py --dis -G logs/full_str_int300/ logs/z3str3_4.8.7_300/`

To get a summary of the discrepancies between CVC4 and Z3-Trau:
`$ utils/compare-smt-runs.py --dis -G logs/full_str_int300/ logs/z3-trau_300/`

The benchmark that Z3-Trau considers to be satisfiable (but both CVC4 and Z3
consider unsatisfiable) is
`py-conbyte_z3seq/leetcode_int-restoreIpAddresses/111.smt2`.

# Implementation

The source code for the implementation of our approach in CVC4 is provided in
`src/CVC4`. The following files may be of interest:

- `src/theory/strings/theory_strings_preprocess.cpp`: Implementation of the
  reductions mentioned in Section 4.
- `src/theory/strings/theory_strings_rewriter.cpp`
  (`TheoryStringsRewriter::rewriteMembership()`): Implementation of regular
  expression ranges using `code` as discussed in Section 4.
- `src/theory/strings/theory_strings.cpp`
  - `TheoryStrings::checkCodes()`: Implementation of the rules C-Intro,
    C-Collaps, C-Inj
  - `TheoryStrings::registerTerm()`: Implementation of the rule C-Valid
  - `TheoryStrings::collectModelInfo()`: Implementation of the model
    construction algorithm