Support delayed computation of partially interpreted functions (#869)

This patch lifts the existing implementation in `IntervalCalculus` for
delayed computation of the `pow` function (by "delayed computation" I
mean that we remember `pow` terms with uninterpreted arguments and
evaluate them once their arguments become interpreted). This is a
generic way of integrating functions that we know how to compute but not
necessarily how to reason about.

The patch is concerned about lifting the implementation for `pow` to a
generic one and adds `int2bv` and `bv2nat` as delayed functions (with
corresponding tests), but does not (yet) use it for other partially
interpreted functions from the arithmetic theory (e.g. `Modulo`,
`Real_of_int`, and the like); this will be done separately.

The implementation is placed in a new `Rel_utils` module that is
intended to provide scaffolding for generic behavior (such as delayed
computation) that can be useful for all relations. An alternative would
be to support delayed computation in a fully generic way in the
`Relation` module directly; providing the feature in `Rel_utils` is
(slightly) simpler and keeps things more decoupled; the implementation
can easily be moved to `Relation` later if we want to.

Fixes #801

src/lib/dune

@@ -40,7 +40,7 @@
     Fun_sat Inequalities Bitv_rel Th_util Adt Adt_rel
     Instances IntervalCalculus Intervals Ite_rel Ite Matching Matching_types
     Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml
-    Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use
+    Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use Rel_utils
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols

src/lib/reasoners/adt.ml

@@ -236,6 +236,15 @@ module Shostak (X : ALIEN) = struct
          List.fold_left (fun sx x -> SX.add x sx) sx (X.leaves r)
       )SX.empty l
 
+  let is_constant r =
+    let l = match r with
+      | Alien r -> [Hs.empty, r]
+      | Constr { c_args ; _ } ->  c_args
+      | Select { d_arg  ; _ } -> [Hs.empty, d_arg]
+      | Tester { t_arg  ; _ } -> [Hs.empty, t_arg]
+    in
+    List.for_all (fun (_, r) -> X.is_constant r) l
+
   [@@ocaml.ppwarning "TODO: not sure"]
   let fully_interpreted _ =
     false (* not sure *)

src/lib/reasoners/arith.ml

@@ -492,6 +492,8 @@ module Shostak
 
   let leaves p = P.leaves p
 
+  let is_constant p = Option.is_some (P.is_const p)
+
   let subst x t p =
     let p = P.subst x (embed t) p in
     let ty = P.type_info p in

src/lib/reasoners/arrays.ml

@@ -53,6 +53,7 @@ module Shostak (X : ALIEN) = struct
   let equal _ _      = assert false
   let hash _         = assert false
   let leaves _       = assert false
+  let is_constant _  = assert false
   let subst _ _ _    = assert false
   let make _         = assert false
   let term_extract _ = None, false

src/lib/reasoners/bitv.ml

@@ -102,6 +102,34 @@ let equal_simple_term eq = equal_alpha_term (equal_simple_term_aux eq)
 
 type 'a abstract =  'a simple_term list
 
