CP: Support for domains on non-leaves (#1044)

This patch re-adds support for storing domains associated with arbitrary
semantic values rather than only with leaves. In a way, it partially
reverts #1004 because some domains are not inherently structural and
cannot be stored on leaves only (for instance, we want to support
interval domains for bit-vectors, but constraints on a concatenation
cannot be propagated exactly on the elements of the concatenation).

Domains at leaves and non-leaves are connected through _structural
propagation_: when the domain of a leaf changes, the change is
propagated to the domain of the non-leaves that contains it using the
`map_leaves` function; when the domain of a non-leaf changes, the change
is propagated to the domain of the leaves it contains using the
`fold_leaves` function.

src/lib/reasoners/bitlist.ml

@@ -51,7 +51,7 @@ let ones b = { b with bits_clr = Z.zero }
 
 let zeroes b = { b with bits_set = Z.zero }
 
-let add_explanation b ex = { b with ex = Ex.union b.ex ex }
+let add_explanation ~ex b = { b with ex = Ex.union b.ex ex }
 
 let pp ppf { width; bits_set; bits_clr; ex } =
   for i = width - 1 downto 0 do
@@ -80,7 +80,7 @@ let value b = b.bits_set
 let is_fully_known b =
   Z.(equal (shift_right (bits_known b + ~$1) b.width) ~$1)
 
-let intersect b1 b2 ex =
+let intersect ~ex b1 b2 =
   let width = b1.width in
   let bits_set = Z.logor b1.bits_set b2.bits_set in
   let bits_clr = Z.logor b1.bits_clr b2.bits_clr in

src/lib/reasoners/bitlist.mli

@@ -67,8 +67,8 @@ val zeroes : t -> t
 (** [zeroes b] returns a bitlist where the one bits in [b] are replaced with
     unknown bits. *)
 
-val add_explanation : t -> Explanation.t -> t
-(** [add_explanation b ex] adds the explanation [ex] to the bitlist [b]. The
+val add_explanation : ex:Explanation.t -> t -> t
+(** [add_explanation ~ex b] adds the explanation [ex] to the bitlist [b]. The
     returned bitlist has both the explanation of [b] and [ex] as explanation. *)
 
 val bits_known : t -> Z.t
@@ -87,8 +87,8 @@ val value : t -> Z.t
     [b] is not fully known, then only the known bits (those that are set in
     [bits_known b]) are meaningful; unknown bits are set to [0]. *)
 
-val intersect : t -> t -> Explanation.t -> t
-(** [intersect b1 b2 ex] returns a new bitlist [b] that subsumes both [b1] and
+val intersect : ex:Explanation.t -> t -> t -> t
+(** [intersect ~ex b1 b2] returns a new bitlist [b] that subsumes both [b1] and
     [b2]. The explanation [ex] justifies that the two bitlists can be merged.
 
     Raises [Inconsistent] if [b1] and [b2] are not compatible (i.e. there are

src/lib/reasoners/bitv.ml

@@ -285,6 +285,8 @@ let hash_abstract hash =
 
 let negate_abstract xs = List.map negate_simple_term xs
 
+let lognot = negate_abstract
+
 type solver_simple_term = tvar alpha_term
 
 let pp_solver_simple_term = pp_alpha_term pp_tvar

src/lib/reasoners/bitv.mli

@@ -54,6 +54,8 @@ type 'a abstract = 'a simple_term list
     [size - 1 .. size - sz] inclusive. *)
 val extract : int -> int -> int -> 'a abstract -> 'a abstract
 
+val lognot : 'a abstract -> 'a abstract
+
 (** [to_Z_opt r] evaluates [r] to an integer if possible. *)
 val to_Z_opt : 'a abstract -> Z.t option