Colibri2 Documentation

Evolution of COLIBRI

While COLIBRI specializes in areas like floating points, bit-vector relations, and integers. The current experimentations in Colibri2 are focused on less specialized areas like quantifiers and shostak theories. So currently Colibri2 is not a replacement of COLIBRI, but it is complementary

Particular reasoning technique

Linear multiplication

The arithmetic theory is mainly focused on linear equations, $x - 2y = -y$ using a Shostak solver or inequation using a simplex. However, it also handles linear equations with multiplications $\frac{x}{y^2}=\frac{1}{y}$ when $y\not=0$, which can be solved similarly to the previous equation.

The solver for linear multiplicative equation, i.e. multiplication and constant rational power, is not directly the same as linear equation with addition. For example $x^2\equiv 2$ does not imply $x \equiv 2^\frac{1}{2}$. Instead of restricting such operations on positive number, the idea is to separate the absolute value from the sign. The previous equation gives two equations $|x^2|=|2|$ and $sgn(x^2)=sgn(2)$, which conclude into $|x| = \sqrt{2}$ and $1=1$. If two equivalence class have the same canonized absolute value and sign, then they are equal. For example $x^2=y^2$ and $0<xy$ implies that $|x|=|y|$ and $1=\operatorname{sgn}(x)\operatorname{sgn}(y)$, so $\operatorname{sgn}(x)=\operatorname{sgn}(y)$, which implies that $x=y$.

$$\operatorname{sgn}(r) = \begin{cases} -1 & r < 0\\ 0 & r = 0\\ 1 & r > 0\\ \end{cases}$$

Unfolding and Folding Definitions

Colibri2 chooses not to turn definitions or recursive definitions into quantification in order to use specific heuristics. The trade-off is based on the interest of opening definitions for adding information, and the drawbacks of having more terms, new decisions (without conflict learning it is a major problem), unfairness (we can open infinitely a recursive definition). The current heuristic is for one function call that doesn’t come from an unfolding:

• in any case wait for functions calls to be registered before unfolding it
• in the first unfolding the decisions can be immediately done
• in the next 5 unfolding the decisions are delayed to last effort
• after 15 unfolding there is no unfolding anymore

The first heuristic is highly dependent on the fact that recursive definition are written with ite, which is registering lazily. The other allows computation (at depth 15) without changing too much the search tree.

Folding is mainly necessary for adding function symbols that can appears in patterns. It is done by matching on the definition of the function. Folding is not attempted if the definition starts with a built-in symbols (like $\lor,\land$$$) because there are hard to match efficiently and completely. After 25 folds in the same branch of the search tree, the folds are delayed to last effort.

Eager Instantiations

Instantiation is often relegated when the ground part of the formula is known to be satisfiable. In Colibri2 it would be during full effort. Instantiating sooner, eagerly, could remove sooner unsatisfiable branch, which is even more important when there is no conflict analysis. However, eager instantiation has been experimented as too costly in some solver. Still in Z3 eager instantiation is reserved at the start for user provided trigger, then promotion/demotion is used to move quantifiers from eager to last effort. Colibri2 use also promotion of useful delayed instantiation to eager instantiation. But we propose also four techniques to improve the use of eager instantiation:

• More efficient incremental e-matching: diminish the cost of finding substitution
  • A criterion to select the instantiation to apply eagerly: avoid adding new terms
  • Substitution modulo equality: avoid creating new terms already equal to existing terms by congruence closure
  • Delaying decisions of eagerly instantiated terms: in order to ensure they are used for propagation and not change the search tree.