feat(BV): Interval domains for bit-vectors #1058

bclement-ocp · 2024-03-13T15:45:08Z

This patch adds interval domains to the Bitv_rel module, as well as
interreductions between the bitlist and interval domains following:

Sharpening Constraint Programming approaches for Bit-Vector Theory.
Zakaria Chihani, Bruno Marre, François Bobot, Sébastien Bardin.
CPAIOR 2017. International Conference on AI and OR Techniques in
Constraint Programming for Combinatorial Optimization Problems, Jun
2017, Padova, Italy.

More precisely:

The Intervals module is extended to support the extract operation, which is used to propagate between bit-vector compositions and their components;
The interreductions are implemented using the new Bitlist.increase_lower_bound, Bitlist.decrease_upper_bound, and the new shared_msb helper in Bitv_rel;
Propagations are performed by alternating propagations until fixpoint in each domain, followed by interreductions and propagations until fixpoint in the other domain, until reaching a fixpoint for the whole procedure. It is not clear that this is the best strategy; the goal is to try and limit interreductions since they are relatively expensive but we should revisit this once more operations are supported.

For now, only the bvule, bvult, bvugt and bvuge primitives are supported as built-in bit-vector operations; other operations such as bvadd are still encoded using bv2nat. These operations will be migrated to bit-vector primitives in a follow-up PR.

Finally, there are some tests for the tricky bits (Intervals.extract and the interreduction primitives) using QCheck.

bclement-ocp · 2024-03-22T19:10:55Z

Note: this is +107-515 or a net regression of about 400 problems on our QF_BV subset. This is expected: this PR uses bit-vector domains for bvule / bvult / etc. but does not change the use of bv2nat / int2bv round-trip for other arithmetic operators. This means that we are prevented from doing many interesting propagations.

A follow-up PR (should be ready sometime next week) fixes that by implementing arithmetic propagators for the BV interval domains: it is currently +1156-209 (or an improvement of almost 1000 problems) on that same subset compared to next, at least in part due to interreduction between arithmetic and bitwise constraints.

bclement-ocp · 2024-04-08T07:34:48Z

After reading and thinking a lot (and starting a small Coq developement) about the explanations for intervals:

I am quite confident that the map_monotone function introduced in this PR, and the map2_monotone function introduced in feat(BV, CP): Add propagators for bvshl and bvlshr #1085, are correct
I am reasonably confident that the other interval functions introduced in this PR and following PRs are correct when called on a single interval, with the exception maybe of extract
I am not convinced that the other interval functions are correct when called on an union of intervals.

That is not to say that I don't think they are correct (in particular, I am confident that all of these functions return the right values for the bounds), but that they may forget necessary explanations in some cases, causing unsoundness. I think the cases where we forget explanations are quite rare (or may be made impossible currently) so I will rewrite these functions to try to be less clever and add more explanations. I will also write a documentation for the intervals module, now that i understand the invariants better.

This does not impact the rest of the PR or the rest of the PRs in the stack.

bclement-ocp · 2024-04-08T13:19:32Z

I am quite confident that the map_monotone function introduced in this PR, and the map2_monotone function introduced inhttps://github.com//pull/1085, are correct

