refactor(BV): Merge `Congruence` and `Constraints` #1010

bclement-ocp · 2023-12-12T12:48:09Z

In #944, the Congruence module was added to simplify handling dependences for both domains and constraints, because we tracked domains separately for all terms.

After #1004, we now track domains only for uninterpreted leaves, and the Congruence module is only used for Constraints. This leads to a sort of double indirection: the Congruence module keeps track of reverse uninterpreted leaves -> class representative dependencies, and then the Constraints module keeps track of reverse class representative -> constraint dependencies.

This patch removes the Congruence module entirely; instead, the Constraints module is now keeping track of reverse uninterpreted leaves -> constraint dependencies directly.

In addition, the Constraints module is made into a functor and moved to the Rel_utils module, since it is now a generic module that can be useful for any relational theory (like Congruence was before).

I recommend reviewing the PR commit by commit to better be able to follow the changes: the commit that does the actual changes in implementation of the Constraints module is the one titled "Fold Congruence into Constraints"; the others are mostly shuffling code around, which makes the global diffs hard to follow.

Note: This currently includes #1004.

bclement-ocp · 2023-12-12T13:20:13Z

This is +1-0 on smtlib/BV; not sure it is worth running on QF_BV for this change since that takes a lot of time (maybe we should build a small subset of QF_BV).

Edit: +1-0 compared to #1004

Halbaroth · 2023-12-20T15:02:13Z

src/lib/reasoners/rel_utils.ml

