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

bclement-ocp · 2024-06-20T09:22:29Z

This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]).

This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations.

Note that this patch is not reverting #1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in #1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y].

The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).

Note: depends on #1144. Only the latest commit with title "feat(BV): Interval domains for bit-vectors" is included in this PR.

Benchmarks: This PR provides a small reasoning boost (+171-48 on the usual QF_BV subset) and a significant performance boost for bit-vector reasoning (-25% on the same QF_BV subset) compared to #1144.

bclement-ocp · 2024-07-29T09:41:23Z

Rebased on next. @Halbaroth ping

bclement-ocp · 2024-08-01T11:45:00Z

Note: this fixes rare crashes with bitvector fields in ADTs/records (previous implementation incorrectly assumed that X.leaves of a composition returned the bit-vectors in the composition, but that is not true if the composition contains ADT/record destructors). I tried to make a test case for it but couldn't figure out the exact conditions to trigger this (it depends on the way propagation is done so would be brittle anyways).

Halbaroth · 2024-07-22T12:28:38Z

src/lib/reasoners/bitv_rel.ml

+      Assuming [x] and [y] are bit-vectors of width 2:
+      - [101 @ x] is [x + 10100] ;
+      - [10 @ x @ 01] is [(x @ 00) + 100001] ;
+      - [10 @ y<0, 0> @ y<1, 1>] is [(y<0, 0> @ y<1>1) + 1000] ;


I do not understand the notation x<.., ...>. Is it an extraction? I guess there is a typo with y<1>1 instead of y<1, 1>?

Yes, this is the syntax that is used elsewhere in documentation comments for extraction (and indeed there is a typo, it should be y<1, 1>). I will clarify.

Halbaroth · 2024-08-01T12:20:52Z

src/lib/reasoners/rel_utils.ml

+        [domain]. The explanation [ex] justifies that the [domain] applies to
+        the entry's key.


This documentation is outdated. There is no ex argument.

True — the justification is in the domain.

src/lib/reasoners/rel_utils.ml

Halbaroth · 2024-08-01T13:38:38Z

src/lib/reasoners/rel_utils.ml

+  (** [entry t k] returns the [handle] associated with [k].
+
+      There is a unique entry associated with each key [k] that is created
+      on-the-fly when [handle t k] is called for the first time.


There is no handle function in this module. I guess you meant entry t k?

Yes, handle was renamed to entry at some point.

Halbaroth · 2024-08-01T13:39:40Z

src/lib/reasoners/rel_utils.ml

+
+      The domain associated with the entry is initialized from the underlying
+      persistent domain the first time it is accessed, and updated with
+      [update]. *)


What is update here? Cannot find it.

It should be set_domain, will fix.

src/lib/reasoners/rel_utils.ml

Halbaroth · 2024-08-01T14:28:01Z

src/lib/reasoners/rel_utils.ml

+  val add : X.t -> W.t -> t -> t
+  (** [add x w r] adds the tuple [(x, w)] to the relation. *)
+
+  val add_many : X.t -> W.Set.t -> t -> t


Please add documentation

Halbaroth · 2024-08-01T14:28:07Z

src/lib/reasoners/rel_utils.ml

+
+  val add_many : X.t -> W.Set.t -> t -> t
+
+  val range : X.t -> t -> W.Set.t


Halbaroth · 2024-08-01T14:29:46Z

src/lib/reasoners/rel_utils.ml

+    DMC.needs_propagation t.composites ||
+    not (W.Set.is_empty t.triggers)
+
+  let variables { variables ; _ } = variables


For this kind of function, I am used to add [@inline always], but I am not sure it is necessary?

It's probably going to be inlined anyways. I can add the annotation.

Halbaroth · 2024-08-01T14:30:00Z

src/lib/reasoners/rel_utils.ml

+
+  let variables { variables ; _ } = variables
+
+  let parents { parents ; _ } = parents


Same question for this one

Halbaroth · 2024-08-01T15:40:08Z

I still believe the code would be easier to read with less functors and signatures. I understand your argument. It is probably easier to write it like this for you but reading the file Rel_utils gives me the same feeling that reading Bourbaki, a bunch of abstract axioms before reaching the real stuff.

bclement-ocp

I still believe the code would be easier to read with less functors and signatures.

I have:

