diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 4660d7e34..36976bc4c 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; @@ -83,8 +82,8 @@ type 'a alpha_term = { 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 @@ -124,30 +123,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 @@ -155,7 +145,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 @@ -182,7 +172,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 @@ -194,7 +184,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' @@ -304,7 +294,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 @@ -315,33 +305,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 @@ -642,11 +625,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] @@ -657,7 +637,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 |[] -> [] @@ -993,17 +979,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 @@ -1014,13 +994,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 @@ -1053,19 +1030,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 @@ -1090,18 +1060,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)