The distinct expression clashes with the SMT-LIB specification

[Halbaroth]

The current implementation of the distinct expression in the module Expr clashes with the SMT-LIB specification.

In Alt-Ergo, the expression mk_distinct [x_1; ...; x_n] means:

x_1 <> x2 and x2 <> x3 and ... x_(n-1) <> x_n

but the expected implementation is:

forall 1 <= i < j <= n, x_i <> x_j

This disagreement induces a soundness bug. For instance with the input file:

(set-logic ALL)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (not (distinct a b c)))
(assert (distinct a b))
(check-sat)

we got unsat with AE but sat with other solvers.

[Halbaroth]

A hot fix have been merged on the branch v2.5.x for the release v2.5.2, see #890.

[Halbaroth]

After some offline discussions, it seems that solving the issue is not a priority for the next release as we don't expect to see valuable performance improvements because of the current implementation. The difficulty comes from the fact that the negation of distinct expressions are in fact clauses. Let's imagine we have the literal distinct x y z. After discovering this literal is inconsistent in the current context, we have to propagate its negation x = y \/ x = z \/ y = z to the union-find environment. But there is no adequate operation to perform on the union-find for this propagation. It means we have to decide some literal of this clause in the SAT solver.

We have a solution to solve this. Basically, if the SAT solver discovers that a decision on distinct x y z is inconsistent, while deciding not (distinct x y z), we add to the context the formula:

(distinct x y z) \/ x = y \/ x = z \/ y = z

This formula is a tautology. Thus, if we forgot to add it at all the backtracking locations in the code, our solver is still sound. Now, as we have not (distinct x y z) in the context, we got also x = y \/ x = z \/ y = z and the SAT solver can decide some literal of this clause. In CC(X), we ignore completely not (distinct) of at least three elements, as the expanded version in the SAT solver will propagate the appropriate equality in the current branch.

This solution is complex. For the release v2.6, we plan to clean up the codebase by removing completely the distinct literal in Expr dans Xliteral. We only keep a smart constructor for distinct which represents this formula by a disjunction.

[bclement-ocp]

This is no longer a soundness bug since we explode distinct for now. Opened #1157 to track work on re-instating native support for distinct.