Simple ADT test with different behavior with or without push

[Stevendeo]

The following test have a different behavior given if the push instruction is here or not:

File test_adt.smt2

(set-logic ALL)
(declare-datatype t ((A) (B) (C (i Int))))

(declare-const e t)

(push 1)
(assert (not ((_ is A) e)))
(assert (not ((_ is B) e)))
(assert (not (exists ((n Int)) (= e (C n)))))
(check-sat)

Command:
alt-ergo test_adt.smt2 --enable-assertions --output smtlib2 --sat-solver CDCL --no-minimal-bj

Without the push, alt-ergo returns unsat (as expected); with the push, it never returns.

The culplrit may be the presence of the existential quantifier and --no-minimal-bj; remove the option and everything works fine. This test is a translation of goal g_valid_5_1 of tests/adts/simple_1.ae.

[bclement-ocp]

The following test have a different behavior given if the push instruction is here or not:

Can you clarify what behavior is different and if either behavior is incorrect/unsound?

[Stevendeo]

Oh you're right I forgot about it: with the push it does not return, while without it returns unsat (as expected). So it's not an unsoundness issue.

[bclement-ocp]

Interesting. I actually don't understand how we prove this in the first place…

Here is a simpler example that we are able to prove:

(set-logic ALL)
(declare-datatype t ((A) (B (i Int))))

(declare-const e t)

(assert ((_ is B) e))
(assert (forall ((n Int)) (distinct e (B n))))
(check-sat)

Here is an even simpler example that we are not able to prove anymore, because the type gets converted to a record:

(set-logic ALL)
(declare-datatype t ((B (i Int))))

(declare-const e t)

(assert ((_ is B) e))
(assert (forall ((n Int)) (distinct e (B n))))
(check-sat)

So the ADT theory must be doing something weird… Pinging @Halbaroth who has been looking at ADTs.

[Halbaroth]

I believe there is no soundness bug here. For instance, for the following input file:

(set-logic ALL)
(declare-datatype t ((A) (B (i Int))))

(declare-const e t)

(assert ((_ is B) e))
(assert (forall ((n Int)) (distinct e (B n))))
(check-sat)

Alt-Ergo reaches a contradiction as folllows:

1. After asserting ((_ is B) e), Alt-Ergo notices that the domain of e is a singleton and so Adt_rel asserts an equation of the form (= (e (B .k0)) where .k0 denotes a fresh integer name. The associated explanation is empty because the equation is asserted by the user.
2. The instantiation engines matches (B .k0) with the unique trigger (B n) of the axiom (forall ((n Int)) (distinct e (B n))).
3. The SAT solver learns (distinct e (B .k0)), we got a contradiction!

Now, if we consider the input:

(set-logic ALL)
(declare-datatype t ((B (i Int))))

(declare-const e t)

(assert ((_ is B) e))
(assert (forall ((n Int)) (distinct e (B n))))
(check-sat)

The type t is a record and (_ is B) e is immediately replaced by true in D_cnf. The current implementation of Matching cannot match e with (B n) because the union-find ignores the equality e = (B (i e)).

There are several solutions:

1. Do nothing as the issue will be solved after merging Merge Records theory into ADT theory #1095.
2. Using Record_rel to generate a definition of e of the form (B .k0) as we do in Adt_rel and use Rel.new_terms to send these terms to the matching module.
3. Allow to match e with (B (i e)) in the matching module.

The last solution is probably the best one because we avoid to add fresh terms for each field of a record.

In the current state of the code, we do not reach a contradiction with the second example, even if we turn on the model generation, because the generated terms by Uf.next_assign are not sent to the matching module:

alt-ergo/src/lib/reasoners/satml.ml

Lines 918 to 926 in 85308d4

	let do_case_split env origin =
	try
	let acts = theory_slice env in
	let tenv, _terms = Th.do_case_split ~acts env.tenv origin in
	(* TODO: terms not added to matching !!! *)
	env.tenv <- tenv;
	C_none
	with Ex.Inconsistent (expl, _) ->
	C_theory expl

I am not sure it is a good idea to add these terms to the matching environment for two reasons:

1. We want to match e with (B (i e)) before reaching the model generation phase
2. While implementing get-value in Support get-value statement #1032, I didn't find new contradiction by asserting all the model and restart all the solver on this new problem. I believe that it means we don't find a lot of new contradiction by performing extra matching rounds during the model generation.

[Halbaroth]

Finally, I think that the best solution is to solve this issue by merging #1095 after v2.6.0. I add a test #1211 and this issue will be closed after merging #1095.