OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
133 stars 33 forks source link

Simple ADT test with different behavior with or without push #1008

Open Stevendeo opened 10 months ago

Stevendeo commented 10 months ago

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 commented 10 months ago

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 commented 10 months ago

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 commented 10 months ago

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 commented 4 months ago

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 #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: https://github.com/OCamlPro/alt-ergo/blob/85308d4b0759fc5f650583d5229aa139f09c3144/src/lib/reasoners/satml.ml#L918-L926 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 #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 commented 2 months ago

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.