-      change.
-  *)
+  val subst : Explanation.t -> X.r -> X.r -> t -> t
+  (** [subst ex p v cs] replaces all the instaces of [p] with [v] in the


Suggested change

(** [subst ex p v cs] replaces all the instaces of [p] with [v] in the

(** [subst ex p v cs] replaces all the instances of [p] with [v] in the

Halbaroth · 2023-12-20T15:04:18Z

src/lib/reasoners/rel_utils.ml

-      semantic values.
+module type Constraint = sig
+  type t
+  (** The type of bit-vector constraints.


I guess we expect to use this module for constraints in other theories? For instance, we should use it in ADT theory.

Yeah, I intended to remove reference to bit-vectors in this module but forgot some :)

src/lib/reasoners/rel_utils.ml

Halbaroth · 2023-12-20T16:25:18Z

src/lib/reasoners/rel_utils.ml

+      identical constraints with different justifications will otherwise behave
+      identically (and, notably, will compare equal).
+
+      Bit-vector constraints contains semantic values / term representatives of


Halbaroth · 2023-12-20T16:27:38Z

src/lib/reasoners/bitv_rel.ml

+    (** Mapping from semantic values to their bitlist domain.
+
+        Note: this mapping only contains domain for leaves (i.e. uninterpreted
+        terms or AC symbols); domains associated with more complex semantic
+        values are rebuilt on-the-fly using the structure of said semantic
+        values. *)


It seems this PR is rebased on #1004, which means we cannot merge it before solving #1005 too.

It is explicitly mentioned in the PR description that it includes #1004 :)

Halbaroth · 2023-12-20T16:34:32Z

src/lib/reasoners/rel_utils.ml

+  val fold_fresh : (Constraint.t -> 'a -> 'a) -> t -> 'a -> t * 'a
+  (** [fold_fresh f cs acc] folds [f] over the fresh constraints in [cs].

-      More precisely, it will fold [f] over the pairs [(rr, nrr)] such that:
-      - [rr] was registered in the congruence
-      - [nrr] is [X.subst p v rr]
+      Fresh constraints are constraints that were never propagated yet. *)


We should mention that the fresh constraint queue is flushed by this iterator.

I will rename this function as propagate_fresh and only expose fold_fresh Constraint.propagate and mention this in the doc of that function.

src/lib/reasoners/rel_utils.ml

This patch makes the representation of bit-vector constraints abstract. This is preparatory work for further refactoring, as there is no reason to expose it outside of the `Constraint` module.

This is in preparation of further refactoring work to make `Constraints` a functor.

In OCamlPro#944, the `Congruence` module was added to simplify handling dependences for both domains and constraints, because we tracked domains separately for all terms. After OCamlPro#1004, we now track domains only for uninterpreted leaves, and the `Congruence` module is only used for `Constraints`. This leads to a sort of double indirection: the `Congruence` module keeps track of reverse uninterpreted leaves -> class representative dependencies, and then the `Constraints` module keeps track of reverse class representative -> constraint dependencies. This patch removes the `Congruence` module entirely; instead, the `Constraints` module is now keeping track of reverse uninterpreted leaves -> constraint dependencies directly. Further refactoring work will move the `Congruence` module to `Rel_utils` as it can be a generally useful module for other theories.

This patch moves the `Constraints` module from the BV theory to the `Rel_utils` theory and make it a functor. This makes it independent from the implementation of BV constraints and makes it useable in other theories in the future.

bclement-ocp · 2024-01-09T16:48:49Z

Rebased after merging #1004; should be ready for a 2nd round @Halbaroth

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)

bclement-ocp force-pushed the bclement/constraint_utils branch from 4f88ab0 to 5a0492c Compare December 15, 2023 12:25

Halbaroth requested changes Dec 20, 2023

View reviewed changes

bclement-ocp force-pushed the bclement/constraint_utils branch 2 times, most recently from 77ddc9d to d9aa8a6 Compare January 3, 2024 14:38

bclement-ocp mentioned this pull request Jan 9, 2024

refactor(BV): Track domains for uninterpreted leaves only #1004

Merged

bclement-ocp added 4 commits January 9, 2024 17:48

refactor(BV): Hide constraint representation

9e1008d

This patch makes the representation of bit-vector constraints abstract. This is preparatory work for further refactoring, as there is no reason to expose it outside of the `Constraint` module.

refactor(BV): Extract signature of the Constraint module

9a43a23

This is in preparation of further refactoring work to make `Constraints` a functor.

refactor(CP): Generalize Constraints module

ea5bce6

This patch moves the `Constraints` module from the BV theory to the `Rel_utils` theory and make it a functor. This makes it independent from the implementation of BV constraints and makes it useable in other theories in the future.

bclement-ocp force-pushed the bclement/constraint_utils branch from d9aa8a6 to ea5bce6 Compare January 9, 2024 16:48

bclement-ocp requested a review from Halbaroth January 9, 2024 16:48

Halbaroth approved these changes Jan 10, 2024

View reviewed changes

Halbaroth merged commit 4d6de71 into OCamlPro:next Jan 10, 2024
13 checks passed

bclement-ocp deleted the bclement/constraint_utils branch January 23, 2024 08:52

bclement-ocp added this to the 2.6.0 milestone Jul 11, 2024

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

refactor(BV): Merge `Congruence` and `Constraints` #1010

refactor(BV): Merge `Congruence` and `Constraints` #1010

bclement-ocp commented Dec 12, 2023

bclement-ocp commented Dec 12, 2023 •

edited

Loading

Halbaroth Dec 20, 2023

Halbaroth Dec 20, 2023

bclement-ocp Dec 20, 2023

Halbaroth Dec 20, 2023

Halbaroth Dec 20, 2023

bclement-ocp Dec 20, 2023

Halbaroth Dec 20, 2023

bclement-ocp Dec 20, 2023

bclement-ocp commented Jan 9, 2024

	(** [subst ex p v cs] replaces all the instaces of [p] with [v] in the
	(** [subst ex p v cs] replaces all the instances of [p] with [v] in the

refactor(BV): Merge Congruence and Constraints #1010

refactor(BV): Merge Congruence and Constraints #1010

Conversation

bclement-ocp commented Dec 12, 2023

bclement-ocp commented Dec 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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bclement-ocp commented Jan 9, 2024

refactor(BV): Merge `Congruence` and `Constraints` #1010

refactor(BV): Merge `Congruence` and `Constraints` #1010

bclement-ocp commented Dec 12, 2023 •

edited

Loading