Associate syntactic terms to bitvector variables (#685)

This is a new version of #679, which itself was a new version of #472.
A similar fix is also in #553 as bb55438

The crux of it is that the bitvector theory returns *interpreted* values
as leaves, where the rest of the solver requires leaves to be
*uninterpreted terms*.

The main difference of this patch with the other patches above is that
here we only create the fresh terms associated with variables *after*
solving, so we only create fresh terms that we do expose. On the other
hand, the solver may create many variables internally that gets split or
otherwise merged and whose associated terms would never get used.

Fixes #350
Fixes #664

src/lib/reasoners/bitv.ml

@@ -59,6 +59,11 @@ type sort_var = A | B | C
    - Each C variable appears at most once in each multi-equation, but appears
       in several (more precisely, two) distinct multi-equations. *)
 
+let pp_sort ppf = function
+  | A -> Format.fprintf ppf "a"
+  | B -> Format.fprintf ppf "b"
+  | C -> Format.fprintf ppf "c"
+
 let compare_sort s1 s2 =
   match s1, s2 with
   | A, A | B, B | C, C -> 0
@@ -67,14 +72,8 @@ let compare_sort s1 s2 =
 
 type tvar = { var : int ; sorte : sort_var }
 
-let compare_tvar v1 v2 =
-  if v1 == v2 then 0
-  else
-    let c = compare v1.var v2.var in
-    if c <> 0 then c
-    else compare_sort v1.sorte v2.sorte
-
-type 'a xterm = Var of tvar | Alien of 'a
+let pp_tvar ppf { var; sorte } =
+  Format.fprintf ppf "%a_%d" pp_sort sorte var
 
 type 'a alpha_term = {
   bv : 'a;
@@ -86,8 +85,8 @@ let equal_alpha_term eq { bv = bv1; sz = sz1 } {bv = bv2; sz = sz2 } =
 
 type 'a simple_term_aux =
   | Cte of bool
-  | Other of 'a xterm
-  | Ext of 'a xterm * int * int * int (*// id * size * i * j //*)
+  | Other of 'a
+  | Ext of 'a * int * int * int (*// id * size * i * j //*)
 
 type 'a simple_term = ('a simple_term_aux) alpha_term
 
@@ -136,38 +135,29 @@ module Shostak(X : ALIEN) = struct
     | None ->
       begin
         match X.type_info r with
-        | Ty.Tbitv n -> [{bv = Other (Alien r) ; sz = n}]
+        | Ty.Tbitv n -> [{bv = Other r ; sz = n}]
         | _  -> assert false
       end
     | Some b -> b
 
-  let compare_xterm xt1 xt2 = match xt1,xt2 with
-    | Var v1, Var v2 ->
-      let c1 = compare_sort v1.sorte v2.sorte in
-      if c1 <> 0 then c1
-      else -(compare v1.var v2.var)
-    (* on inverse le signe : les variables les plus fraiches sont
-       les plus jeunes (petites)*)
-
-    | Alien t1, Alien t2 -> X.str_cmp t1 t2
-    | Var _, Alien _ -> 1
-    | Alien _, Var _ -> -1
-
+  (* Note: we must use [x.str_cmp] here because this is used in
+     [compare_abstract] which in turn is used by [compare], which is the
+     implementation called by [X.str_cmp] itself. *)
   let compare_simple_term = compare_alpha_term (fun st1 st2 ->
       match st1, st2 with
       | Cte b1, Cte b2 -> Bool.compare b1 b2
       | Cte false , _ | _ , Cte true -> -1
       | _ , Cte false | Cte true,_ -> 1
 
-      | Other t1 , Other t2 -> compare_xterm t1 t2
+      | Other t1 , Other t2 -> X.str_cmp t1 t2
       | _ , Other _ -> -1
       | Other _ , _ -> 1
 
       | Ext(t1,s1,i1,_) , Ext(t2,s2,i2,_) ->
         let c1 = compare s1 s2 in
         if c1<>0 then c1
         else let c2 = compare i1 i2 in
-          if c2 <> 0 then c2 else compare_xterm t1 t2
+          if c2 <> 0 then c2 else X.str_cmp t1 t2
     )
 
   let compare_abstract = Lists.compare compare_simple_term
