Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Do not use existential variables for integer division #881

Merged
merged 2 commits into from
Oct 19, 2023

Conversation

bclement-ocp
Copy link
Collaborator

This patch implements integer remainder in terms of integer division rather than the opposite. This avoids the introduction of fresh existential variables.

Fixes #875

Verified

This commit was signed with the committer’s verified signature.
rom1504 Romain Beaumont
This patch implements integer remainder in terms of integer division
rather than the opposite. This avoids the introduction of fresh
existential variables.

Fixes OCamlPro#875
@bclement-ocp
Copy link
Collaborator Author

The reasoning for this one is mostly explained in #875. Currently, we rewrite a / n (where n is a non-zero constant value) into a * (1/n) - (a % n) * (1 / n) and we rewrite a % n into a - !k * n where !k is a fresh constant for each occurrence of a % n, and we have the constraint 0 ≤ a - !k * n < |n|.

To avoid causing the creation of fresh constants, the PR flips things around: now, we rewrite a % n into a - (a / n) * n, and we just add the constraint 0 ≤ a - (a / n) * n < |n| directly whenever we encounter a / n. In addition, we rewrite a / (-n) into -(a / n) for normalization purposes — we would be able to prove it anyways, but we learn it a bit earlier this way.

let r, ctx' = X.make E.Ints.(t1 / ~$$a2) in
P.mult_const Q.m_one (embed r), ctx' @ ctx
else
(* 0 <= t1 % t2 = t1 - t2 * (t1 / t2) < |t2| *)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
(* 0 <= t1 % t2 = t1 - t2 * (t1 / t2) < |t2| *)
(* 0 <= t1 % t2 = t1 - |t2| * (t1 / t2) < |t2| *)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I prefer the version that is always true, even if in this case t2 is positive so t2 = |t2|, I will clarify.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have no strong opinion about it. For me it was clearer that the formula agrees syntactically with the code below.

Comment on lines 137 to 142
(* Compute [t1 % t2] as [t1 - |t2| * (t1 / |t2|)].

Requires: [t1], [t2] have type [Tint]
Requires: [p1] is the representative for [t1]
Requires: [p2] is the representative for [t2]
Requires: [p2] is a non-zero constant *)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The previous comment gave a precise definition of the modulo used by Arith.

  (* t1 % t2 = md  <->
     c1. 0 <= md ;
     c2. md < t2 ;
     c3. exists k. t1 = t2 * k + t ;
     c4. t2 <> 0 (already checked) *)

It's meaningful to know that we choose an integer between 0and t2 as the representative element of the equivalence classes of Z/t2Z.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

t1 % t2 here is not an equivalence class, it is defined as the remainder of euclidean division, which is an integer between 0 and |t2| by definition (note that the condition c2 in the pre-existing comment was incorrect because t2 can be negative). Should be clear with the added definition of % as remainder of Euclidean division.

P.mult_const (Q.div Q.one coef_p2) (embed r) in
P.sub p rp, ctx' @ ctx
| _ -> assert false
(* Compute [t1 % t2] as [t1 - |t2| * (t1 / |t2|)].
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know the division symbol / here means the integer division but at the first sight, it was a bit confusing as the fact t1 and t2 are integer is mentioned later. We may precise that / is the integer division?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure, added a note that / is Euclidean division here, and that % is the remainder of Euclidean division. Also renamed the function mk_euc_modulo.

let a2 = Q.to_z n2 |> Z.abs in
assert (Z.sign a2 > 0);

(* NB: [t1 % t2] = [t1 % |t2|] *)
Copy link
Collaborator

@Halbaroth Halbaroth Oct 18, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here the equality = denotes the usual equality relation between integers and this equation is consequence of our choice of representative term for the equivalence classes. I think we should clarify this point.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This follows from the definition of t1 % t2 as the remainder of euclidean division. Anyways, I have removed this to avoid recomputing X.make t1 and call mk_euc_division directly instead.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This follows from the definition of t1 % t2 as the remainder of euclidean division.

It's exactly what I said ;)

Comment on lines 167 to 170
if Q.sign n2 < 0 then
(* t1 / (-|t2|) = -(t1 / |t2|)*)
let r, ctx' = X.make E.Ints.(t1 / ~$$a2) in
P.mult_const Q.m_one (embed r), ctx' @ ctx
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If I understand well, we don't need to produce here an interval for the case n2 < 0 as the recursive call X.make will produce the appropriate interval for -n2?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, here we just rewrite t1 / (-|t2|) into -(t1 / |t2|) and then we let the recursive call take care of things. Although I am now realizing this means we will compute X.make t1 twice; I will inline the code.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually I have removed the distinction; we will create t1 / n and t1 / (-n) and rely on reasoning to prove they are identical, it is less error-prone.

@bclement-ocp bclement-ocp merged commit b8563ad into OCamlPro:next Oct 19, 2023
14 checks passed
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this pull request Nov 20, 2023
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 added a commit to bclement-ocp/alt-ergo that referenced this pull request Nov 20, 2023
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 added a commit that referenced this pull request Nov 22, 2023
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 bclement-ocp deleted the bclement/moddiv branch January 23, 2024 08:24
bclement-ocp added a commit to bclement-ocp/opam-repository that referenced this pull request Sep 24, 2024
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)
tjammer pushed a commit to tjammer/opam-repository that referenced this pull request Sep 24, 2024
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Do not use existential variables for integer division
2 participants