incomplete detection of EPR axioms

[damien-zufferey-sonarsource]

Hi @jhoenicke,

while playing around with SMTInterpol and quantifiers, I found the following funny example:

(set-logic UF)
(declare-sort Unit 0)
(assert (forall ((u0 Unit) (u1 Unit)) (= u0 u1)))
(declare-fun x () Unit)
(declare-fun y () Unit)
(assert (distinct x y))
(check-sat)
(exit)

I expected SMTInerpol to return unsat. However, it returns unknown. Unless I'm mistaken, that should be an EPR formula (variables occurring only below relations). So SMTInterpol should be complete there.

Looking at the solver's output, it complains that:

INFO - Quant: Clause contains literal that is not almost uninterpreted: (= .u0.0 .u1.1)

If you don't have the time to take a look, I can give it a shot. But I'll need your help to confirm my analysis. My best guess is that there is a case missing in getQuantEquality.

[jhoenicke]

By default the EPR solver is not enabled. You can enable it with (set-option :epr true). I'm not sure, if it is still working after the changes done for the default quantifier procedure. I tried your example and it returns sat instead of unsat, so this seems to be buggy.

The default quantifier theory is based on the almost uninterpreted fragment, which doesn't support positive equalities between variables (negated equalities can be eliminated with DER).

[damien-zufferey-sonarsource]

I'm kind of getting confused. The almost uninterpreted fragment (AUF) is supposed to be an extension of EPR. At least the paper claims that.

Independently of that, Section 4.1 of the paper discusses equality with uninterpreted sorts. This should cover the example. The gist is that equality with uninterpreted sorts can be axiomatized within AUF. However, as solvers understand equality we can rely on that.

For fun, here is a version with the axiomatization

(set-logic UF)
(declare-sort Unit 0)
(declare-fun x () Unit)
(declare-fun y () Unit)
; axiomatization of equality as an equivalence relation
(declare-fun equiv (Unit Unit) Bool)
(assert (forall ((u0 Unit)) (equiv u0 u0)))
(assert (forall ((u0 Unit) (u1 Unit)) (=> (equiv u0 u1) (equiv u1 u0))))
(assert (forall ((u0 Unit) (u1 Unit) (u2 Unit)) (=> (and (equiv u0 u1) (equiv u1 u2)) (equiv u0 u2))))
; declare a congruence closure axiom to check it is almost uninterpreted
(declare-sort S 0)
(declare-fun f (Unit) S)
(assert (forall ((u0 Unit) (u1 Unit)) (=> (equiv u0 u1) (= (f u0) (f u1)))))
; now the constraints
(assert (forall ((u0 Unit) (u1 Unit)) (equiv u0 u1)))
(assert (not (equiv x y)))
(check-sat)
(exit)

SMTInterpol works fine on it.

[jhoenicke]

I'm not completely sure what the answer is here. The models we want to use for the almost uninterpreted fragment would not work, if we allow equalities between quantified variables. E.g., you can encode injectivity: forall x,y. (f(x) != f(y) \/ x= y).

Now if a function is injective and monotone, it is strict monotone. If the function is over integer then the additional constraint f(n) - f(m) < n - m /\ n > m would yield a contradiction, that wouldn't be even possible to derive with instantiation.

You can axiomatise an equiv predicate as you did in your second example, but we would compute a model where equiv is not equality, e.g. it would be true for almost all pairs of integer. But for uninterpreted sorts it may work.

[damien-zufferey-sonarsource]

Very good point. I need some time (and some spare cycles) to think about this. I'll let you know if I have some idea about that.