From dc129b8f7d87da0067a95469fdd7b3ee13c9d530 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 20 Mar 2024 11:34:21 +0100 Subject: [PATCH] Paper references --- src/lib/reasoners/bitlist.ml | 9 ++++++++- src/lib/reasoners/bitv_rel.ml | 9 ++++++++- 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/src/lib/reasoners/bitlist.ml b/src/lib/reasoners/bitlist.ml index a0508da9ce..b1f6d333b4 100644 --- a/src/lib/reasoners/bitlist.ml +++ b/src/lib/reasoners/bitlist.ml @@ -153,7 +153,14 @@ let logxor b1 b2 = } (* The logic for the [increase_lower_bound] function below is described in - section 4.1 of https://cea.hal.science/cea-01795779/document *) + section 4.1 of + + 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. + https://cea.hal.science/cea-01795779/document *) (* [left_cl_can_set highest_cleared cleared_can_set] returns the least-significant bit that is: diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index f196632081..3cd0501726 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/src/lib/reasoners/bitv_rel.ml @@ -681,6 +681,12 @@ let rec shared_msb sz inf sup = (* If m and M are the minimal and maximal values of an union of intervals, the longest sequence of most significant bits shared between m and M can be fixed in the bit-vector domain; see "Is to BVs" in section 4.1 of + + 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. https://cea.hal.science/cea-01795779/document *) let constrain_bitlist_from_interval bv int = let open Domains.Ephemeral in @@ -733,7 +739,8 @@ let interval ~ex lb ub = (is_large lineq) (is_large uineq) ex ex Tint -(* Algorithm 1 from https://cea.hal.science/cea-01795779/document *) +(* Algorithm 1 from "Sharpening Constraint Programming approaches for + Bit-Vector Theory". *) let constrain_interval_from_bitlist int bv = let open Interval_domains.Ephemeral in let ex = Bitlist.explanation bv in