Removed the EphemeralMap functor that turned out not to be useful
Merged the OffsetDomain and CompositeDomain signature into the Domain signature (the goal was to be able to extend the code to domains such as ADT constructors, which don't have an offset and are never composite, but that is not really an useful generalization at the moment)
Merged AtomicType and CompositeType into the NormalForm signature (I intended to do this one prior to submitting the PR but forgot to actually do it)
Removed the UfHandle functor in favor of a Canon sub-module in Domains_make.Ephemeral
Inlined the HandleNotations functor into the EphemeralDomainMap signature (I was not really happy with this functor in the first place; the goal was to avoid code duplication for the definition of update but all solutions I found, including HandleNotations, were too clunky and verbose, and the code for update is small, so I think it's OK to duplicate here)
Renamed the BinRel functor to WatchMap to make it less abstract, and removed some functions from it that were unused.

I think the remaining abstractions (except for WatchMap) are necessary to be able to share the implementation between interval/bitlist domains and (in the future) between bit-vector/arithmetic normal forms. I am not too happy with the remaining WatchMap functor but I don't have a good solution to avoid it without significant changes.

It is probably easier to write it like this for you

It is not that it is easier to write but that I find it easier to understand code with small encapsulated abstractions. I agree I went a little overboard here though, hopefully it is better now.

reading the file Rel_utils gives me the same feeling that reading Bourbaki, a bunch of abstract axioms before reaching the real stuff.

That is a common and unfortunate side-effect of OCaml processing definitions in order, and the solution is to read from the bottom up — OCaml code reads like a research paper, out of order. I have moved the signature definitions to a new Domains_intf module, and the implementation itself to a new Domains module.

bclement-ocp · 2024-08-01T15:48:37Z

src/lib/reasoners/bitv_rel.ml

+      Assuming [x] and [y] are bit-vectors of width 2:
+      - [101 @ x] is [x + 10100] ;
+      - [10 @ x @ 01] is [(x @ 00) + 100001] ;
+      - [10 @ y<0, 0> @ y<1, 1>] is [(y<0, 0> @ y<1>1) + 1000] ;


Yes, this is the syntax that is used elsewhere in documentation comments for extraction (and indeed there is a typo, it should be y<1, 1>). I will clarify.

bclement-ocp · 2024-08-01T15:49:48Z

src/lib/reasoners/rel_utils.ml

+        [domain]. The explanation [ex] justifies that the [domain] applies to
+        the entry's key.


True — the justification is in the domain.

bclement-ocp · 2024-08-01T15:50:01Z

src/lib/reasoners/rel_utils.ml

+  (** [entry t k] returns the [handle] associated with [k].
+
+      There is a unique entry associated with each key [k] that is created
+      on-the-fly when [handle t k] is called for the first time.


Yes, handle was renamed to entry at some point.

bclement-ocp · 2024-08-01T15:50:18Z

src/lib/reasoners/rel_utils.ml

+
+      The domain associated with the entry is initialized from the underlying
+      persistent domain the first time it is accessed, and updated with
+      [update]. *)


It should be set_domain, will fix.

bclement-ocp · 2024-08-01T15:52:32Z

src/lib/reasoners/rel_utils.ml

+    DMC.needs_propagation t.composites ||
+    not (W.Set.is_empty t.triggers)
+
+  let variables { variables ; _ } = variables


It's probably going to be inlined anyways. I can add the annotation.

This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).

Co-authored-by: Pierrot <[email protected]>

bclement-ocp · 2024-08-02T15:23:39Z

Benchmarks: This PR provides a small reasoning boost (+171-48 on the usual QF_BV subset) and a significant performance boost for bit-vector reasoning (-25% on the same QF_BV subset) compared to #1144.

In the current state of both the PR and the next branch, this is now a smaller reasoning boost (+19-14, essentially a wash) and performance boost (10%, still nothing to sneer at) on the QF_BV dataset. On the J3 dataset it gives a small reasoning boost (+51-6) and larger performance boost (15%).

bclement-ocp · 2024-08-05T06:55:48Z

I am not too happy with the remaining WatchMap functor but I don't have a good solution to avoid it without significant changes.

Actually, I can just fold WatchMap to DomainsMap. Pushed a last commit that does just that. This should be ready for round 2 now @Halbaroth .

Halbaroth · 2024-08-06T07:36:45Z

Thanks for your effort, I will do a second pass now and we can merge :)

bclement-ocp force-pushed the nf3 branch 3 times, most recently from f17f2b7 to ce8559d Compare June 21, 2024 08:49

