Chrobelias - Chrobak normal form-based Exponential Linear Integer Arithmetic Solver

ChrobELIAS is an smt-solver for the existential Exponential-Linear Integer Arithmetic with regular constraints $\langle\mathbb{N}; 0, 1, +, x\mapsto 2^x, \mathscr{R}, =,\leq\rangle$. The solver implements the decision procedure for existential generalised Semёnov arithmetic from Quantifier Elimination for Regular Integer Linear-Exponential Programming, where Chrobak Normal Form of sub-NFAs is used to linearise exponential occurrences of the variables.

Building

To build the project you need the following dependencies to be installed:

• OPam - OCaml package manager.
• OCaml >5.0.

The dependencies can be installed using the bash commands

# Installing OCaml package manager and OCaml 5.2.
bash -c "sh <(curl -fsSL https://opam.ocaml.org/install.sh)"
opam switch create 5.2.0+flambda --packages=ocaml-variants.5.2.0+options,ocaml-option-flambda --yes

ChrobELIAS is built as follows:

# Installing project dependencies.
opam install . --deps-only --with-test

# Building the project and its tests.
opam exec -- dune build @check @all

The executable binary is available in the _build dir.

Usage

Supports .smt2 files with

• QF_LIA extended with the binary exp function exponentiation. Use (set-logic ALL) for files with exponentiation.
• QF_SLIA subclass corresponding to the logic $T_{\mathit{REln}}$ from Semënov Arithmetic, Affine VASS, and String Constraints.

./_build/default/bin/chro.exe <path-to-smt2-file>

Simple .smt2 files for ChrobELIAS can be found in benchmarks and examples.

Examples

• sat problem from TPDB_ITS_Termination

./_build/default/bin/chro.exe benchmarks/QF_LIA/LoAT/TPDB_ITS_Termination/PastaC1.jar-obl-8.smt2_9.smt2

• unsat problem $x\in\mathtt{16}\cdot(\mathtt{000}\cup\mathtt{999})^{\ast}\land y\in\mathtt{9}\cdot(\mathtt{9})^{\ast}\land |x| =$ to_int $(y) + 1$

./_build/default/bin/chro.exe examples/lnr-unsat.smt2

• sat problem $x\in\mathtt{16}\cdot(\mathtt{000}\cup\mathtt{999})^{\ast}\land y\in\mathtt{9}\cdot(\mathtt{9})^{\ast}\land 9|x| =$ to_int $(y)$

./_build/default/bin/chro.exe examples/lnr-sat.smt2

Publications

• M. R. Starchak. Quantifier Elimination for Regular Integer Linear-Exponential Programming, In Proc. of LICS'25, Singapore, 2025, pp. 44-56.

Acknowledgements

We use custom SMT-lib v2.6 exp syntax and examples from SwInE by Florian Frohn licensed under LGPL v2.1.

Benchmarks

# Clone benchmarks
git submodule update --init

# Generate dune files with benchmarks (example: will generate benchmarks in `benchmarks/tests/QF_LIA/LoAT/TPDP_ITS_Complexity`
# See the root `Makefile` with other commands)
make genTPDB_ITS_Complexity

# Autopromote benchmarks (example)
make -C  benchmarks/tests/QF_LIA/LoAT/TPDB_ITS_Complexity

# Run a single benchmark. The output is located in `benchmarks/tests/QF_LIA/LoAT/TPDB_ITS_Complexity/a.03.koat_0.t`
dune b @benchmarks/tests/QF_LIA/LoAT/TPDB_ITS_Complexity/a.03.koat_0 --profile=benchmark