From 60469280f58de2491330fcc8179b0c2873be430e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Fri, 23 Jun 2023 12:47:57 +0200 Subject: [PATCH] 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 bb554381a142600b15bde96adcc3a9c0813edd34 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 | 149 ++++++++++++------------------- tests/issues/350.ae | 44 +++++++++ tests/issues/350.expected | 8 ++ tests/issues/664.ae | 6 ++ tests/issues/664.expected | 2 + tests/issues/dolmen/664.expected | 2 + tests/issues/dolmen/664.smt2 | 7 ++ 7 files changed, 127 insertions(+), 91 deletions(-) create mode 100644 tests/issues/350.ae create mode 100644 tests/issues/350.expected create mode 100644 tests/issues/664.ae create mode 100644 tests/issues/664.expected create mode 100644 tests/issues/dolmen/664.expected create mode 100644 tests/issues/dolmen/664.smt2 diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 7b52ab1f8..8b38b64fe 100644 --- a/src/lib/reasoners/bitv.ml +++ b/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,30 +135,21 @@ 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 @@ -167,7 +157,7 @@ module Shostak(X : ALIEN) = struct 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 + 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)} diff --git a/tests/issues/350.ae b/tests/issues/350.ae new file mode 100644 index 000000000..14ed8f66d --- /dev/null +++ b/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|] *) diff --git a/tests/issues/350.expected b/tests/issues/350.expected new file mode 100644 index 000000000..126ceb7be --- /dev/null +++ b/tests/issues/350.expected @@ -0,0 +1,8 @@ + +unsat + +unsat + +unsat + +unsat diff --git a/tests/issues/664.ae b/tests/issues/664.ae new file mode 100644 index 000000000..e52773031 --- /dev/null +++ b/tests/issues/664.ae @@ -0,0 +1,6 @@ +logic T: bitv[2] + +goal g: + ( T = [|00|] ) + or + ( [|00|] <> ( [|0|] @ T^{0,0}) ) diff --git a/tests/issues/664.expected b/tests/issues/664.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/issues/664.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/issues/dolmen/664.expected b/tests/issues/dolmen/664.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/issues/dolmen/664.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/issues/dolmen/664.smt2 b/tests/issues/dolmen/664.smt2 new file mode 100644 index 000000000..e329197eb --- /dev/null +++ b/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)