Merge `Enum` theory into `ADT` theory #1094

Halbaroth · 2024-04-13T07:32:23Z

After refactoring both Enum and ADT theories, they shared most of
their implementation.

This PR merges Enum theory into ADT ones.

This PR is rebased on #1093

Halbaroth · 2024-06-11T09:23:36Z

This PR have been tested on our internal benchmarks.

bclement-ocp

Can you please change the name of the PR? "Merge enum" is very obscure; "Merge the enum and ADT theories" or "Merge the enum theory into the ADT theory" would be better.

This PR have been tested on our internal benchmarks.

What are the results of those tests? Is it +0-0?

As far as the code goes, this looks mostly OK to me. Outside of some small suggestions, my main concern is the new boolean flag in the Tadt constructor. I know you did some things to try to get rid of it — can you say a bit more about what other approaches you tried and the issues with them? I want to make sure we don't miss an easy way of not needing this flag.

bclement-ocp · 2024-06-11T10:20:54Z

src/lib/reasoners/adt_rel.ml

+  let is_enum r =
+    match X.type_info r with
+    | Ty.Tadt (_, [], true) -> true
+    | _ -> false


It looks like this is the only place where we care about the new is_enum flag of the Tadt constructor. I understand it is probably here for performance reasons (seeing #1138 and previous offline discussions), but ideally we would like to remove it if possible (I think a time regression is OK for this, but not a number-of-solved-problems regression).

Did you try splitting only if all the current constructors have no payload rather than splitting on any constructor that has no payload?

It's not just a time regression, we lost some problems. As we decided offline, it's better to do a PR for merging Enum into ADT without any regression, then testing better approaches later. My only concern with this extra flag is the fact there is no equivalent flag in Dolmen's types, so we have to get rid of it before switching to these types.

A solution without flag consists in checking if the type is an enum in Adt_rel.Domains. The cost should be acceptable (we could cache the result in a weak cache, but there are too much weak caches in AE in my opinion).

Did you try splitting only if all the current constructors have no payload rather than splitting on any constructor that has no payload?

Not yet, I will try today.

If we want to cache it, I think that this can be easily added to the Ty module that already has a cache (for the definition of a type) — we can add it to Ty.Adt which is better than adding it to Ty.t because it is part of the type definition, not of the type name.

bclement-ocp · 2024-06-11T10:22:59Z

src/lib/reasoners/adt_rel.ml

+let split_enum env uf =
+  let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in
+  let* n, r, c = pick_enum ds uf in
+  let n = Numbers.Q.from_int n in
+  if can_split env n then
+    let _, cons = Option.get @@ build_constr_eq r c in
+    let nr, ctx = X.make cons in
+    (* 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 (Lists.is_empty ctx);
+    Some (LR.mkv_eq r nr)
+  else
+    None


I think there is some duplication with split_best_domain that can be eliminated by defining a make_split n r c function that makes the split, and a pick function that dispatches to either pick_enum or pick_best as appropriate.

bclement-ocp · 2024-06-11T10:26:12Z

src/lib/structures/ty.mli


-  | Tadt of Uid.t * t list
-  (** Application of algebraic data types. [Tadt (a, params)] denotes
+  | Tadt of Uid.t * t list * bool


Unnamed booleans should generally be avoided; if we keep this flag, we should either adt_kind = Adt | Enum and use that instead of bool, use [ Adt | Enum ], or define Tadt with an inline record with an is_enum : bool field.

Sure. I didn't make much effort here as we plan to get rid of the legacy types soon. I will create an extra ADT.

bclement-ocp · 2024-06-11T10:32:02Z

src/lib/frontend/typechecker.ml

+    | Enum l ->
+      let body = List.map (fun constr -> Uid.of_string constr, []) l in
+      let ty = Ty.t_adt ~enum:true ~body:(Some body) (Uid.of_string id) [] in
+      ty, { env with to_ty = MString.add id ty env.to_ty }


Not sure why this was moved; the check for PolymorphicEnum error should be kept (we do bad things when type variables are unused and this is a case where we can catch it).

It's an artifact of the last rebase. I will fix that.

Halbaroth · 2024-06-11T11:50:41Z

What are the results of those tests? Is it +0-0?

It's +0-0 on ae-format, QF_DT and UFDT. In fact, the enum theory is slightly faster after this PR.

Halbaroth · 2024-06-11T12:02:25Z

As far as the code goes, this looks mostly OK to me. Outside of some small suggestions, my main concern is the new boolean flag in the Tadt constructor. I know you did some things to try to get rid of it — can you say a bit more about what other approaches you tried and the issues with them? I want to make sure we don't miss an easy way of not needing this flag.

I only tried one other approach, which is currently in the draft #1138. See the diff between these branches:
Halbaroth/alt-ergo@merge-enum...Halbaroth:alt-ergo:casesplit-enum-cstr

Instead of splitting on enum types only after each assert, I split on domains that contains a constructor without payload. I got 4 regressions (with OCaml 5) and 0 improvements and the enum theory is slower (14m30s before and 15m28s). These tests have been run on next and PR #1138 with only the UFDT test suite.

Halbaroth · 2024-06-11T15:33:12Z

I will test your suggestion in another PR. I think we can merge this one. I removed the extra flag as you wish.

bclement-ocp

This looks cleaner. I'm OK with trying to change the split strategy separately.

bclement-ocp

Temporarily revoking approval to avoid accidental merging since it seems a regression snuck in the benchmarks.

Halbaroth · 2024-06-12T07:05:42Z

There is no regression. I forgot to rebase the PR after merging the fix for #1099. I ran again benchmarks on #1138 with the fix and there is no regression anymore.

After refactoring both `Enum` and `ADT` theories, they shared most of their implementation.

bclement-ocp · 2024-06-12T08:24:47Z

I forgot to rebase the PR after merging the fix for #1099.

Does this mean that it is that fix that introduced regressions?

Halbaroth · 2024-06-12T08:55:02Z

I forgot to rebase the PR after merging the fix for #1099.

Does this mean that it is that fix that introduced regressions?

No. The fix solved regressions introduced with the Dolmen frontend in 2.5.0 and I didn't rebase this PR with it. So next solved new problems.

bclement-ocp · 2024-06-12T08:56:20Z

Ah, I got things backwards — thanks for the clarification.

CHANGES: ### Command-line interface - Enable FPA theory by default (OCamlPro/alt-ergo#1177) - Remove deprecated output channels (OCamlPro/alt-ergo#782) - Deprecate the --use-underscore since it produces models that are not SMT-LIB compliant (OCamlPro/alt-ergo#805) - Add --dump-models-on to dump models on a specific output channel (OCamlPro/alt-ergo#838) - Use consistent return codes (OCamlPro/alt-ergo#842) - Add --continue-on-error flag to set the SMT-LIB error behavior (OCamlPro/alt-ergo#853) - Make dolmen the default value for the --frontend option (OCamlPro/alt-ergo#857) - Restore functionality to broken `--profiling` option (OCamlPro/alt-ergo#947) - Add bare-bones support for interactive input in SMT-LIB format (OCamlPro/alt-ergo#949) - Less confusing behavior on timeout (OCamlPro/alt-ergo#982, OCamlPro/alt-ergo#984) - Add `--strict` option for SMT-LIB compliant mode (OCamlPro/alt-ergo#916, OCamlPro/alt-ergo#1133) - Deprecate `sum`, `typing` and `warnings` debug flags (OCamlPro/alt-ergo#1204) ### SMT-LIB support - Add support for the many new SMT-LIB commands (OCamlPro/alt-ergo#837, OCamlPro/alt-ergo#848, OCamlPro/alt-ergo#852, OCamlPro/alt-ergo#863, OCamlPro/alt-ergo#911, OCamlPro/alt-ergo#942, OCamlPro/alt-ergo#945, OCamlPro/alt-ergo#961, OCamlPro/alt-ergo#975, OCamlPro/alt-ergo#1069) - Expose the FPA rounding builtin in the SMT-LIB format (OCamlPro/alt-ergo#876, OCamlPro/alt-ergo#1135) - Allow changing the SAT solver using (set-option) (OCamlPro/alt-ergo#880) - Add support for the `:named` attribute (OCamlPro/alt-ergo#957) - Add support for quoted identifiers (OCamlPro/alt-ergo#909, OCamlPro/alt-ergo#972) - Add support for naming lemmas in SMT-LIB syntax (OCamlPro/alt-ergo#1141, OCamlPro/alt-ergo#1143) ### Model generation - Use post-solve SAT environment in model generation, fixing issues where incorrect models were generated (OCamlPro/alt-ergo#789) - Restore support for records in models (OCamlPro/alt-ergo#793) - Use abstract values instead of dummy values in models where the actual value does not matter (OCamlPro/alt-ergo#804, OCamlPro/alt-ergo#835) - Use fresh names for all abstract values to prevent accidental captures (OCamlPro/alt-ergo#811) - Add support for model generation with the default CDCL solver (OCamlPro/alt-ergo#829) - Support model generation for the BV theory (OCamlPro/alt-ergo#841, OCamlPro/alt-ergo#968) - Add support for optimization (MaxSMT / OptiSMT) with lexicographic Int and Real objectives (OCamlPro/alt-ergo#861, OCamlPro/alt-ergo#921) - Add a SMT-LIB printer for expressions (OCamlPro/alt-ergo#952, OCamlPro/alt-ergo#981, OCamlPro/alt-ergo#1082, OCamlPro/alt-ergo#931, OCamlPro/alt-ergo#932) - Ensure models have a value for all constants in the problem (OCamlPro/alt-ergo#1019) - Fix a rare soundness issue with integer constraints when model generation is enabled (OCamlPro/alt-ergo#1025) - Support model generation for the ADT theory (OCamlPro/alt-ergo#1093, OCamlPro/alt-ergo#1153) ### Theory reasoning - Add word-level propagators for the BV theory (OCamlPro/alt-ergo#944, OCamlPro/alt-ergo#1004, OCamlPro/alt-ergo#1007, OCamlPro/alt-ergo#1010, OCamlPro/alt-ergo#1011, OCamlPro/alt-ergo#1012, OCamlPro/alt-ergo#1040, OCamlPro/alt-ergo#1044, OCamlPro/alt-ergo#1054, OCamlPro/alt-ergo#1055, OCamlPro/alt-ergo#1056, OCamlPro/alt-ergo#1057, OCamlPro/alt-ergo#1065, OCamlPro/alt-ergo#1073, OCamlPro/alt-ergo#1144, OCamlPro/alt-ergo#1152) - Add interval domains and arithmetic propagators for the BV theory (OCamlPro/alt-ergo#1058, OCamlPro/alt-ergo#1083, OCamlPro/alt-ergo#1084, OCamlPro/alt-ergo#1085) - Native support for bv2nat of bit-vector normal forms (OCamlPro/alt-ergo#1154) - Fix incompleteness issues in the BV solver (OCamlPro/alt-ergo#978, OCamlPro/alt-ergo#979) - Abstract more arguments of AC symbols to avoid infinite loops when they contain other AC symbols (OCamlPro/alt-ergo#990) - Do not make irrelevant decisions in CDCL solver, improving performance slightly (OCamlPro/alt-ergo#1041) - Rewrite the ADT theory to use domains and integrate the enum theory into the ADT theory (OCamlPro/alt-ergo#1078, OCamlPro/alt-ergo#1086, OCamlPro/alt-ergo#1087, OCamlPro/alt-ergo#1091, OCamlPro/alt-ergo#1094, OCamlPro/alt-ergo#1138) - Rewrite the Intervals module entirely (OCamlPro/alt-ergo#1108) - Add maximize/minimize terms for matching (OCamlPro/alt-ergo#1166) - Internalize `sign_extend` and `repeat` (OCamlPro/alt-ergo#1192) - Run cross-propagators to completion (OCamlPro/alt-ergo#1221) - Support binary distinct on arbitrary bit-widths (OCamlPro/alt-ergo#1222) - Only perform optimization when building a model (OCamlPro/alt-ergo#1224) - Make sure domains do not overflow the default domain (OCamlPro/alt-ergo#1225) - Do not build unnormalized values in `zero_extend` (OCamlPro/alt-ergo#1226) ### Internal/library changes - Rewrite the Vec module (OCamlPro/alt-ergo#607) - Move printer definitions closer to type definitions (OCamlPro/alt-ergo#808) - Mark proxy names as reserved (OCamlPro/alt-ergo#836) - Use a Zarith-based representation for numbers and bit-vectors (OCamlPro/alt-ergo#850, OCamlPro/alt-ergo#943) - Add native support for (bvnot) in the BV solver (OCamlPro/alt-ergo#856) - Add constant propagators for partially interpreted functions (OCamlPro/alt-ergo#869) - Remove `Util.failwith` in favor of `Fmt.failwith` (OCamlPro/alt-ergo#872) - Add more `Expr` smart constructors (OCamlPro/alt-ergo#877, OCamlPro/alt-ergo#878) - Do not use existential variables for integer division (OCamlPro/alt-ergo#881) - Preserve `Subst` literals to prevent accidental incompleteness (OCamlPro/alt-ergo#886) - Properly start timers (OCamlPro/alt-ergo#924) - Compute a concrete representation of a model instead of performing (OCamlPro/alt-ergo#925) - Allow direct access to the SAT API in the Alt-Ergo library computations during printing (OCamlPro/alt-ergo#927) - Better handling for step limit (OCamlPro/alt-ergo#936) - Add a generic option manager to deal with the dolmen state (OCamlPro/alt-ergo#951) - Expose an imperative SAT API in the Alt-Ergo library (OCamlPro/alt-ergo#962) - Keep track of the SMT-LIB mode (OCamlPro/alt-ergo#971) - Add ability to decide on semantic literals (OCamlPro/alt-ergo#1027, OCamlPro/alt-ergo#1118) - Preserve trigger order when parsing quantifiers with multiple trigger (OCamlPro/alt-ergo#1046). - Store domains inside the union-find module (OCamlPro/alt-ergo#1119) - Remove some polymorphic hashtables (OCamlPro/alt-ergo#1219) ### Build and integration - Drop support for OCaml <4.08.1 (OCamlPro/alt-ergo#803) - Use dune-site for the inequalities plugins. External pluginsm ust now be registered through the dune-site plugin mechanism in the `(alt-ergo plugins)` site to be picked up by Alt-Ergo (OCamlPro/alt-ergo#1049). - Add a release workflow (OCamlPro/alt-ergo#827) - Add a Windows workflow (OCamlPro/alt-ergo#1203) - Mark the dune.inc file as linguist-generated to avoid huge diffs (OCamlPro/alt-ergo#830) - Use GitHub Actions badges in the README (OCamlPro/alt-ergo#882) - Use `dune build @check` to build the project (OCamlPro/alt-ergo#887) - Enable warnings as errors on the CI (OCamlPro/alt-ergo#888) - Uniformization of internal identifiers generation (OCamlPro/alt-ergo#905, OCamlPro/alt-ergo#918) - Use an efficient `String.starts_with` implementation (OCamlPro/alt-ergo#912) - Fix the Makefile (OCamlPro/alt-ergo#914) - Add `Logs` dependency (OCamlPro/alt-ergo#1206) - Use `dynamic_include` to include the generated file `dune.inc` (OCamlPro/alt-ergo#1199) - Support Windows (OCamlPro/alt-ergo#1184,OCamlPro/alt-ergo#1189,OCamlPro/alt-ergo#1195,OCamlPro/alt-ergo#1199,OCamlPro/alt-ergo#1200) - Wrap the library `Alt_ergo_prelude` (OCamlPro/alt-ergo#1223) ### Testing - Use --enable-assertions in tests (OCamlPro/alt-ergo#809) - Add a test for push/pop (OCamlPro/alt-ergo#843) - Use the CDCL solver when testing model generation (OCamlPro/alt-ergo#938) - Do not test .smt2 files with the legacy frontend (OCamlPro/alt-ergo#939) - Restore automatic creation of .expected files (OCamlPro/alt-ergo#941) ### Documentation - Add a new example for model generation (OCamlPro/alt-ergo#826) - Add a Pygments lexer for the Alt-Ergo native language (OCamlPro/alt-ergo#862) - Update the current authors (OCamlPro/alt-ergo#865) - Documentation of the `Enum` theory (OCamlPro/alt-ergo#871) - Document `Th_util.lit_origin` (OCamlPro/alt-ergo#915) - Document the CDCL-Tableaux solver (OCamlPro/alt-ergo#995) - Document Windows support (OCamlPro/alt-ergo#1216) - Remove instructions to install Alt-Ergo on Debian (OCamlPro/alt-ergo#1217) - Document optimization feature (OCamlPro/alt-ergo#1231)

Halbaroth added the clean-up label Apr 13, 2024

Halbaroth force-pushed the merge-enum branch 4 times, most recently from ab32559 to f16ac0e Compare April 19, 2024 13:15

Halbaroth force-pushed the merge-enum branch 2 times, most recently from 799ec51 to ec5db54 Compare May 19, 2024 14:08

Halbaroth mentioned this pull request May 21, 2024

Simplify is_mine_symb #1130

Merged

Halbaroth force-pushed the merge-enum branch from ec5db54 to 7cbabb5 Compare May 23, 2024 12:52

Halbaroth marked this pull request as ready for review May 23, 2024 13:24

Halbaroth added this to the 2.6.0 milestone May 23, 2024

Halbaroth force-pushed the merge-enum branch 2 times, most recently from a67d8fb to 8b6f472 Compare May 24, 2024 09:47

Halbaroth force-pushed the merge-enum branch 2 times, most recently from dc37601 to 17d9e3c Compare June 3, 2024 11:59

Halbaroth force-pushed the merge-enum branch from e1bac3b to 408d33a Compare June 10, 2024 19:49

Halbaroth requested a review from bclement-ocp June 11, 2024 09:23

bclement-ocp reviewed Jun 11, 2024

View reviewed changes

Halbaroth changed the title ~~Merge enum~~ Merge Enum theory into ADT theory Jun 11, 2024

Halbaroth requested a review from bclement-ocp June 11, 2024 15:32

bclement-ocp approved these changes Jun 11, 2024

View reviewed changes

bclement-ocp requested changes Jun 12, 2024

View reviewed changes

Halbaroth force-pushed the merge-enum branch from f3fe7c3 to 3fc2112 Compare June 12, 2024 07:06

Halbaroth added 2 commits June 12, 2024 09:07

Merge Enum Theory into ADT Theory

9bb31c4

After refactoring both `Enum` and `ADT` theories, they shared most of their implementation.

Attempt to fix regressions

7045bb6

Halbaroth added 5 commits June 12, 2024 09:07

poetry

226fda1

Restore the check for polymorphism in enum type

1bc685a

Use a polymorphic variant for the enum flag

36d143d

Store the enum flag in the type_body

73739aa

Factorize the code of split_enum and split_best

3fc2112

bclement-ocp approved these changes Jun 12, 2024

View reviewed changes

Halbaroth merged commit 84e29b9 into OCamlPro:next Jun 12, 2024
14 checks passed

Halbaroth mentioned this pull request Jun 17, 2024

Remove Enum_rel #1147

Merged

bclement-ocp mentioned this pull request Sep 24, 2024

[new release] alt-ergo (4 packages) (2.6.0) ocaml/opam-repository#26609

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Merge `Enum` theory into `ADT` theory #1094

Merge `Enum` theory into `ADT` theory #1094

Halbaroth commented Apr 13, 2024 •

edited

Loading

Halbaroth commented Jun 11, 2024

bclement-ocp left a comment

bclement-ocp Jun 11, 2024

Halbaroth Jun 11, 2024 •

edited

Loading

bclement-ocp Jun 11, 2024

bclement-ocp Jun 11, 2024

bclement-ocp Jun 11, 2024

Halbaroth Jun 11, 2024

bclement-ocp Jun 11, 2024

Halbaroth Jun 11, 2024

Halbaroth commented Jun 11, 2024

Halbaroth commented Jun 11, 2024 •

edited

Loading

Halbaroth commented Jun 11, 2024

bclement-ocp left a comment

bclement-ocp left a comment

Halbaroth commented Jun 12, 2024

bclement-ocp commented Jun 12, 2024

Halbaroth commented Jun 12, 2024

bclement-ocp commented Jun 12, 2024

Merge Enum theory into ADT theory #1094

Merge Enum theory into ADT theory #1094

Conversation

Halbaroth commented Apr 13, 2024 • edited Loading

Halbaroth commented Jun 11, 2024

bclement-ocp left a comment

Choose a reason for hiding this comment

bclement-ocp Jun 11, 2024

Choose a reason for hiding this comment

Halbaroth Jun 11, 2024 • edited Loading

Choose a reason for hiding this comment

bclement-ocp Jun 11, 2024

Choose a reason for hiding this comment

bclement-ocp Jun 11, 2024

Choose a reason for hiding this comment

bclement-ocp Jun 11, 2024

Choose a reason for hiding this comment

Halbaroth Jun 11, 2024

Choose a reason for hiding this comment

bclement-ocp Jun 11, 2024

Choose a reason for hiding this comment

Halbaroth Jun 11, 2024

Choose a reason for hiding this comment

Halbaroth commented Jun 11, 2024

Halbaroth commented Jun 11, 2024 • edited Loading

Halbaroth commented Jun 11, 2024

bclement-ocp left a comment

Choose a reason for hiding this comment

bclement-ocp left a comment

Choose a reason for hiding this comment

Halbaroth commented Jun 12, 2024

bclement-ocp commented Jun 12, 2024

Halbaroth commented Jun 12, 2024

bclement-ocp commented Jun 12, 2024

Merge `Enum` theory into `ADT` theory #1094

Merge `Enum` theory into `ADT` theory #1094

Halbaroth commented Apr 13, 2024 •

edited

Loading

Halbaroth Jun 11, 2024 •

edited

Loading

Halbaroth commented Jun 11, 2024 •

edited

Loading