+let rec to_Z_opt_aux acc = function
+  | [] -> Some acc
+  | { bv = Cte false; sz } :: sts ->
+    to_Z_opt_aux Z.(acc lsl sz) sts
+  | { bv = Cte true; sz } :: sts ->
+    to_Z_opt_aux Z.((acc lsl sz) + (~$1 lsl sz) - ~$1) sts
+  | _ -> None
+
+let to_Z_opt r = to_Z_opt_aux Z.zero r
+
+let int2bv_const n z =
+  (* If [z] is out of the [0 .. 2^n] range (including if [z] is negative),
+     considering only the first [n] bits is equivalent to computing [z mod 2^n],
+     so we just do that and don't bother computing the modulus. *)
+  let acc = ref [] in
+  for i = 0 to n - 1 do
+    match Z.testbit z i, !acc with
+    | false, { bv = Cte false; sz } :: rst ->
+      acc := { bv = Cte false; sz = sz + 1 } :: rst
+    | false, rst ->
+      acc := { bv = Cte false; sz = 1 } :: rst
+    | true, { bv = Cte true; sz } :: rst ->
+      acc := { bv = Cte true; sz = sz + 1 } :: rst
+    | true, rst ->
+      acc := { bv = Cte true; sz = 1 } :: rst
+  done;
+  !acc
+
 let equal_abstract eq = Lists.equal (equal_simple_term eq)
 
 (* for the solver *)
@@ -332,19 +360,8 @@ module Shostak(X : ALIEN) = struct
     and vmake ~neg tv ctx =
       match tv.descr with
       | Vcte z ->
-        let acc = ref [] in
-        for i = 0 to tv.size - 1 do
-          match Z.testbit z i, !acc with
-          | false, { bv = Cte b; sz } :: rst when Bool.equal b neg ->
-            acc := { bv = Cte b; sz = sz + 1 } :: rst
-          | false, rst ->
-            acc := { bv = Cte neg; sz = 1 } :: rst
-          | _, { bv = Cte b; sz } :: rst when Bool.equal b (not neg) ->
-            acc := { bv = Cte b; sz = sz + 1 } :: rst
-          | _, rst ->
-            acc := { bv = Cte (not neg); sz = 1 } :: rst
-        done;
-        !acc, ctx
+        let z = if neg then Z.lognot z else z in
+        int2bv_const tv.size z, ctx
       | Vother t -> other ~neg t tv.size ctx
       | Vextract (t', i, j) ->
         run ctx @@ vextract ~neg i j (view t')
@@ -1151,6 +1168,12 @@ module Shostak(X : ALIEN) = struct
          | Other t | Ext(t,_,_,_) -> (X.leaves t)@acc
       ) [] bitv
 
+  let is_constant bitv =
+    List.for_all (fun x ->
+        match x.bv with
+        | Cte _ -> true
+        | Other r | Ext (r, _, _, _) -> X.is_constant r) bitv
+
   let is_mine_opt = function [{ bv = Other r; _ }] -> Some r | _ -> None
 
   let is_mine bv =

src/lib/reasoners/bitv.mli

@@ -30,6 +30,16 @@
 
 type 'a abstract
 
+(** [to_Z_opt r] evaluates [r] to an integer if possible. *)
+val to_Z_opt : 'a abstract -> Z.t option
+
+(** [int2bv_const n z] evaluates [z] as a constant [n]-bits bitvector.
+
+    If [z] is out of the [0 .. 2^n] range, only the first [n] bits of [z] in
+    binary representation are considered, i.e.  [int2bv_const n z] is always
+    equal to [int2bv_const n (erem z (1 lsl n))]. *)
+val int2bv_const : int -> Z.t -> 'a abstract
+
 module type ALIEN = sig
   include Sig.X
   val embed : r abstract -> r

src/lib/reasoners/bitv_rel.ml

@@ -28,14 +28,50 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type t = unit
+type t = { delayed : Rel_utils.Delayed.t }
 
-let empty _ = ()
-let assume _ _ _ =
-  (), { Sig_rel.assume = []; remove = []}
+(* Currently we only compute, but in the future we may want to perform the same
+   simplifications as in [Bitv.make]. We currently don't, because we don't
+   really have a way to share code that uses polynome between the theory and the
+   relations without touching the Shostak [module rec].
+
+   Note that if we *do* want to compute here, the check for [X.is_constant] in
+   [Rel_utils.update] needs to be removed, which may have (small) performance
+   implications. *)
+let bv2nat _op bv =
+  match Bitv.to_Z_opt bv with
+  | Some n -> Some (Shostak.Polynome.create [] (Q.of_bigint n) Tint)
+  | None -> None
+
+(* [int2bv] is in the bitvector theory rather than the arithmetic theory because
+   we treat the arithmetic as more "primitive" than bit-vectors. *)
+let int2bv op p =
+  match op, Shostak.Polynome.is_const p with
+  | Symbols.Int2BV n, Some q ->
+    assert (Z.equal (Q.den q) Z.one);
+    let m = Q.to_bigint q in
+    Some (Bitv.int2bv_const n m)
+  | Int2BV _, None -> None
+  | _ -> assert false
+
+let delay1 = Rel_utils.delay1
+
+let dispatch = function
+  | Symbols.BV2Nat ->
+    Some (delay1 Shostak.Bitv.embed Shostak.Arith.is_mine bv2nat)
+  | Int2BV _ ->
+    Some (delay1 Shostak.Arith.embed Shostak.Bitv.is_mine int2bv)
+  | _ -> None
+
+let empty _ = { delayed = Rel_utils.Delayed.create dispatch }
+let assume env uf la =
+  let delayed, result = Rel_utils.Delayed.assume env.delayed uf la in
+  { delayed }, result
 let query _ _ _ = None
 let case_split _ _ ~for_model:_ = []
-let add env _ _ _ = env, []
+let add env uf r t =
+  let delayed, eqs = Rel_utils.Delayed.add env.delayed uf r t in
+  { delayed }, eqs
 let new_terms _ = Expr.Set.empty
 let instantiate ~do_syntactic_matching:_ _ env _ _ = env, []
 

src/lib/reasoners/ccx.ml

@@ -451,7 +451,7 @@ module Main : S = struct
            LRE.add (LR.make ra, aopt) e mp
         ) LRE.empty sa
     in
-    LRE.fold (fun _ e acc -> e::acc)mp []
+    LRE.fold (fun _ e acc -> e::acc) mp []
 
   let replay_atom env sa =
     Options.exec_thread_yield ();

src/lib/reasoners/enum.ml

@@ -127,6 +127,8 @@ module Shostak (X : ALIEN) = struct
 
   let leaves _ = []
 
+  let is_constant _ = true
+
   let subst p v c =
     let cr = is_mine c in
     if X.equal p cr then v