[bitv] Add support for model generation (#841)

This patch adds support for model generation in the bitvector theory.

To generate a value for a model, a simple brute-force backtracking
search amongst all possible bitvector values is performed to find one
that is different from the values that were asserted distinct. If none
can be found (or if exactly one is found, in which case the value is
forced) the `case_split` flag is set so that we report `unsat` instead
of looping during model generation.

In the future, this should be augmented with proper support for case
splits / bit-blasting in the relational theory. Note that even if we add
support for case splits in the relational theory, having an enumeration
in model generation is useful, because we may not always want to perform
case splits on large bitvector types.

src/lib/reasoners/bitv.ml

@@ -1325,14 +1325,115 @@ module Shostak(X : ALIEN) = struct
   let solve r1 r2 pb =
     Sig.{pb with sbt = List.rev_append (solve_bis r1 r2) pb.sbt}
 
-  let assign_value _ _ _ =
-    Printer.print_err
-      "[Bitv.models] assign_value currently not implemented";
-    raise (Util.Not_implemented "Models for bit-vectors")
-
-  let choose_adequate_model _ _ =
-    Printer.print_err
-      "[Bitv.models] choose_adequate_model currently not implemented";
-    raise (Util.Not_implemented "Models for bit-vectors")
+  (* Pop the first bit, raises [Not_found] if there is no first bit *)
+  let pop_bit = function
+    | [] -> raise Not_found
+    | { bv = Cte b; sz } as st :: rst ->
+      Some b, if sz > 1 then { st with sz = sz - 1 } :: rst else rst
+    | { bv = Other _ | Ext _ ; sz } as st :: rst ->
+      None, if sz > 1 then { st with sz = sz - 1 } :: rst else rst
+
+  (* Fills the segment of [buf] from [pos] to [sz] with a bitvector that is
+     different from all those in [abstracts].
+
+     Uninterpreted ("Other" and "Ext") components in [abstracts] are ignored.
+
+     Currently a fairly naive backtracking search. *)
+  let rec search buf pos sz abstracts =
+    (* [t] are the values we must be distinct from that starts with a '1' *)
+    (* [f] are the values we must be distinct from that starts with a '0' *)
+    let t, nt, f, nf = List.fold_left (fun (t, nt, f, nf) ab ->
+        let b, bv = pop_bit ab in
+        match b with
+        | Some true -> (bv :: t, 1 + nt, f, nf)
+        | Some false -> (t, nt, bv :: f, 1 + nf)
+        | None -> (t, nt, f, nf)) ([], 0, [], 0) abstracts
+    in
+    match t, f with
+    | _, [] -> Bytes.fill buf pos sz '0'
+    | [], _ -> Bytes.fill buf pos sz '1'
+    | _, _ ->
+      (* Prefer searching where there are more candidates, i.e. less
+         constraints. *)
+      let x, cx, y, cy =
+        if nt < nf then t, '1', f, '0' else f, '0', t, '1'
+      in
+      match search buf (pos + 1) (sz - 1) x with
+      | () -> Bytes.set buf pos cx
+      | exception Not_found ->
+        search buf (pos + 1) (sz - 1) y;
+        Bytes.set buf pos cy
+
+  let is_cte = function | { bv = Cte _; _ } -> true | _ -> false
+  let is_cte_abstract = List.for_all is_cte
+
+  let assign_value r distincts eq =
+    (* If we are trying to assign a value to a constant, or a term that has a
+       constant in its equivalence class, bail out *)
+    let biv = embed r in
+    if is_cte_abstract biv || List.exists
+         (fun (_, x) ->
+            match X.extract x with
+            | Some b -> is_cte_abstract b
+            | None -> false) eq
+    then None else
+      let sz = List.fold_left (fun tot { sz; _ } -> tot + sz) 0 biv in
+      (* Only try to be distinct from constants. *)
+      let distincts =
+        List.fold_left (fun acc x ->
+            let biv = embed x in
+            if is_cte_abstract biv then biv :: acc else acc) [] distincts
+      in
+      let buf = Bytes.create sz in
+      match search buf 0 sz distincts with
+      | () ->
+        (* If there are exactly [2^n - 1] constant values we must be distinct
+           from, this is not a case split: the choice is forced. *)
+        let nb =
+          List.fold_left (fun nb a ->
+              if is_cte_abstract a then nb + 1 else nb) 1 distincts
+        in
+        let is_cs = not (Z.equal (Z.of_int nb) (Z.pow (Z.of_int 2) sz)) in
+        let bv = Bytes.unsafe_to_string buf in
+        Some (E.bitv bv (Ty.Tbitv sz), is_cs)
+      | exception Not_found ->
+        (* This is not solvable: we are forced to be distinct from all possible
+           values. We signal that by returning an arbitrary bitvector and
+           setting the "case-split" flag to [false], which means that the
+           choice was "forced".
+
+           Since a forced choice is actually inconsistent, this will cause
+           backtracking (and possibly unsat-ness). *)
+        let bv = String.make sz '0' in
+        Some (E.bitv bv (Ty.Tbitv sz), false)
+
+  let choose_adequate_model t r l =
+    if Options.get_debug_interpretation () then
+      Printer.print_dbg
+        ~module_name:"Bitv" ~function_name:"choose_adequate_model"
+        "choose_adequate_model for %a" E.print t;
+    let l = List.map (fun (t, r) -> (t, r, embed r)) l in
+    let l = List.filter (fun (_, _, a) -> is_cte_abstract a) l in
+    let r, a =
+      match l with
+      | [] ->
+        let a = embed r in
+        assert (is_cte_abstract a);
+        r, a
+      | (_, r, a) :: l ->
+        List.iter (fun (_, x, _) -> assert (X.equal x r)) l;
+        r, a
+    in
+    let s =
+      List.map (function
+          | { bv = Cte b; sz } -> String.make sz (if b then '1' else '0')
+          | _ ->
+            (* Cannot happen because [a] must satisfy [is_cte_abstract] at this
+               point. *)
+            assert false
+        ) a
+      |> String.concat ""
+    in
+    r, "#b" ^ s
 
 end

src/lib/structures/ty.ml

@@ -107,7 +107,9 @@ let print_generic body_of =
       | Treal -> fprintf fmt "real"
       | Tbool -> fprintf fmt "bool"
       | Tunit -> fprintf fmt "unit"
-      | Tbitv n -> fprintf fmt "bitv[%d]" n
+      | Tbitv n ->
+        if Options.get_output_smtlib () then fprintf fmt "(_ BitVec %d)" n
+        else fprintf fmt "bitv[%d]" n
       | Tvar{v=v ; value = None} -> fprintf fmt "'a_%d" v
       | Tvar{v=v ; value = Some (Trecord { args = l; name = n; _ } as t) } ->
         if Hashtbl.mem h v then

tests/models/bitv/cardinal.models.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/models/bitv/cardinal.models.smt2

@@ -0,0 +1,9 @@
+(set-logic BV)
+(set-option :produce-models true)
+
+; Without :produce-models we say 'unknown', not 'unsat'
+(declare-const a (_ BitVec 1))
+(declare-const b (_ BitVec 1))
+(declare-const c (_ BitVec 1))
+(assert (distinct a b c))
+(check-sat)

tests/models/bitv/extract.models.expected

@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun z () (_ BitVec 1) #b0)
+  (define-fun a () (_ BitVec 2) #b11)
+  (define-fun b () (_ BitVec 3) #b111)
+  (define-fun c () (_ BitVec 6) #b111011)
+)

tests/models/bitv/extract.models.smt2

@@ -0,0 +1,18 @@
+(set-logic BV)
+(set-option :produce-models true)
+
+(declare-const a (_ BitVec 2))
+(declare-const b (_ BitVec 3))
+(declare-const c (_ BitVec 6))
+(declare-const z (_ BitVec 1))
+
+(assert (= ((_ extract 0 0) c) #b1))
+(assert (= ((_ extract 5 5) c) #b1))
+(assert (= (concat (concat b z) a) c))
+
+(assert (= ((_ extract 1 1) a) #b1))
+(assert (= ((_ extract 1 0) b) #b11))
+(assert (= z #b0))
+
+(check-sat)
+(get-model)

tests/models/bitv/specified.models.expected

@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun x () (_ BitVec 4) #b0101)
+)

tests/models/bitv/specified.models.smt2

@@ -0,0 +1,10 @@
+(set-logic BV)
+(set-option :produce-models true)
+
+(declare-const x (_ BitVec 4))
+(assert (= ((_ extract 0 0) x) #b1))
+(assert (= ((_ extract 1 1) x) #b0))
+(assert (= ((_ extract 2 2) x) #b1))
+(assert (= ((_ extract 3 3) x) #b0))
+(check-sat)
+(get-model)