Documentation of the Enum theory #871

Halbaroth · 2023-10-12T09:51:42Z

No description provided.

src/lib/reasoners/enum.ml

bclement-ocp · 2023-10-12T10:48:39Z

src/lib/reasoners/enum_rel.ml

+(* Update the domains of the semantic values [sm1] and [sm2] according to
+   the disequality [sm1 <> sm2]. *)


This is not really useful as it repeats in English what can be assumed by the name of the function. It would be more useful to document how the domains are updated when encountering sm1 <> sm2. I assume singleton values from one side are removed from the other, but maybe something else also happens?

bclement-ocp · 2023-10-12T10:49:47Z

src/lib/reasoners/enum_rel.ml

+(* Update the domains of the semantic values [sm1] and [sm2] according to
+   the equation [sm1 = sm2]. *)


Same remark as for add_diseq above — how are the domains updated? I assume we compute the intersection of the existing domains?

src/lib/reasoners/enum_rel.ml

bclement-ocp · 2023-10-12T10:55:28Z

src/lib/reasoners/enum_rel.ml

+  (* State of the union-find represented by its equivalence classes.
+     The field is updated while assuming literals of the theory. *)


Is this a list of all the equivalence classes of the union-find, or only all the classes for terms of enum types (or something else)? What do we use it for?

It's actually the same design in most theories. We have to save the state of the all union-find after assuming each literal in order to return the appropriate state if we perform a query in this theory and we got an inconsistency.

Actually, it's the case in all theories, which means we can bubble this feature in Relation but I'm not sure it will be clearer.

Ah right, this for caching is the result of cl_extract that is used only for a debug message. I don't think we can lift this to Relation (it is needed to raise Ex.Inconsistent and the relations do raise Ex.Inconsistent). We should make it clear in the doc that this is a cache of Uf.cl_extract (if the --bottom-classes flag is not passed to Alt-Ergo, Uf.cl_extract is always []).

That's why I said I'm not sure it will be clearer as we would have to create a new intermediate exception :/
I agree that the best solution is to write a clear comment.

bclement-ocp · 2023-10-12T10:57:09Z

src/lib/reasoners/enum_rel.ml

+  (* Map of uninterpreted enum semantic values to domains of their possible
+     values. The explanation justifies that the value of the semantic value
+     lies in the domain. *)


Are the keys in the MX.t arbitrary semantic values or (current) normal forms only?

(Looks like it is arbitrary semantic values)

I'm not sure to understand what you mean by normal form here? There is no canonization for Enum theory.

I mean normal form modulo congruence (see find_r → find_or_normal_form in Uf), e.g. if we have f(x) and f(x) = y then the normal form of f(x) is y; in other word, class representatives (modulo AC(X) shenaningans).

It's arbitrary semantic values as the only way to remove elements in the field mx is by backtracking in the SAT solver. We could remove the old normal form key and use Uf.find to search in the mx map. I don't know if it's very important. We could save a tiny amount of memory and I guess doing this will be a bit slower.

I am not asking to change the implementation, just trying to understand what it does so that the documentation is accurate :)

(Note that using class representatives as the key would also cause the same issue we observe in #474 / #823 )

I am not saying to change the implementation in this PR ;)

bclement-ocp · 2023-10-12T11:02:04Z

src/lib/reasoners/enum_rel.ml

@@ -195,6 +222,7 @@ let count_splits env la =
  in
  {env with size_splits = nb}

+(* Add the uninterpreted semantic value [r] to the environment. *)


Same as above, it is clear from the name that we add [r] to the environment, but what does it mean? Apparently we initialize the corresponding mx entry with all the possible constructors for its type.

bclement-ocp · 2023-10-12T11:24:05Z

src/lib/reasoners/enum_rel.ml

+              of cardinal 1 as we have to put this value in the
+              equivalence class of [r]. *)


I think that "let Uf know about the equality" would be more precise — in particular this matters for model generation.

Halbaroth · 2023-10-12T12:58:14Z

src/lib/reasoners/enum_rel.ml

+(* Update the domains of the semantic values [sm1] and [sm2] according to
+   the equation [sm1 = sm2]. More precisely, we replace their domains by
+   the intersection of these domains.
+
+   In any case, we produce an equality if the domain of these semantic values
+   becomes a singleton.
+
+   @raise Ex.Inconsistent if the domains of [sm1] and [sm2] are disjoint. *)


I know this comment is a bit wrong as the function doesn't produce a new equality when one of the semantic values is a constructor. I don't know why? Maybe we don't need to process it here because it will be done somewhere else.

If we execute this function with Alien _, Cons _ or Cons _, Alien _ we are already processing the equality that we would be producing :)

Halbaroth · 2023-10-12T13:00:06Z

src/lib/reasoners/enum_rel.ml

+  (* Map of uninterpreted enum semantic values to domains of their possible
+     values. The explanation justifies that any value assigns to the semantic
+     value has to lie in the domain. *)


I changed a bit the comment. It didn't make sense to talk about the value of the semantic value.

src/lib/reasoners/enum_rel.ml

bclement-ocp · 2023-10-13T13:11:41Z