@@ -194,7 +184,7 @@ module Shostak(X : ALIEN) = struct
 
     type term_aux  =
       | I_Cte of bool
-      | I_Other of X.r xterm
+      | I_Other of X.r
       | I_Ext of term * int * int
       | I_Comp of term * term
 
@@ -206,7 +196,7 @@ module Shostak(X : ALIEN) = struct
       | I_Cte true, I_Cte _ -> 1
       | I_Cte _, I_Cte _ -> -1
 
-      | I_Other xterm1, I_Other xterm2 -> compare_xterm xterm1 xterm2
+      | I_Other xterm1, I_Other xterm2 -> X.str_cmp xterm1 xterm2
 
       | I_Ext (t, i, j), I_Ext (t', i', j') ->
         if i <> i' then i - i'
@@ -316,7 +306,7 @@ module Shostak(X : ALIEN) = struct
         | { E.ty = Ty.Tbitv n; _ } ->
           let r', ctx' = X.make t' in
           let ctx = ctx' @ ctx in
-          {bv = I_Other (Alien r') ; sz = n}, ctx
+          {bv = I_Other r' ; sz = n}, ctx
         | _ -> assert false
       in
       let r, ctx = make_rec t [] in
@@ -327,33 +317,26 @@ module Shostak(X : ALIEN) = struct
   module Debug = struct
     open Printer
 
-    let print_tvar fmt ({var=v;sorte=s},sz) =
-      Format.fprintf fmt "%s_%d[%d]@?"
-        (match s with | A -> "a" | B -> "b" | C -> "c")
-        v sz
-
-    (* unused
-       open Canonizer
-       let rec print_I_ast fmt ast = match ast.bv with
-       | I_Cte b -> fprintf fmt "%d[%d]@?" (if b then 1 else 0) ast.sz
-       | I_Other (Alien t) -> fprintf fmt "%a[%d]@?" X.print t ast.sz
-       | I_Other (Var tv) -> fprintf fmt "%a@?" print_tvar (tv,ast.sz)
-       | I_Ext (u,i,j) -> fprintf fmt "%a<%d,%d>@?" print_I_ast u i j
-       | I_Comp(u,v) -> fprintf fmt "@[(%a * %a)@]" print_I_ast u print_I_ast v
-    *)
+    let print_tvar fmt (tv,sz) =
+      Format.fprintf fmt "%a[%d]@?" pp_tvar tv sz
 
     let print fmt ast =
       let open Format in
       match ast.bv with
       | Cte b -> fprintf fmt "%d[%d]@?" (if b then 1 else 0) ast.sz
-      | Other (Alien t) -> fprintf fmt "%a@?" X.print t
-      | Other (Var tv) -> fprintf fmt "%a@?" print_tvar (tv,ast.sz)
-      | Ext (Alien t,_,i,j) ->
+      | Other t -> fprintf fmt "%a@?" X.print t
+      | Ext (t,_,i,j) ->
         fprintf fmt "%a@?" X.print t;
         fprintf fmt "<%d,%d>@?" i j
-      | Ext (Var tv,_,i,j) ->
-        fprintf fmt "%a@?" print_tvar (tv,ast.sz);
-        fprintf fmt "<%d,%d>@?" i j
+
+    let[@warning "-32"] rec print_I_ast fmt ast =
+      let open Canonizer in
+      let open Format in
+      match ast.bv with
+      | I_Cte b -> fprintf fmt "%d[%d]@?" (if b then 1 else 0) ast.sz
+      | I_Other t -> fprintf fmt "%a[%d]@?" X.print t ast.sz
+      | I_Ext (u,i,j) -> fprintf fmt "%a<%d,%d>@?" print_I_ast u i j
+      | I_Comp(u,v) -> fprintf fmt "@[(%a * %a)@]" print_I_ast u print_I_ast v
 
     let print_C_ast fmt = function
         [] -> assert false
@@ -654,11 +637,8 @@ module Shostak(X : ALIEN) = struct
       let c_solve (st1,st2) = match st1.bv,st2.bv with
         |Cte _, Cte _ -> raise Util.Unsolvable (* forcement un 1 et un 0 *)
 
-        |Cte b, Other (Var _) -> [cte_vs_other b st2]
-        |Other (Var _), Cte b -> [cte_vs_other b st1]
-
-        |Cte b, Other (Alien _) -> [cte_vs_other b st2]
-        |Other (Alien _), Cte b -> [cte_vs_other b st1]
+        |Cte b, Other _ -> [cte_vs_other b st2]
+        |Other _, Cte b -> [cte_vs_other b st1]
 
         |Cte b, Ext(xt,s_xt,i,j) -> [cte_vs_ext b xt s_xt i j]
         |Ext(xt,s_xt,i,j), Cte b -> [cte_vs_ext b xt s_xt i j]
@@ -669,7 +649,7 @@ module Shostak(X : ALIEN) = struct
 
         |Ext(xt,s_xt,i,j), Other _ -> other_vs_ext st2 xt s_xt i j
         |Ext(id,s,i,j), Ext(id',s',i',j') ->
-          if compare_xterm id id' <> 0
+          if not (X.equal id id')
           then ext1_vs_ext2 (id,s,i,j) (id',s',i',j')
           else [ext_vs_ext id s (if i<i' then (i,i') else (i',i)) (j - i + 1)]
 
@@ -1024,18 +1004,24 @@ module Shostak(X : ALIEN) = struct
        solution to the uniform system by replacing each term with the
        concatenation of representatives for the corresponding multi-equation. *)
     let build_solution unif_slic sets =
+      let tvars =
+        List.map (fun (r, set) ->
+            let r =
+              match r.bv with
+              | S_Cte b -> Cte b
+              | S_Var _ ->
+                let t = E.fresh_name (Ty.Tbitv r.sz) in
+                Other (X.term_embed t)
+            in
+            (r, set)) sets
+      in
       let get_rep var =
-        fst(List.find ( fun(_,set)->ST_Set.mem var set ) sets) in
+        fst(List.find ( fun(_,set)->ST_Set.mem var set ) tvars) in
       let to_external_ast v =
         {sz = v.sz;
          bv = match v.bv with
            |S_Cte b -> Cte b
-           |S_Var _ ->
-             begin
-               match (get_rep v).bv with
-               |S_Cte b -> Cte b
-               |S_Var tv -> Other (Var tv)
-             end
+           |S_Var _ -> get_rep v
         }in
       let rec cnf_max l = match l with
         |[] -> []
@@ -1106,17 +1092,11 @@ module Shostak(X : ALIEN) = struct
   (* should use hashed compare to be faster, not structural comparison *)
   let equal bv1 bv2 = compare_mine bv1 bv2 = 0
 
-  let hash_xterm = function
-    | Var {var = i; sorte = A} -> 11 * i
-    | Var {var = i; sorte = B} -> 17 * i
-    | Var {var = i; sorte = C} -> 19 * i
-    | Alien r -> 23 * X.hash r
-
   let hash_simple_term_aux = function
     | Cte b -> 11 * Hashtbl.hash b
-    | Other x -> 17 * hash_xterm x
+    | Other x -> 17 * X.hash x
     | Ext (x, a, b, c) ->
-      hash_xterm x + 19 * (a + b + c)
+      X.hash x + 19 * (a + b + c)
 
   let hash l =
     List.fold_left
@@ -1127,13 +1107,10 @@ module Shostak(X : ALIEN) = struct
       (fun acc x ->
          match x.bv with
          | Cte _  -> acc
-         | Ext( Var v,sz,_,_) ->
-           (X.embed [{bv=Other (Var v) ; sz = sz }])::acc
-         | Other (Var _)  -> (X.embed [x])::acc
-         | Other (Alien t) | Ext(Alien t,_,_,_) -> (X.leaves t)@acc
+         | Other t | Ext(t,_,_,_) -> (X.leaves t)@acc
       ) [] bitv
 
-  let is_mine = function [{ bv = Other (Alien r); _ }] -> r | bv -> X.embed bv
+  let is_mine = function [{ bv = Other r; _ }] -> r | bv -> X.embed bv
 
   let print = Debug.print_C_ast
 
@@ -1166,19 +1143,12 @@ module Shostak(X : ALIEN) = struct
   let extract r ty =
     match X.extract r with
       Some (_::_ as bv) -> to_i_ast bv
-    | None -> {bv =  Canonizer.I_Other (Alien r); sz = ty}
+    | None -> {bv =  Canonizer.I_Other r; sz = ty}
     | Some [] -> assert false
 
-  let extract_xterm r =
-    match X.extract r with
-      Some ([{ bv = Other (Var _ as x); _ }]) -> x
-    | None -> Alien r
-    | _ -> assert false
-
   let var_or_term x =
     match x.bv with
-      Other (Var _) -> X.embed [x]
-    | Other (Alien r) -> r
+    | Other r -> r
     | _ -> assert false
 
 
@@ -1203,18 +1173,15 @@ module Shostak(X : ALIEN) = struct
 
 
   let rec subst_rec x subs biv =
-    match biv.bv , extract_xterm x with
-    | Canonizer.I_Cte _ , _ -> biv
-    | Canonizer.I_Other (Var y), Var z when compare_tvar y z = 0 ->
-      extract subs biv.sz
-    | Canonizer.I_Other (Var _) , _ -> biv
-    | Canonizer.I_Other (Alien tt) , _ ->
+    match biv.bv with
+    | Canonizer.I_Cte _ -> biv
+    | Canonizer.I_Other tt ->
       if X.equal x tt then
         extract subs biv.sz
       else extract (X.subst x subs tt) biv.sz
-    | Canonizer.I_Ext (t,i,j) , _ ->
+    | Canonizer.I_Ext (t,i,j) ->
       { biv with bv = Canonizer.I_Ext(subst_rec x subs t,i,j) }
-    | Canonizer.I_Comp (u,v) , _ ->
+    | Canonizer.I_Comp (u,v) ->
       { biv with
         bv = Canonizer.I_Comp(subst_rec x subs u ,subst_rec x subs v)}
 

tests/issues/350.ae

@@ -0,0 +1,44 @@
+(** Constants of bitv[1] *)
+
+logic b0:bitv[1]
+axiom b0_def: b0=[|0|]
+logic b1:bitv[1]
+axiom b1_def: b1=[|1|]
+
+(** Conversion functions bool<->bitv[|1|] *)
+
+function bit_of_bool(x:bool):bitv[1] =
+    if x then b1 else b0
+
+function bool_of_bit(x:bitv[1]):bool =
+    x=b1
+
+(** Boolean functions on bitv[|1|] *)
+
+function bnot(x:bitv[1]):bitv[1] =
+    bit_of_bool(not bool_of_bit(x))
+
+function band(x:bitv[1], y:bitv[1]):bitv[1] =
+    bit_of_bool(bool_of_bit(x) and bool_of_bit(y))
+
+function bor(x:bitv[1], y:bitv[1]):bitv[1] =
+    bit_of_bool(bool_of_bit(x) or bool_of_bit(y))
+
+(** Boolean functions on bitv *)
+
+(** Not *)
+function b2not(x:bitv[2]):bitv[2] =
+    bnot(x^{1,1})@bnot(x^{0,0})
+function b4not(x:bitv[4]):bitv[4] =
+    b2not(x^{2,3})@b2not(x^{0,1})
+function b8not(x:bitv[8]):bitv[8] =
+    b4not(x^{4,7})@b4not(x^{0,3})
+function b16not(x:bitv[16]):bitv[16] =
+    b8not(x^{8,15})@b8not(x^{0,7})
+
+goal gn:   bnot([|1|]) = [|0|]
+goal gn2:  not(b2not([|10|])=[|00|])
+goal gn4:  b4not([|1001|])=[|0110|]
+(* Start bugging at this line *)
+goal gn8:  b8not([|10001111|])=[|01110000|]
+(* goal gn16: b16not([|1000100011111111|])=[|0111011100000000|] *)

tests/issues/350.expected

@@ -0,0 +1,8 @@
+
+unsat
+
+unsat
+
+unsat
+
+unsat

tests/issues/664.ae

@@ -0,0 +1,6 @@
+logic T: bitv[2]
+
+goal g:
+    ( T = [|00|] )
+  or
+    ( [|00|] <> ( [|0|] @ T^{0,0}) )

tests/issues/664.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/issues/dolmen/664.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/issues/dolmen/664.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_BV)
+(declare-fun T () (_ BitVec 2))
+(assert
+  (and
+    (distinct T (_ bv0 2))
+    (= (_ bv0 2) (concat (_ bv0 1) ((_ extract 0 0) T)))))
+(check-sat)