Remove the `Record` theory #1095

Halbaroth · 2024-04-19T13:27:50Z

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.

Halbaroth · 2024-10-30T13:47:18Z

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.

Halbaroth · 2024-10-30T14:57:16Z

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.

Halbaroth · 2024-10-30T17:26:43Z

+55-12 on ae-format and the solver is slightly faster :)

Halbaroth · 2024-11-04T14:35:19Z

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.

Halbaroth · 2024-11-12T13:19:56Z

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.

bclement-ocp

Looks good overall, but there are a few things that seem non-obvious to me that I'd like to see explained.

bclement-ocp · 2025-02-04T15:50:36Z

src/lib/reasoners/adt.ml

+      if Compat.List.is_empty c_args then
+        Fmt.pf ppf "%a" DE.Term.Const.print c_name
+      else
+        Fmt.pf ppf "(%a %a)"
+          DE.Term.Const.print c_name
+          Fmt.(box @@ list ~sep:sp @@ pair nop X.print) c_args

    | Select d ->
-      Fmt.pf ppf "%a#!!%a" X.print d.d_arg DE.Term.Const.print d.d_name
-
+      Fmt.pf ppf "(%a %a)" X.print d.d_arg DE.Term.Const.print d.d_name


This looks like it is an AE-style printer rather than an SMT-lib style printer, not sure it should be changed.

It is a debug message, so we can print whatever we want. In my opinion, we should avoid using different formats for debug messaged based on the input format. We could use a similar printer than Dolmen for these debug messages. This modification contradicts with my own opinion (because infix notations are more readable) ;)

bclement-ocp · 2025-02-04T15:54:55Z

src/lib/reasoners/adt.ml

    let { E.f; xs; ty; _ } = E.term_view t in
-    let sx, ctx =
+    let ssx, ctx =


We should call this rev_rs and rs below to denote that they are semantic value -- ssx and xxs are not particularly readable names!

bclement-ocp · 2025-02-04T15:56:34Z

src/lib/reasoners/adt_rel.ml