src/lib/reasoners/enum_rel.ml

+  (* State of the union-find represented by all its equivalence classes.
+     This state is kept for debugging purposes only. It is updated after
+     assuming literals of the theory and returned by queries in case of
+     inconsistency. *)


Please mention Uf.cl_extract explicitly here.

bclement-ocp · 2023-10-13T13:39:29Z

src/lib/reasoners/enum_rel.ml

+    (* We don't need to produce a new equality as we already know it
+       by transitivity of equality. *)


I don't think transitivity is involved here, maybe commutativity? We are processing the equality r = h, which is exactly the equality we would be adding.

Co-authored-by: Basile Clément <[email protected]>

src/lib/reasoners/enum_rel.ml

Co-authored-by: Basile Clément <[email protected]>

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 documentation label Oct 12, 2023

bclement-ocp reviewed Oct 12, 2023

View reviewed changes

Halbaroth force-pushed the documentation-enum branch from 01feffc to 6ec457b Compare October 12, 2023 12:54

Halbaroth requested a review from bclement-ocp October 12, 2023 12:55

Halbaroth commented Oct 12, 2023

View reviewed changes

bclement-ocp reviewed Oct 12, 2023

View reviewed changes

src/lib/reasoners/enum_rel.ml Outdated Show resolved Hide resolved

Halbaroth requested a review from bclement-ocp October 13, 2023 12:42

bclement-ocp requested changes Oct 13, 2023

View reviewed changes

Halbaroth force-pushed the documentation-enum branch from a542a5b to 0d368a5 Compare October 23, 2023 08:15

Halbaroth requested a review from bclement-ocp October 23, 2023 08:16

Halbaroth and others added 11 commits October 23, 2023 10:16

Documentation of the Enum theory

7526987

Update src/lib/reasoners/enum.ml

d092729

Co-authored-by: Basile Clément <[email protected]>

Update src/lib/reasoners/enum.ml

e791a1e

Co-authored-by: Basile Clément <[email protected]>

Update src/lib/reasoners/enum_rel.ml

1ef6ba7

Co-authored-by: Basile Clément <[email protected]>

Update src/lib/reasoners/enum_rel.ml

002ef72

Co-authored-by: Basile Clément <[email protected]>

Update src/lib/reasoners/enum_rel.ml

e00cc52

Co-authored-by: Basile Clément <[email protected]>

Review changes

3729dad

Update src/lib/reasoners/enum_rel.ml

a320857

Co-authored-by: Basile Clément <[email protected]>

Review changes 2

d54e4c1

Specify that the state is updated with cl_extract

bf8c468

Review changes 3

0d368a5

bclement-ocp approved these changes Oct 23, 2023

View reviewed changes

src/lib/reasoners/enum_rel.ml Outdated Show resolved Hide resolved

src/lib/reasoners/enum_rel.ml Outdated Show resolved Hide resolved

Halbaroth and others added 2 commits October 23, 2023 10:51

Update src/lib/reasoners/enum_rel.ml

2c73362

Co-authored-by: Basile Clément <[email protected]>

Update src/lib/reasoners/enum_rel.ml

365df7c

Co-authored-by: Basile Clément <[email protected]>

Halbaroth enabled auto-merge (squash) October 23, 2023 08:52

Halbaroth merged commit 0140c9a into OCamlPro:next Oct 23, 2023

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

Documentation of the Enum theory #871

Documentation of the Enum theory #871

Halbaroth commented Oct 12, 2023

bclement-ocp Oct 12, 2023

bclement-ocp Oct 12, 2023

bclement-ocp Oct 12, 2023

Halbaroth Oct 12, 2023

Halbaroth Oct 12, 2023

bclement-ocp Oct 12, 2023

Halbaroth Oct 12, 2023

bclement-ocp Oct 12, 2023

bclement-ocp Oct 12, 2023

Halbaroth Oct 12, 2023

bclement-ocp Oct 12, 2023

Halbaroth Oct 12, 2023

bclement-ocp Oct 12, 2023

Halbaroth Oct 13, 2023

bclement-ocp Oct 12, 2023

bclement-ocp Oct 12, 2023

Halbaroth Oct 12, 2023 •

edited

Loading

bclement-ocp Oct 12, 2023

Halbaroth Oct 12, 2023

bclement-ocp Oct 13, 2023

bclement-ocp Oct 13, 2023

		(* Update the domains of the semantic values [sm1] and [sm2] according to
		the disequality [sm1 <> sm2]. *)

		(* Update the domains of the semantic values [sm1] and [sm2] according to
		the equation [sm1 = sm2]. *)

		(* State of the union-find represented by its equivalence classes.
		The field is updated while assuming literals of the theory. *)

		of cardinal 1 as we have to put this value in the
		equivalence class of [r]. *)

		(* We don't need to produce a new equality as we already know it
		by transitivity of equality. *)

Documentation of the Enum theory #871

Documentation of the Enum theory #871

Conversation

Halbaroth commented Oct 12, 2023

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

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 Oct 12, 2023 • edited Loading

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 Oct 12, 2023 •

edited

Loading