Turns out they are not (: I thought I had replicated the behavior of the add function properly, but turns out I missed a crucial detail.

Halbaroth · 2024-04-08T14:32:19Z

I started a review of the code? Should I discard it?

bclement-ocp · 2024-04-08T14:35:59Z

Everything except for changes to the Intervals.ml module is still valid and can be reviewed. There are subtleties in the interval module (I am starting to believe that there are pre-existing hard-to-trigger soundness bugs lurking, although the module is very unclear about its invariants so maybe it is actually impossible), so I would hold off reviewing changes to this file specifically. But the rest should not be affected — again, it is just implementation details of the way the Intervals module stores explanations.

src/lib/reasoners/intervals.ml

tests/bitv/bitlist-interval001.smt2

src/lib/reasoners/bitv_rel.ml

Halbaroth · 2024-04-08T14:44:33Z

Everything except for changes to the Intervals.ml module is still valid and can be reviewed. There are subtleties in the interval module (I am starting to believe that there are pre-existing hard-to-trigger soundness bugs lurking, although the module is very unclear about its invariants so maybe it is actually impossible), so I would hold off reviewing changes to this file specifically. But the rest should not be affected — again, it is just implementation details of the way the Intervals module stores explanations.

Honestly, when I read this module months ago, my conclusion was we should rewrite it completely. It's not a priority but I plan to work on it later.

bclement-ocp · 2024-04-08T15:19:49Z

Honestly, when I read this module months ago, my conclusion was we should rewrite it completely. It's not a priority but I plan to work on it later.

I am about 99% sure there currently are soundness bugs that can be triggered by properly crafted formulas so I am actually looking into it now. Hopefully I will not need a full rewrite to fix them :/

The existing Intervals module suffers from multiple drawbacks. It is undocumented, uses a questionable implementation where explanations associated with each internal bounds have unclear semantics (did I mention it is not documented), and it has been the source of many soundness bug in the past due to the way it uses exceptions to indicate emptiness. This makes it hard to extend the module; for instance OCamlPro#1058 was delayed because we were not quite sure whether the implementation of functions related to bit-vectors were correct. This patch is a reimplementation of the Intervals module from scratch. The new implementation keeps the representation used by the `intersect` function in the existing implementation (and in a way can be thought of as resolving the TODO in the existing implementation suggesting to generalize that type). It is thoroughly documented, and is split between a "core" module that provides safe functions to deal with explanations, and specialized implementations for common functions (addition, multiplication, etc.) using the "core" interface such that reasoning about the implementation of addition etc. does not require thinking about explanations at all. This makes it easier to extend the module with new specialized functions. The implementation is done through a (small) family of functors, allowing separate implementations for real and integer intervals that prevent accidentally mixing them up. For the time being, the old interface is re-implemented on top of the new interface (except where implementation details leaked too much) so as to keep the changes mostly confined to the `Intervals` module. Migrating to the new interface (and especially abandoning the use of exceptions) will be done in a second step. The patch is relatively big, but can't realistically be split into smaller parts without ending up in intermediate states full of dead code. I suggest reviewers first take a look at the documentation of the `OrderedType`, `Interval` and `Union` signatures in the `Intervals_intf` module (note that this includes some LaTeX, and might be easier to read using `odoc` -- I tried to make sure the `odoc`-generated documentation was usable). This should provide a good understanding of the "core" functionality of the new implementation. The rest of the review can be split into parts that should be mostly independent: - Implementation of the `OrderedType` interface for `Z.t` and `Q.t` in `ZEuclideanType` and `QAlgebraicType`; - Implementation of the concrete functions for addition, multiplication, etc. in the `Intervals` module; - Re-implementation of the old API in the `Intervals.Legacy` module (and minor related changes in other modules, notably `IntervalCalculus`); - Implementation of the "core" functionality in the `Intervals_core` module.

The existing Intervals module suffers from multiple drawbacks. It is undocumented, uses a questionable implementation where explanations associated with each internal bounds have unclear semantics (did I mention it is not documented), and it has been the source of many soundness bug in the past due to the way it uses exceptions to indicate emptiness. This makes it hard to extend the module; for instance OCamlPro#1058 was delayed because we were not quite sure whether the implementation of functions related to bit-vectors were correct. This patch is a reimplementation of the Intervals module from scratch. The new implementation keeps the representation used by the `intersect` futnction in the existing implementation (and in a way can be thought of as resolving the TODO in the existing implementation suggesting to generalize that type). It is thoroughly documented, and is split between a "core" module that provides safe functions to deal with explanations, and specialized implementations for common functions (addition, multiplication, etc.) using the "core" interface such that reasoning about the implementation of addition etc. does not require thinking about explanations at all. This makes it easier to extend the module with new specialized functions. The implementation is done through a (small) family of functors, allowing separate implementations for real and integer intervals that prevent accidentally mixing them up. For the time being, the old interface is re-implemented on top of the new interface (except where implementation details leaked too much) so as to keep the changes mostly confined to the `Intervals` module. Migrating to the new interface (and especially abandoning the use of exceptions) will be done in a second step. The patch is relatively big, but can't realistically be split into smaller parts without ending up in intermediate states full of dead code. I suggest reviewers first take a look at the documentation of the `OrderedType`, `Interval` and `Union` signatures in the `Intervals_intf` module (note that this includes some LaTeX, and might be easier to read using `odoc` -- I tried to make sure the `odoc`-generated documentation was usable). This should provide a good understanding of the "core" functionality of the new implementation. The rest of the review can be split into parts that should be mostly independent: - Implementation of the `OrderedType` interface for `Z.t` and `Q.t` in `ZEuclideanType` and `QAlgebraicType`; - Implementation of the concrete functions for addition, multiplication, etc. in the `Intervals` module; - Re-implementation of the old API in the `Intervals.Legacy` module (and minor related changes in other modules, notably `IntervalCalculus`); - Implementation of the "core" functionality in the `Intervals_core` module.

bclement-ocp · 2024-05-07T08:52:26Z

I have adapted the code on top of #1108 (unfortunately I messed up the rebase so the history is a bit weird, apologies for that!).

bclement-ocp · 2024-05-07T08:54:20Z

I am about 99% sure there currently are soundness bugs that can be triggered by properly crafted formulas so I am actually looking into it now. Hopefully I will not need a full rewrite to fix them :/

FWIW: We were in the 1% of chances, but the code in this PR for Intervals.extract was still wrong. Fairly confident the new one is right (and if wrong that we have a chance to catch it by reading the code).

The existing Intervals module suffers from multiple drawbacks. It is undocumented, uses a questionable implementation where explanations associated with each internal bounds have unclear semantics (did I mention it is not documented), and it has been the source of many soundness bug in the past due to the way it uses exceptions to indicate emptiness. This makes it hard to extend the module; for instance OCamlPro#1058 was delayed because we were not quite sure whether the implementation of functions related to bit-vectors were correct. This patch is a reimplementation of the Intervals module from scratch. The new implementation keeps the representation used by the `intersect` futnction in the existing implementation (and in a way can be thought of as resolving the TODO in the existing implementation suggesting to generalize that type). It is thoroughly documented, and is split between a "core" module that provides safe functions to deal with explanations, and specialized implementations for common functions (addition, multiplication, etc.) using the "core" interface such that reasoning about the implementation of addition etc. does not require thinking about explanations at all. This makes it easier to extend the module with new specialized functions. The implementation is done through a (small) family of functors, allowing separate implementations for real and integer intervals that prevent accidentally mixing them up. For the time being, the old interface is re-implemented on top of the new interface (except where implementation details leaked too much) so as to keep the changes mostly confined to the `Intervals` module. Migrating to the new interface (and especially abandoning the use of exceptions) will be done in a second step. The patch is relatively big, but can't realistically be split into smaller parts without ending up in intermediate states full of dead code. I suggest reviewers first take a look at the documentation of the `OrderedType`, `Interval` and `Union` signatures in the `Intervals_intf` module (note that this includes some LaTeX, and might be easier to read using `odoc` -- I tried to make sure the `odoc`-generated documentation was usable). This should provide a good understanding of the "core" functionality of the new implementation. The rest of the review can be split into parts that should be mostly independent: - Implementation of the `OrderedType` interface for `Z.t` and `Q.t` in `ZEuclideanType` and `QAlgebraicType`; - Implementation of the concrete functions for addition, multiplication, etc. in the `Intervals` module; - Re-implementation of the old API in the `Intervals.Legacy` module (and minor related changes in other modules, notably `IntervalCalculus`); - Implementation of the "core" functionality in the `Intervals_core` module.

* feat: Rewrite the Intervals module entirely The existing Intervals module suffers from multiple drawbacks. It is undocumented, uses a questionable implementation where explanations associated with each internal bounds have unclear semantics (did I mention it is not documented), and it has been the source of many soundness bug in the past due to the way it uses exceptions to indicate emptiness. This makes it hard to extend the module; for instance #1058 was delayed because we were not quite sure whether the implementation of functions related to bit-vectors were correct. This patch is a reimplementation of the Intervals module from scratch. The new implementation keeps the representation used by the `intersect` futnction in the existing implementation (and in a way can be thought of as resolving the TODO in the existing implementation suggesting to generalize that type). It is thoroughly documented, and is split between a "core" module that provides safe functions to deal with explanations, and specialized implementations for common functions (addition, multiplication, etc.) using the "core" interface such that reasoning about the implementation of addition etc. does not require thinking about explanations at all. This makes it easier to extend the module with new specialized functions. The implementation is done through a (small) family of functors, allowing separate implementations for real and integer intervals that prevent accidentally mixing them up. For the time being, the old interface is re-implemented on top of the new interface (except where implementation details leaked too much) so as to keep the changes mostly confined to the `Intervals` module. Migrating to the new interface (and especially abandoning the use of exceptions) will be done in a second step. The patch is relatively big, but can't realistically be split into smaller parts without ending up in intermediate states full of dead code. I suggest reviewers first take a look at the documentation of the `OrderedType`, `Interval` and `Union` signatures in the `Intervals_intf` module (note that this includes some LaTeX, and might be easier to read using `odoc` -- I tried to make sure the `odoc`-generated documentation was usable). This should provide a good understanding of the "core" functionality of the new implementation. The rest of the review can be split into parts that should be mostly independent: - Implementation of the `OrderedType` interface for `Z.t` and `Q.t` in `ZEuclideanType` and `QAlgebraicType`; - Implementation of the concrete functions for addition, multiplication, etc. in the `Intervals` module; - Re-implementation of the old API in the `Intervals.Legacy` module (and minor related changes in other modules, notably `IntervalCalculus`); - Implementation of the "core" functionality in the `Intervals_core` module.

Halbaroth · 2024-06-12T13:06:24Z

As soon as you rebase it, I will do a last pass on this PR but I think it's already good.

bclement-ocp · 2024-06-12T13:17:06Z

Rebased the whole stack.

Halbaroth · 2024-06-12T13:33:37Z

src/lib/reasoners/rel_utils.ml

  (** [map_leaves f r acc] is the "inverse" of [fold_leaves] in the sense that
      it rebuilds a domain for [r] by using [f] to access the domain for each
      of [r]'s leaves. *)


This documentation is outdated.

Done (took me a minute to realize you meant the acc argument no longer exists).

Halbaroth · 2024-06-12T13:36:25Z

src/lib/reasoners/intervals.mli

@@ -30,6 +30,8 @@

 open Intervals_intf

+val map_bound : ('a -> 'b) -> 'a bound -> 'b bound


Please add a documentation :)

Halbaroth · 2024-06-12T13:41:09Z

src/lib/reasoners/intervals_intf.ml

+  (** [scale v u] evaluates to {m \{ v \times x \mid x \in S \}} when [u]
+      evaluates to {m S}. *)


This function raises an assertion if the scalar is zero. We should mention it in its documentation.

Halbaroth · 2024-06-12T13:55:05Z

src/lib/reasoners/intervals.mli

+  (** [extract s i j] returns the bits of [s] from position [i] to [j],
+      inclusive.
+
+      Represents the function [fun x -> floor(x / 2^i) % 2^(j - i + 1)].


As this function is clear not semialgebraic, we cannot expect that the image of union of intervals is again an union of intervals. We should mention that this map compute an estimation of this image by an union of intervals.

Do you know if we compute the best approximation, that is the smallest union that contains the image?

I am not sure I understand your point about semialgebraicity. The image of an (integer) interval by this function is an union of (integer) intervals (in fact either a single interval or an union of two disjoint intervals), so the image of an union of intervals is also an union of intervals.

src/lib/reasoners/bitv_rel.ml

Halbaroth · 2024-06-12T14:36:24Z

src/lib/reasoners/bitv_rel.ml

@@ -75,6 +75,93 @@ let is_bv_ty = function

 let is_bv_r r = is_bv_ty @@ X.type_info r

+module Interval_domain : Rel_utils.Domain with type t = Intervals.Int.t = struct


For sake of uniformity, we should rename Domains into Bitlist_domains.

I wanted this patch to avoid touching the bitlist part as much as possible. Renamed it.

src/lib/reasoners/bitv_rel.ml

Halbaroth · 2024-06-12T14:54:34Z

src/lib/reasoners/bitv_rel.ml

+
+    (* Now the interval domain is stable, but the new intervals may have an
+       impact on the bitlist domains, so we must shrink them again when
+       applicable. We repeat until a fixpoint is reached. *)
    let bcs = Constraints.clear_pending bcs in


As we flush the pending constraints here, we can use the new propagate function in this loop again.

Halbaroth · 2024-06-12T14:57:00Z

src/lib/reasoners/bitv_rel.ml

+    touch_pending queue;
+    HX.iter (fun r () ->
+        HX.replace bitlist_changed r ();
+        constrain_interval_from_bitlist
+          Interval_domains.Ephemeral.(handle idom r)
+          Domains.Ephemeral.(!!(handle bdom r))
+      ) touched;
+    HX.clear touched;
+    propagate_intervals queue touched bcs idom;
+    assert (QC.is_empty queue);


src/lib/reasoners/bitv_rel.ml

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

@Halbaroth as discussed prior to my vacation this is ready for a second pass.

This patch adds interval domains to the Bitv_rel module, as well as interreductions between the bitlist and interval domains following: Sharpening Constraint Programming approaches for Bit-Vector Theory. Zakaria Chihani, Bruno Marre, François Bobot, Sébastien Bardin. CPAIOR 2017. International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, Jun 2017, Padova, Italy. More precisely: - The `Intervals` module is extended to support the `extract` operation, which is used to propagate between bit-vector compositions and their components; - The interreductions are implemented using the new `Bitlist.increase_lower_bound`, `Bitlist.decrease_upper_bound`, and the new `shared_msb` helper in `Bitv_rel`; - Propagations are performed by alternating propagations until fixpoint in each domain, followed by interreductions and propagations until fixpoint in the other domain, until reaching a fixpoint for the whole procedure. It is not clear that this is the best strategy; the goal is to try and limit interreductions since they are relatively expensive but we should revisit this once more operations are supported. For now, only the `bvule`, `bvult`, `bvugt` and `bvuge` primitives are supported as built-in bit-vector operations; other operations such as `bvadd` are still encoded using `bv2nat`. These operations will be migrated to bit-vector primitives in a follow-up PR. Finally, there are some tests for the tricky bits (`Intervals.extract` and the interreduction primitives) using QCheck.

Halbaroth

Let's merge this one :)

* feat(BV): Interval domains for bit-vectors This patch adds interval domains to the Bitv_rel module, as well as interreductions between the bitlist and interval domains following: Sharpening Constraint Programming approaches for Bit-Vector Theory. Zakaria Chihani, Bruno Marre, François Bobot, Sébastien Bardin. CPAIOR 2017. International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, Jun 2017, Padova, Italy. More precisely: - The `Intervals` module is extended to support the `extract` operation, which is used to propagate between bit-vector compositions and their components; - The interreductions are implemented using the new `Bitlist.increase_lower_bound`, `Bitlist.decrease_upper_bound`, and the new `shared_msb` helper in `Bitv_rel`; - Propagations are performed by alternating propagations until fixpoint in each domain, followed by interreductions and propagations until fixpoint in the other domain, until reaching a fixpoint for the whole procedure. It is not clear that this is the best strategy; the goal is to try and limit interreductions since they are relatively expensive but we should revisit this once more operations are supported. For now, only the `bvule`, `bvult`, `bvugt` and `bvuge` primitives are supported as built-in bit-vector operations; other operations such as `bvadd` are still encoded using `bv2nat`. These operations will be migrated to bit-vector primitives in a follow-up PR. Finally, there are some tests for the tricky bits (`Intervals.extract` and the interreduction primitives) using QCheck.

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 constraints3 branch 4 times, most recently from dc129b8 to a596fc5 Compare March 20, 2024 11:21

bclement-ocp force-pushed the constraints3 branch 2 times, most recently from c7ad3c9 to 0e39243 Compare March 22, 2024 16:09

bclement-ocp force-pushed the constraints3 branch 2 times, most recently from f8e8bba to 83dd9d7 Compare March 29, 2024 17:01

This was referenced Mar 29, 2024

feat(BV, CP): Propagators for addition and multiplication #1083

Merged

feat(BV, CP): Add propagators for bvudiv and bvurem #1084

Merged

feat(BV, CP): Add propagators for bvshl and bvlshr #1085

Merged

Halbaroth requested changes Apr 8, 2024

View reviewed changes

bclement-ocp mentioned this pull request May 6, 2024

feat: Rewrite the Intervals module entirely #1108

Merged

bclement-ocp force-pushed the constraints3 branch from 83dd9d7 to f600657 Compare May 7, 2024 08:51

bclement-ocp force-pushed the constraints3 branch from f600657 to 6d1d83b Compare May 10, 2024 07:45

bclement-ocp force-pushed the constraints3 branch from 6d1d83b to 859f4e7 Compare May 10, 2024 10:07

bclement-ocp force-pushed the constraints3 branch from 6d316b8 to 0b9051f Compare June 11, 2024 16:10

bclement-ocp mentioned this pull request Jun 11, 2024

feat(BV): Do not store width in Bitlist #1144

Merged

bclement-ocp force-pushed the constraints3 branch from 0b9051f to 713a606 Compare June 11, 2024 16:31

bclement-ocp force-pushed the constraints3 branch from 713a606 to f585fcd Compare June 12, 2024 13:15

Halbaroth requested changes Jun 12, 2024

View reviewed changes

Halbaroth reviewed Jun 12, 2024

View reviewed changes

src/lib/reasoners/bitv_rel.ml Show resolved Hide resolved

bclement-ocp requested a review from Halbaroth June 20, 2024 08:55

This was referenced Jun 20, 2024

feat(BV, CP): Add bitlist propagators for add/sub #1151

Merged

feat(BV): Only store domains on variable parts #1152

Merged

bclement-ocp added 7 commits June 20, 2024 11:23

Review comments

b9fab02

Add _bitlist prefix

96e99bd

Fix typo

a8772c2

Add documentation

5000254

Mention exception

7ef7477

Remove obsolete argument from doc

13a695c

bclement-ocp force-pushed the constraints3 branch from d06b9b0 to 13a695c Compare June 20, 2024 09:24

Bitlist_domains

143b640

Halbaroth approved these changes Jun 21, 2024

View reviewed changes

Halbaroth merged commit 5c14a39 into OCamlPro:next Jun 21, 2024
14 checks passed

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

feat(BV): Interval domains for bit-vectors #1058

feat(BV): Interval domains for bit-vectors #1058

bclement-ocp commented Mar 13, 2024 •

edited

Loading

bclement-ocp commented Mar 22, 2024

bclement-ocp commented Apr 8, 2024

bclement-ocp commented Apr 8, 2024

Halbaroth commented Apr 8, 2024

bclement-ocp commented Apr 8, 2024

Halbaroth commented Apr 8, 2024

bclement-ocp commented Apr 8, 2024

bclement-ocp commented May 7, 2024

bclement-ocp commented May 7, 2024

Halbaroth commented Jun 12, 2024

bclement-ocp commented Jun 12, 2024

Halbaroth Jun 12, 2024

bclement-ocp Jun 12, 2024

Halbaroth Jun 12, 2024

bclement-ocp Jun 12, 2024

Halbaroth Jun 12, 2024

bclement-ocp Jun 12, 2024

Halbaroth Jun 12, 2024

bclement-ocp Jun 12, 2024

Halbaroth Jun 12, 2024

bclement-ocp Jun 12, 2024

Halbaroth Jun 12, 2024

Halbaroth Jun 12, 2024

bclement-ocp commented Jun 20, 2024

Halbaroth left a comment

		@@ -30,6 +30,8 @@

		open Intervals_intf

		val map_bound : ('a -> 'b) -> 'a bound -> 'b bound

		(** [scale v u] evaluates to {m \{ v \times x \mid x \in S \}} when [u]
		evaluates to {m S}. *)

		@@ -75,6 +75,93 @@ let is_bv_ty = function

		let is_bv_r r = is_bv_ty @@ X.type_info r

		module Interval_domain : Rel_utils.Domain with type t = Intervals.Int.t = struct

feat(BV): Interval domains for bit-vectors #1058

feat(BV): Interval domains for bit-vectors #1058

Conversation

bclement-ocp commented Mar 13, 2024 • edited Loading

bclement-ocp commented Mar 22, 2024

bclement-ocp commented Apr 8, 2024

bclement-ocp commented Apr 8, 2024

Halbaroth commented Apr 8, 2024

bclement-ocp commented Apr 8, 2024

Halbaroth commented Apr 8, 2024

bclement-ocp commented Apr 8, 2024

bclement-ocp commented May 7, 2024

bclement-ocp commented May 7, 2024

Halbaroth commented Jun 12, 2024

bclement-ocp commented Jun 12, 2024

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

bclement-ocp commented Jun 20, 2024

Halbaroth left a comment

Choose a reason for hiding this comment

bclement-ocp commented Mar 13, 2024 •

edited

Loading