feat(BV): Word-level propagation for BV logic #944

bclement-ocp · 2023-11-16T15:10:02Z

**This PR currently includes #943 **

This patch implements constraint propagation for the logical operators (and, or, xor) on bit-vectors.

The goal of this patch is to ensure that Alt-Ergo has a complete understanding of the logical operators on bit-vectors, and in particular that it will never violate the definition of the logical operators when generating models. They are thus removed from the "suspicious" operators (along with int2bv and bv2nat that are now handled through the "delayed functions" mechanism, even though this patch does not impact these functions).

The patch can be decomposed in changes of the following categories, where each category can mostly be reviewed independently (all in the same patch because they wouldn't really make sense on their own):

Some minor refactoring in Bitv, Th_util, Expr, ModelMap and Symbols to expose the required functions and types, including a Th_bitv constructor for bit-vector case-splits and a built-in symbol for bvxor
The new Bitlist module introduces a representation of bit-vector domains as bit-lists, i.e. pairs of (ones, zeroes) represented as integers where the bits forced to 1 are set in ones, and the bits forced to 0 are set in zeroes.
There is a new Congruence module in Rel_utils that is exploited by the BV constraint propagators. The Congruence module can be understood as a lighter version of Use for semantic values (rather than terms): it provides a mechanism to register "semantic values of interest" (in our case, it will be the arguments of the logical operators and the result of the logical operator themselves) and be notified when the representative of these semantic values of interest are updated. To avoid partially inconsistent states, the congruence module computes the leaves the each semantic values of interest and updates all the semantic values that have a given leaf at once.

This Congruence module is not BV-specific, hence why it is in Rel_utils.
Finally, the main course is in the Bitv_rel module, where the new constraint propagators are added. The constraint propagators are represented using separate Domains and Constraints modules that are kept normalized (i.e. they only reference current class representatives in Uf) through the Congruence utility.

The Domains module is simply a map from class representatives to their domain, represented as a Bitlist. To avoid unnecessary propagations, the Domains module keeps track of the values whose domain has changed since the last propagation, to know that we must propagate the associated constraints again.

The Constraints module is a set of Constraints that keeps track of the semantic values that are involved in each constraint to avoid unnecessary propagations. The Constraints are normalized (so that if we have both a = b & c and a = b & d, we only keep one once we learn that c = d), and we also keep track of the constraints that were never propagated.

The Bitv_rel environment then keeps track of a Domains and a Constraints set that are updated through Congruence whenever a class representative changes (detected through equalities with Subst origin). After each change to either the domains or the constraints (either through a class representative change or because we added a new constraint), we propagate the fresh constraints and the constraints involving values whose domain has changed. We maintain the invariant that, outside of the add and assume functions, all the constraints in the Constraints set are satisfied by the domains of the Domains.

In the interest of keeping the patch relatively short and facilitate its review, many desirable features have been left out for now, and there are many places where the implementation can be improved. Notably:

We do not perform any sort of constraint simplification (outside of the normalization used for de-duplication). This can cause backtracking inefficiencies: if we have a constraint involving the concatenation a @ b, and we substitute b -> c, then detect a conflict involving a, the explanation for the substitution b -> c will end up in the conflict even though it had no impact, causing more work than necessary. This can be added in a second step.
The constraints are represented in a relational way rather than a functional way. This means that if we have both a = b & c and d = b & c as constraints, we will not learn that a = d. I don't think this has any impact currently, because the only way we can learn a constraint a = b & c is if a is equal to b & c as a term, but could have one in the future if we want to perform simplifications.
Only logical operators are supported. In particular, there is no support for combined reasoning with arithmetic, which is a whole can of worms in itself (in the current Alt-Ergo architecture, we do not have access to the interval domains from the bit-vector theory and conversely).

Finally, this patch purposely does not implement any sort of algebraic reasoning on bit-vectors ¹: while with this patch Alt-Ergo is able to prove theorems such as De Morgan's laws or algebraic properties (associativity, commutativity, neutral elements, inverses, etc.) of the logical operators, this will currently happen through painstaking case-splitting which gets slow on large bit-vector sizes ².

The equation x ^ x = 0 happens to be known as a side-effect of the representation of XOR constraints. ↩
The value of "large" here is actually fairly small, because proving these laws through propagation often requires exploring the full space, which is exponential. ↩

It turns out that OCamlPro#881 revealed a latent issue with the implementation in OCamlPro#733 When we encounter a [bv2nat] term, we create a *term* that represents the [bv2nat] computation, then call [X.make] on the result. This has the unfortunate effect that the sub-terms of that new term are not added to the Union-Find (or at least not before the term itself). This is bad, but was harmless at the time. However, the resulting term from a call of [bv2nat] includes divisions. And since OCamlPro#881 divisions are represented by an uninterpreted term rather than an existential variable — and [IntervalCalculus.add] inspects that term, rightfully expecting that its sub-terms have been added to the Union-Find, which in this case they are not, and so we crash. This patch fixes the issue by introducing an uninterpreted term for the result of [bv2nat] and adding the equality between that uninterpreted term and the [bv2nat] computation. This equality is then processed as a term on its own, ensuring that subterms are added to the Union-Find before the terms that contain them. Note that long-term, we probably want to get rid of the construction of [bv2nat] terms directly in [X.make] in favor of propagators in a follow-up to OCamlPro#944 . This would avoid needing to go through terms for this.

bclement-ocp · 2023-11-20T12:31:48Z

Note: running benchmarks against next require #954 to be merged.

It turns out that #881 revealed a latent issue with the implementation in #733 When we encounter a [bv2nat] term, we create a *term* that represents the [bv2nat] computation, then call [X.make] on the result. This has the unfortunate effect that the sub-terms of that new term are not added to the Union-Find (or at least not before the term itself). This is bad, but was harmless at the time. However, the resulting term from a call of [bv2nat] includes divisions. And since #881 divisions are represented by an uninterpreted term rather than an existential variable — and [IntervalCalculus.add] inspects that term, rightfully expecting that its sub-terms have been added to the Union-Find, which in this case they are not, and so we crash. This patch fixes the issue by introducing an uninterpreted term for the result of [bv2nat] and adding the equality between that uninterpreted term and the [bv2nat] computation. This equality is then processed as a term on its own, ensuring that subterms are added to the Union-Find before the terms that contain them. Note that long-term, we probably want to get rid of the construction of [bv2nat] terms directly in [X.make] in favor of propagators in a follow-up to #944 . This would avoid needing to go through terms for this.

bclement-ocp · 2023-11-22T17:54:35Z

Looks like there is unsoundness in some benches — marking as draft until I can dig deeper.

Halbaroth · 2023-11-23T08:31:29Z

Can I submit my review anyway? My remarks are mostly about documentation and some questions.

bclement-ocp · 2023-11-23T08:34:56Z

Can I submit my review anyway? My remarks are mostly about documentation and some questions.

Yes sure — I have just marked it as draft to make sure it is not merged.

I also have identified the soundness issue (a misunderstanding on my part in the meaning of the is_cs return value of case_split); a patch is on the way.

The BV model generation was using an incorrect understanding of the [is_cs] flag that lead to unsoundness because it assumed that it was fine to set this flag to [false] when the value is forced *in the current context* whereas it is only valid to do so when the value is forced *in all contexts*. This PR fixes that Unfortunately the fix leads to a test that no longer passes, but for good reason as the reasoning used for it was unsound. Hopefully this should be fixed in a follow-up to OCamlPro#944 I have also added a new test that is actually satisfiable but would previously return [unsat]. It times out for now, but is solved properly in OCamlPro#944

The BV model generation was using an incorrect understanding of the [is_cs] flag that lead to unsoundness because it assumed that it was fine to set this flag to [false] when the value is forced *in the current context* whereas it is only valid to do so when the value is forced *in all contexts*. This PR fixes that, and adds copious amounts of documentation to explain the [is_cs] flag so that we don't make the same mistake again. Unfortunately the fix leads to a test that no longer passes, but for good reason as the reasoning used for it was unsound. Hopefully this should be fixed in a follow-up to OCamlPro#944 I have also added a new test that is actually satisfiable but would previously return [unsat]. It times out for now, but is solved properly in OCamlPro#944

bclement-ocp · 2023-11-23T10:57:41Z

The soundness issue is solved through a combination of Handle case-split conflicts properly and #968

Waiting on #968 and #969 to be merged to run benches again

Note that there are cases where we used to be able to solve but we no longer are able to solve due to (I believe) the coarse explanations returned by constraint propagation that causes Alt-Ergo to perform exhaustive enumeration rather than actually performing the higher-level reasoning steps that it is able to do without this patch. These should be at least partially fixed by performing constraint simplifications, which was explicitly left out of this PR for now, as explained in the description.

Halbaroth · 2023-11-22T12:51:02Z

src/lib/reasoners/rel_utils.ml

+  (** The [Congruence] module implements a simil-congruence closure algorithm on
+      semantic values.
+
+      It provides an interface to register some semantic values of interest, and
+      for applying a callback when the representative of those registered values
+      change.
+  *)


A general question about the necessity of this module. During the last meeting, you suggest that we use expression too deeply in the solver (for instance we keep using expression in SatML for the representation of literals). If we stop doing this and use as soon as possible semantic values, could we use the CC(X) algorithm here?

I am not sure it is related to the use of expressions in satML, but yes, ideally CC(X) would have a built-in way of keeping track of this information rather than having each relation re-implement the bits it needs as we currently do. But AE currently doesn't really provide the required infrastructure (I thought about using it, but I believe that would require some non-trivial modifications that would be a full PR on their own, so I decided against it), so at least we can try to share the infrastructure.

Halbaroth · 2023-11-22T12:59:38Z

src/lib/reasoners/rel_utils.ml

+  type t = { parents : SX.t MX.t ; registered : SX.t }
+


Could you add a bit of documentation for parents? We call recall it's a similar structure to the Use one.

Yeah, but Use is on terms, and this is on semantic values. Added a comment.

src/lib/reasoners/rel_utils.ml

Halbaroth · 2023-11-22T14:07:05Z

src/lib/reasoners/bitlist.mli

+val subsumes : t -> t -> bool
+(** [subsumes b1 b2] returns [true] if [b1] has more information than [b2].
+
+    More precisely, it checks that all the bits known by [b2] are also known by
+    [b1]; it *does not* check that [b1] and [b2] are consistent. *)


subsumes is misleading as the function doesn't check the consistency. When I read subsumes, I expect one of the two arguments implies the other one.

It initially did check that when I called it that way, then it no longer did. Actually this is only used in situations where equal can be used instead, so I will just use that and remove subsumes.

src/lib/reasoners/bitv_rel.ml

The BV model generation was using an incorrect understanding of the [is_cs] flag that lead to unsoundness because it assumed that it was fine to set this flag to [false] when the value is forced *in the current context* whereas it is only valid to do so when the value is forced *in all contexts*. This PR fixes that, and adds copious amounts of documentation to explain the [is_cs] flag so that we don't make the same mistake again. Unfortunately the fix leads to a test that no longer passes, but for good reason as the reasoning used for it was unsound. Hopefully this should be fixed in a follow-up to #944 I have also added a new test that is actually satisfiable but would previously return [unsat]. It times out for now, but is solved properly in #944

bclement-ocp · 2023-11-24T13:50:31Z

Test failure is slow f1 again.

bclement-ocp · 2023-11-27T14:24:16Z

This was +876-692 (delta of +184 which is nice) on QF_BV against #943 but the benchmarks lead to the detection of #978 and #979

Among the 692 regressions there is a certain number of cases where we time out due to being too aggressive in terms of splits; I have implemented support for Options.get_max_split () in the BV domain which seems to help on the few cases I have manually re-run. Rerunning benchmarks on QF_BV with these changes against next, with #943 and the fixes for #978 and #979.

Edit: I know I messed up the style, I will fix it once the benches are done.

This was just an unfortunate omission that led to needlessly bloated environments.

We cannot simply claim that forced splits are not case splits (see OCamlPro#968 ). In order to do proper backtracking using exlpanations, we have to propagate the equality [x = #b1] when we learn [x = #b0] from the case-split. To keep things simple, we only directly support [Distinct] in the BV domain for the literals that come from a case split (other cases are handled by the union-find *after* the splits). We might want to add proper support for arbitrary [Distinct] constraints later.

We can just use [Bitlist.equal].

Co-authored-by: Hichem R. A. <hra687261@gmail.com>

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.

* refactor(BV): Hide constraint representation 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 This is in preparation of further refactoring work to make `Constraints` a functor. * refactor(BV): Fold `Congruence` into `Constraints` 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. Further refactoring work will move the `Congruence` module to `Rel_utils` as it can be a generally useful module for other theories. * refactor(CP): Generalize `Constraints` module 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.

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 requested review from Halbaroth and hra687261 November 16, 2023 15:10

bclement-ocp force-pushed the bclement-ocp/bvprop branch from 229fa6b to abed389 Compare November 16, 2023 18:47

bclement-ocp added the models This issue is related to model generation. label Nov 17, 2023

bclement-ocp force-pushed the bclement-ocp/bvprop branch from abed389 to 38f3a93 Compare November 17, 2023 16:04

bclement-ocp mentioned this pull request Nov 20, 2023

fix: Do not call [X.make] on non-subterms for bv2nat #954

Merged

bclement-ocp force-pushed the bclement-ocp/bvprop branch from 38f3a93 to 3210744 Compare November 20, 2023 12:31

bclement-ocp force-pushed the bclement-ocp/bvprop branch from 3210744 to 5dcd86f Compare November 22, 2023 12:25

bclement-ocp marked this pull request as draft November 22, 2023 17:54

bclement-ocp mentioned this pull request Nov 23, 2023

fix(BV): Fix unsoundness in BV model generation #968

Merged

bclement-ocp marked this pull request as ready for review November 23, 2023 10:57

Halbaroth requested changes Nov 23, 2023

View reviewed changes

bclement-ocp force-pushed the bclement-ocp/bvprop branch from 9d2713c to e8ba880 Compare November 24, 2023 08:59

bclement-ocp requested a review from Halbaroth November 24, 2023 09:00

bclement-ocp force-pushed the bclement-ocp/bvprop branch 3 times, most recently from 1d48284 to d5e83b9 Compare November 27, 2023 14:20

bclement-ocp and others added 15 commits November 30, 2023 17:33

Remove substituted constraints

1e73745

This was just an unfortunate omission that led to needlessly bloated environments.

Fix warning: uf not needed in case_split

d50e2b5

Remove [Bitlist.subsumes]

710c78b

We can just use [Bitlist.equal].

Add @raise annotations

00b7f05

Clarification

5e39f46

Back to 1972

b607970

F(or)m(a)t

6386c81

Util.MI

3a11c85

Gimme space

c485042

Document congruence parents

bea7d42

That's not consistent!

cc133ea

Tests from OCamlPro#968 are now passing 🎉

0d4e0d6

Limit split size

40f489b

Apply suggestions from code review

c9aa00f

Co-authored-by: Hichem R. A. <hra687261@gmail.com>

bclement-ocp force-pushed the bclement-ocp/bvprop branch from 59d7e3c to c9aa00f Compare November 30, 2023 16:34

bclement-ocp enabled auto-merge (squash) November 30, 2023 16:35

bclement-ocp merged commit b9ca08f into OCamlPro:next Nov 30, 2023
14 checks passed

bclement-ocp mentioned this pull request Dec 6, 2023

Improving reasoning for the BV theory #903

Open

4 tasks

bclement-ocp mentioned this pull request Dec 12, 2023

refactor(BV): Merge Congruence and Constraints #1010

Merged

bclement-ocp deleted the bclement-ocp/bvprop branch January 23, 2024 08:51

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

feat(BV): Word-level propagation for BV logic #944

feat(BV): Word-level propagation for BV logic #944

bclement-ocp commented Nov 16, 2023

bclement-ocp commented Nov 20, 2023

bclement-ocp commented Nov 22, 2023

Halbaroth commented Nov 23, 2023

bclement-ocp commented Nov 23, 2023

bclement-ocp commented Nov 23, 2023

Halbaroth Nov 22, 2023

bclement-ocp Nov 23, 2023

Halbaroth Nov 22, 2023

bclement-ocp Nov 23, 2023

Halbaroth Nov 22, 2023

bclement-ocp Nov 23, 2023

bclement-ocp commented Nov 24, 2023

bclement-ocp commented Nov 27, 2023 •

edited

Loading

feat(BV): Word-level propagation for BV logic #944

feat(BV): Word-level propagation for BV logic #944

Conversation

bclement-ocp commented Nov 16, 2023

Footnotes

bclement-ocp commented Nov 20, 2023

bclement-ocp commented Nov 22, 2023

Halbaroth commented Nov 23, 2023

bclement-ocp commented Nov 23, 2023

bclement-ocp commented Nov 23, 2023

Halbaroth Nov 22, 2023

Choose a reason for hiding this comment

bclement-ocp Nov 23, 2023

Choose a reason for hiding this comment

Halbaroth Nov 22, 2023

Choose a reason for hiding this comment

bclement-ocp Nov 23, 2023

Choose a reason for hiding this comment

Halbaroth Nov 22, 2023

Choose a reason for hiding this comment

bclement-ocp Nov 23, 2023

Choose a reason for hiding this comment

bclement-ocp commented Nov 24, 2023

bclement-ocp commented Nov 27, 2023 • edited Loading

bclement-ocp commented Nov 27, 2023 •

edited

Loading