OCamlPro
Remove the `Record` theory
This PR removes the Record theory and sends all the records to the ADT theory.
This modification does not fix #1008 as expected because SatML does not send some terms generated by Adt_rel to the instantiation engine.
As I expected, we got regressions if we do not produce a context in the make function of Adt as we did in Records. Consider for instance this example (I got it from a real regression):
(set-logic ALL)
(declare-datatype unit ((void)))
(declare-datatype t ((box (unbox unit))))
(declare-fun f (t t) Bool)
(assert (forall ((u t) (v t)) (f u (box (unbox v)))))
(assert (not (f (box void) (box void))))
(check-sat)
We expect that Alt-Ergo outputs unsat. It works on next because X.make adds the extra equality (unbox (box void)) = void. The trigger of the first assertion is (f u (box (unbox v))). First, we match (box void) with (box (unbox v)), then we try to match (unbox v) with void. Of course, we cannot match them if we only consider syntactical equality, but Matching allows to match terms modulo equality of the union-find. (unbox (box void)) is in the class of void and can match (unbox v) with v --> (box void).
If you modify the input file as follows:
(set-logic ALL)
(declare-datatype unit ((void)))
(declare-datatype t ((box (unbox unit))))
(declare-fun f (t) Bool)
(assert (forall ((v t)) (f (box (unbox v)))))
(assert (not (f (box void))))
(check-sat)
Alt-Ergo outputs unsat on next and this branch. It succeeds because after many matching rounds, it will try with variable triggers and there is one variable trigger v which covers all the variables of the axiom. In the previous case, it won't generate it because of u. So the instantiation engine produces a fresh instantiation with v = void.
Notice that there is specific code in Matching to manage another corner case of the Records theory. For instance, consider the input:
(set-logic ALL)
(declare-datatype t ((c (b Bool))))
(declare-fun f (t) Bool)
(declare-const x t)
(assert (forall ((y Bool)) (f (c y))))
(assert (not (f x)))
(check-sat)
Alt-Ergo outputs unsat on next and this branch. On next, Alt-Ergo need to match x with (c y) (it is the pattern of the axiom). Again, we need to match modulo equality. But it does not know that x = (c (b x)). The function xs_modulo_records in the module Matching will add the term (c (b x)) to the list of terms equal to x and Alt-Ergo produces the right instance.
I removed this code in the present branch and did not write anything to replace it but still the test passes. It works for a good reason! First of all, the ADT x is sent to Adt_rel thanks to the new function init in Uf.
Since t is a record, we immediately obtain a domain of size 1 for x and we produce a fresh boolean term k and the equality x = (c k). Of course (c k) is the new representative element and we can match it against the pattern of the axiom.
In the last patch, I use the context of Adt.make to propagate the same equalities as we did in Records.make. Actually I produce these equalities as soon as the type of the term is an ADT with only one constructor, which is bit more general.
I am running benchmarks to check if this patch removes most of the regressions. Even if it does, I would prefer a solution without using the context of X.make.
Okay, I was not completely satisfied by the last commit. It is sad to still use the context of X.make.
Another way to solve this issue consists in eliminating as earlier as possible terms of the form (box ... (unbox u) ...) where box is the unique constructor of a record type and unbox is one of its destructor (at the appropriate position). Let us imagine that we have the axiom:
forall u : t. (P u (box (unbox u)))
where P is a undefined predicate and t is our record type.
If we replace it by:
forall w : unit. u = box w --> (P u u)
Alt-Ergo should generate the trigger (P u u) for this axiom. If we have the term (box unit) in the union-find, we can match (P (box unit) (box unit)) against (P u u) with u --> (box unit) and we can take w --> unit. We do not need to add the equality (unbox (box unit)) = unit.
Actually, I tried another transformation:
forall w : unit.
let u = box w in
(P u u)
It works if we disable some simplifications done in the smart constructor Expr.mk_let and during triggers generation but we lost other problems.
I think that this PR is now ready to review. I keep the current code with context in X.make even if I dislike this design because I didn't find a proper approach and I think we should merge this PR and look for a better design later.
I am really uneasy about losing such simple proofs as the 1008 example — we really should figure out a way to send those terms back to matching.
I can work on it this week, no rush to merge this PR.
Ok, this PR is quite old... I thought 1008/record.smt2 was a regression but it wasn't! Before this PR, we cannot prove the test with both Tableaux and CDCL. After this PR, we can prove it with Tableaux. The test have been introduced in this PR https://github.com/OCamlPro/alt-ergo/pull/1211 and you suggested to add it in the issue https://github.com/OCamlPro/alt-ergo/issues/1008. In #1008, you noticed that we are able to solve:
(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)
which means that the issue with 1008/record.smt2 is not related with #1262 as I thought. I remove the link to #1262 and merge this PR as it does not introduce regressions.