-           of the `Arith` and `Records` theories. The semantic
-           values `cons` never involves such values. *)
-        assert (Compat.List.is_empty ctx);
+        let r', _ctx = X.make cons in
        let eq = Shostak.L.(view @@ mk_eq r r') in
        Some (eq, E.mk_constr c xs ty)


Suggested change

Some (eq, E.mk_constr c xs ty)

Some (eq, cons)

bclement-ocp · 2025-02-04T15:57:20Z

src/lib/reasoners/adt_rel.ml

-        (* In the current implementation of `X.make`, we produce
-           a nonempty context only for interpreted semantic values
-           of the `Arith` and `Records` theories. The semantic
-           values `cons` never involves such values. *)
-        assert (Compat.List.is_empty ctx);


We can't keep the assertion because now we create side conditions for ADTs (when they are records), but we shold keep a comment to explain why it is OK to ignore these side conditions.

bclement-ocp · 2025-02-04T15:57:48Z

src/lib/reasoners/adt_rel.ml

-    (* In the current implementation of `X.make`, we produce
-       a nonempty context only for interpreted semantic values
-       of the `Arith` and `Records` theories. The semantic
-       values `cons` never involves such values. *)
-    assert (Compat.List.is_empty ctx);


Same as above -- we should keep a comment why it is OK to ignore the second return value of X.make.

I put a link to the issue #1296

bclement-ocp · 2025-02-04T15:58:46Z

src/lib/reasoners/matching.ml

-                 let { E.f = f; xs = xs; ty = ty; _ } = E.term_view t in
-                 if Symbols.compare f_pat f = 0 then xs::l
-                 else
-                   begin
-                     match f_pat, ty with
-                     | Symbols.Op (Symbols.Record), Ty.Trecord record ->
-                       (xs_modulo_records t record) :: l
-                     | _ -> l
-                   end


Why is this not needed for records as ADTs?

I previously explained in this PR why this piece of code is no longer necessary. I forgot about it too and investigated it again! I'm copying my explanation here with additional details:

The specific code in Matching is there to handle a corner case of the Record theory. For instance, consider the input file:

(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 on this branch. On next, Alt-Ergo needs to match x with (c y), as it is the pattern of the first axiom. We need to match modulo equality. But it does not know that x = (c (b x)). This equation is only generated for record construction terms and x is a variable. The function xs_modulo_records adds the term (c (b x)) into the class of 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 above test succeeds. 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 type, 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.

bclement-ocp · 2025-02-04T16:00:36Z

src/lib/structures/ty.ml

-  name : DE.ty_cst;
-  mutable lbs :  (DE.term_cst * t) list;
-  record_constr : DE.term_cst;
-  (* for ADTs that become records. default is "{" *)


Can't say I am sad to see this one go.

bclement-ocp · 2025-02-04T16:02:50Z

tools/gentest.ml

+              | "tableaux" ->
+                {acc with filters = Some ["tableaux"]}


I seem to remember the difference between Tableaux and CDCL went away when adding the field equations to the context — is it not the case?

If not, a comment should be added to the test to explain why it is failing with CDCL.

Good catch. It is a regression. The test:

(set-logic ALL)the (declare-datatype t ((B (i Int)))) (declare-const e t) (assert ((_ is B) e)) (assert (forall ((n Int)) (distinct e (B n)))) (check-sat)

succeeds on next but fails on this branch. Note that this input file is very closed to issue #1295 but (assert ((_ is B) e) is a ground constraint on e. Currently, this branch manages to discover the equality e = (B .k) for a fresh integer .k but the new term (B .k) never reaches the matching environment. More precisely, the new term is discarded here:

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

Lines 1084 to 1099 in 837293e

try

(*let full_model = nb_assigns() = nb_vars () in*)

(* XXX what to do with the other results of Th.assume ? *)

let t,_,cpt =

Th.assume ~ordered:false

(List.rev facts) env.unit_tenv

in

Steps.incr (Steps.Th_assumed cpt);

env.unit_tenv <- t;

C_none

with Ex.Inconsistent (dep, _terms) ->

(* XXX what to do with terms ? *)

(* Printer.print_dbg

"th inconsistent : %a @." Ex.print dep; *)

if Options.get_profiling() then Profiling.theory_conflict();

C_theory dep

In tableaux, all the new terms generated by relations are sent to the matching environment.
Actually, I tried to fix this issue months ago. See cca3280. The benchmark was pretty bad (+25-195 after correction).

The test is still ignored on CDCL but I put a link to the issue #1262

bclement-ocp · 2025-02-04T16:05:11Z

src/lib/reasoners/adt.ml

+      let ctx =
+        match cases with
+        | [{ destrs; _ }] ->
+          List.fold_left2
+            (fun ctx x (d, d_ty) ->
+               let access = E.mk_term (Sy.destruct d) [t] d_ty in
+               E.mk_eq ~iff:false x access :: ctx
+            ) ctx xs destrs
+        | _ -> ctx
+      in


Can you add a comment explaining what we are doing here?

As we load by default prelude with plenty of axioms, we got a lot of messages about these axioms in the debugging printers of `Matching`. This commit changes this behavior. We only print messages if there is at least one candidate.

Currently, the test `record.smt2` of the issue 1008 only succeeds with the Tableaux SAT solver

The function `xs_modulo_records` is not useful anymore. Indeed, all the ADT variables are sent to the ADT relation thanks to the `init` function of `Uf`. As record type has only one constructor by definition, this will always replace a record variable by a record definition in the union find and we can match patterns of the form `{ lbl1 = ..; ...; lblk = ..}`.

This reverts commit 31c4c66.

This reverts commit 874ea98.

This reverts commit 4fb7fff.

Halbaroth added the clean-up label Apr 19, 2024

Halbaroth added this to the 2.7.0 milestone Apr 19, 2024

Halbaroth force-pushed the merge-records branch from bbb4feb to c9661b1 Compare May 18, 2024 21:37

Halbaroth changed the title ~~Merge records~~ Merge Records theory into ADT theory Jun 11, 2024

Halbaroth mentioned this pull request Jun 17, 2024

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

Open

Halbaroth force-pushed the merge-records branch 2 times, most recently from 0e0a6a1 to 3ba843d Compare July 9, 2024 13:35

Halbaroth force-pushed the merge-records branch from 3ba843d to 4c0477e Compare July 18, 2024 09:39

Halbaroth force-pushed the merge-records branch 2 times, most recently from 117dfe2 to 1d30760 Compare August 6, 2024 08:57

Halbaroth linked an issue Aug 16, 2024 that may be closed by this pull request

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

Open

Halbaroth force-pushed the merge-records branch from 1d30760 to 4ac01de Compare October 22, 2024 15:07

Halbaroth mentioned this pull request Oct 23, 2024

Propagate fresh terms of Relations to the instantiation engine in SatML #1262

Open

Halbaroth force-pushed the merge-records branch from 2e54e7a to 79099b0 Compare October 28, 2024 12:24

Halbaroth removed a link to an issue Oct 28, 2024

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

Open

Halbaroth changed the title ~~Merge Records theory into ADT theory~~ Remove the Record theory Oct 28, 2024

Halbaroth force-pushed the merge-records branch from 75b2d25 to 31c4c66 Compare October 30, 2024 14:43

Halbaroth force-pushed the merge-records branch 2 times, most recently from 7d55bc9 to 20d966c Compare November 12, 2024 13:17

Halbaroth marked this pull request as ready for review November 12, 2024 13:19

Halbaroth requested a review from bclement-ocp November 12, 2024 13:20

Halbaroth force-pushed the merge-records branch from 20d966c to 08f5d40 Compare January 27, 2025 10:23

Halbaroth force-pushed the merge-records branch from 08f5d40 to 16251af Compare February 4, 2025 15:47

bclement-ocp requested changes Feb 4, 2025

View reviewed changes

Merge Records into ADT

531a683

Halbaroth added 13 commits February 13, 2025 11:49

Remove useless flag in adt type

ce0892c

Remove more dead code

0780f7d

Promote tests

25b2223

Do not display 0 candidates messages

dd58ca7

As we load by default prelude with plenty of axioms, we got a lot of messages about these axioms in the debugging printers of `Matching`. This commit changes this behavior. We only print messages if there is at least one candidate.

Add a variant of the issue 1008 test

08cd4f1

Currently, the test `record.smt2` of the issue 1008 only succeeds with the Tableaux SAT solver

Add new tests

fb9be20

Use context of X.make

495adb0

Revert "Use context of X.make"

5047aab

This reverts commit 31c4c66.

Remove test.smt2

bb18a99

clean up

77d06de

Reapply "Use context of X.make"

93b6744

This reverts commit 874ea98.

restore printer

462309d

Halbaroth mentioned this pull request Feb 13, 2025

Incompleteness example for record theory (with quantifiers) #1295

Open

Halbaroth force-pushed the merge-records branch from 16251af to 9628209 Compare February 13, 2025 17:49

Halbaroth added 2 commits February 13, 2025 18:50

Review changes

3ea55cd

Simplify split_domain

19b4816

Halbaroth force-pushed the merge-records branch from 9628209 to 4fb7fff Compare February 13, 2025 22:35

Halbaroth added 4 commits February 13, 2025 23:36

Propagate context in Adt_rel

4fb7fff

Revert "Propagate context in Adt_rel"

08259f1

This reverts commit 4fb7fff.

remove artefact

4895710

Add a link to issue 1262

56d4cb1

Halbaroth mentioned this pull request Feb 14, 2025

Propagate record equations in Adt_rel #1296

Open

Add a link to issue 1296

f94d1b5

Halbaroth requested a review from bclement-ocp February 14, 2025 16:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Remove the `Record` theory #1095

Remove the `Record` theory #1095

Halbaroth commented Apr 19, 2024 •

edited

Loading

Halbaroth commented Oct 30, 2024

Halbaroth commented Oct 30, 2024

Halbaroth commented Oct 30, 2024

Halbaroth commented Nov 4, 2024

Halbaroth commented Nov 12, 2024

bclement-ocp left a comment

bclement-ocp Feb 4, 2025

Halbaroth Feb 4, 2025

bclement-ocp Feb 4, 2025

bclement-ocp Feb 4, 2025

bclement-ocp Feb 4, 2025

bclement-ocp Feb 4, 2025

Halbaroth Feb 14, 2025

bclement-ocp Feb 4, 2025

Halbaroth Feb 13, 2025 •

edited

Loading

bclement-ocp Feb 4, 2025

bclement-ocp Feb 4, 2025

Halbaroth Feb 13, 2025 •

edited

Loading

Halbaroth Feb 14, 2025

bclement-ocp Feb 4, 2025

	try
	(let full_model = nb_assigns() = nb_vars () in)
	(* XXX what to do with the other results of Th.assume ? *)
	let t,_,cpt =
	Th.assume ~ordered:false
	(List.rev facts) env.unit_tenv
	in
	Steps.incr (Steps.Th_assumed cpt);
	env.unit_tenv <- t;
	C_none
	with Ex.Inconsistent (dep, _terms) ->
	(* XXX what to do with terms ? *)
	(* Printer.print_dbg
	"th inconsistent : %a @." Ex.print dep; *)
	if Options.get_profiling() then Profiling.theory_conflict();
	C_theory dep

Remove the Record theory #1095

Are you sure you want to change the base?

Remove the Record theory #1095

Conversation

Halbaroth commented Apr 19, 2024 • edited Loading

Halbaroth commented Oct 30, 2024

Halbaroth commented Oct 30, 2024

Halbaroth commented Oct 30, 2024

Halbaroth commented Nov 4, 2024

Halbaroth commented Nov 12, 2024

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Feb 13, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Feb 13, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Remove the `Record` theory #1095

Remove the `Record` theory #1095

Halbaroth commented Apr 19, 2024 •

edited

Loading

Halbaroth Feb 13, 2025 •

edited

Loading

Halbaroth Feb 13, 2025 •

edited

Loading