bclement-ocp force-pushed the nf3 branch from ce8559d to e83375e Compare July 1, 2024 10:11

bclement-ocp mentioned this pull request Jul 1, 2024

feat(BV): Add support for bv2nat/int2bv normal forms #1154

Merged

bclement-ocp force-pushed the nf3 branch from e83375e to 9ba6653 Compare July 9, 2024 13:13

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

bclement-ocp force-pushed the nf3 branch 4 times, most recently from 5a7abba to 8053e0c Compare July 19, 2024 15:09

bclement-ocp mentioned this pull request Jul 19, 2024

fix(BV): Do not lose explanations in bvmul #1170

Merged

bclement-ocp force-pushed the nf3 branch 2 times, most recently from baae945 to 94ad32d Compare July 29, 2024 09:39

bclement-ocp mentioned this pull request Jul 29, 2024

chore(BV, CP): Refactor propagation mechanism #1185

Merged

bclement-ocp force-pushed the nf3 branch 2 times, most recently from 0e8847f to 9cf0a67 Compare August 1, 2024 10:08

Halbaroth reviewed Aug 1, 2024

View reviewed changes

bclement-ocp commented Aug 2, 2024

View reviewed changes

bclement-ocp and others added 8 commits August 2, 2024 12:07

also watch result of constraint

a0214a8

subst must always trigger or we miss simplifications

7fe55ec

Update CHANGES

a088611

Apply suggestions from code review

b4f03dc

Co-authored-by: Pierrot <[email protected]>

Address review

36d7d0c

Remove EphemeralMap module

da6c305

Remove OffsetDomain signature

ccd0f32

bclement-ocp added 6 commits August 2, 2024 12:07

Remove AtomicType, CompositeType, CompositeDomain signatures

eaa6d53

Remove UfHandle module

979701a

Remove HandleNotations

0405a90

Make BinRel less abstract

591164a

Move signatures to Domains_intf

0d709a2

Move implementation to Domains

2c641c9

bclement-ocp force-pushed the nf3 branch from 1819911 to 2c641c9 Compare August 2, 2024 10:08

Drop WatchMap

5e01d59

Halbaroth approved these changes Aug 6, 2024

View reviewed changes

bclement-ocp merged commit 6424e77 into OCamlPro:next Aug 6, 2024
15 checks passed

bclement-ocp deleted the nf3 branch August 6, 2024 07:48

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

bclement-ocp commented Jun 20, 2024 •

edited

Loading

bclement-ocp commented Jul 29, 2024

bclement-ocp commented Aug 1, 2024

Halbaroth Jul 22, 2024

bclement-ocp Aug 1, 2024

Halbaroth Aug 1, 2024

bclement-ocp Aug 1, 2024

Halbaroth Aug 1, 2024

bclement-ocp Aug 1, 2024

Halbaroth Aug 1, 2024

bclement-ocp Aug 1, 2024

Halbaroth Aug 1, 2024

Halbaroth Aug 1, 2024

Halbaroth Aug 1, 2024

bclement-ocp Aug 1, 2024

Halbaroth Aug 1, 2024

Halbaroth commented Aug 1, 2024 •

edited

Loading

bclement-ocp left a comment

bclement-ocp Aug 1, 2024

bclement-ocp Aug 1, 2024

bclement-ocp Aug 1, 2024

bclement-ocp Aug 1, 2024

bclement-ocp Aug 1, 2024

bclement-ocp commented Aug 2, 2024

bclement-ocp commented Aug 5, 2024

Halbaroth commented Aug 6, 2024

		[domain]. The explanation [ex] justifies that the [domain] applies to
		the entry's key.


		val add_many : X.t -> W.Set.t -> t -> t

		val range : X.t -> t -> W.Set.t


		let variables { variables ; _ } = variables

		let parents { parents ; _ } = parents

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

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

Conversation

bclement-ocp commented Jun 20, 2024 • edited Loading

bclement-ocp commented Jul 29, 2024

bclement-ocp commented Aug 1, 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

Choose a reason for hiding this comment

Halbaroth commented Aug 1, 2024 • edited Loading

bclement-ocp left a 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 Aug 2, 2024

bclement-ocp commented Aug 5, 2024

Halbaroth commented Aug 6, 2024

bclement-ocp commented Jun 20, 2024 •

edited

Loading

Halbaroth commented Aug 1, 2024 •

edited

Loading