diff --git a/src/bv.ml b/src/bv.ml
index ce32f5cfdcce2553bf1d19ed8e24707e32d1b75d..a219dd2cb8090e8087c61065a503143932b4a31f 100644
--- a/src/bv.ml
+++ b/src/bv.ml
@@ -38,16 +38,20 @@ let debug = Debug.register_info_flag
*)
(* Bit *)
+type binop = | Bxor | Bor | Band | Bsl | Bsr
type bvexp =
-| Bxor of Cl.t * Cl.t
-| Bor of Cl.t * Cl.t
-| Band of Cl.t * Cl.t
+| Binop of binop * Cl.t * Cl.t
| Bnot of Cl.t
-| Bsl of Cl.t * Cl.t
-| Bsr of Cl.t * Cl.t
| Cst of Z.t
(* end *)
+let hash_bop a b = function
+| Bxor -> 3 * a + 5 * b
+| Bor -> 7 * a + 9 * b
+| Band -> 11 * a + 13 * b
+| Bsl -> 19 * a + 31 * b
+| Bsr -> 23 * a + 33 * b
+
let sem : bvexp sem = Sem.create_key "bv_sem"
(* BVdomain *)
@@ -158,75 +162,45 @@ module T = struct
type t = bvexp
let equal e1 e2 =
match e1,e2 with
- | Bxor (a,b), Bxor (aa,bb)
- | Bor (a,b), Bor (aa,bb)
- | Band (a,b), Band (aa,bb)
- | Bsl (a,b), Bsl (aa, bb)
- | Bsr (a,b), Bsr (aa, bb) -> Cl.equal a aa && Cl.equal b bb
+ | Binop (bop, a, b), Binop (bop', aa, bb) ->
+ (bop == bop') && Cl.equal a aa && Cl.equal b bb
| Cst i, Cst j -> Z.equal i j
| Bnot a , Bnot aa -> Cl.equal a aa
| _,_ -> false
let hash = function
- | Bxor (a,b) -> 3 * (Cl.hash a) + 5 * (Cl.hash b)
- | Bor (a,b) -> 7 * (Cl.hash a) + 9 * (Cl.hash b)
- | Band (a,b) -> 11 * (Cl.hash a) + 13 * (Cl.hash b)
+ | Binop (bop, a, b) -> hash_bop (Cl.hash a) (Cl.hash b) bop
| Bnot a -> 17 * Cl.hash a
| Cst i -> Z.hash i
- | Bsr (a,n) -> 19 * (Cl.hash a) + 31 * (Cl.hash n)
- | Bsl (a,n) -> 23 * (Cl.hash a) + 33 * (Cl.hash n)
let compare n m =
match n, m with
- | Bxor (a,b), Bxor (aa,bb) ->
- let c = Cl.compare a aa in
- if c <> 0 then c
- else Cl.compare b bb
- | Bxor _ , _ -> 1
- | _ , Bxor _ -> 1
- | Bor (a,b), Bor (aa,bb) ->
- let c = Cl.compare a aa in
- if c <> 0 then c
- else Cl.compare b bb
- | Bor _ , _ -> 1
- | _ , Bor _ -> 1
- | Band (a,b), Band (aa,bb) ->
- let c = Cl.compare a aa in
+ | Binop (bop, a, b), Binop (bop', aa, bb) ->
+ let c = compare bop bop' in
if c <> 0 then c
- else Cl.compare b bb
- | Band _ , _ -> 1
- | _ , Band _ -> 1
+ else let c = Cl.compare a aa in
+ if c <> 0 then c
+ else Cl.compare b bb
+ | Binop _ , _ -> 1
+ | _ , Binop _ -> 1
| Bnot a, Bnot aa -> Cl.compare a aa
| Bnot _, _ -> 1
| _, Bnot _ -> 1
- | Bsr (a,b), Bsr (aa,bb) ->
- let c = Cl.compare a aa in
- if c <> 0 then c
- else compare b bb
- | Bsr _, _ -> 1
- | _, Bsr _ -> 1
- | Bsl (a,b), Bsl (aa,bb) ->
- let c = Cl.compare a aa in
- if c <> 0 then c
- else compare b bb
- | Bsl _, _ -> 1
- | _, Bsl _ -> 1
| Cst i, Cst j -> Z.compare i j
+ let op_to_string = function
+ | Bxor -> "⊕"
+ | Bor -> "|"
+ | Band -> "&"
+ | Bsl -> "<<"
+ | Bsr -> ">>"
+
let print fmt (e : t)=
match e with
- | Bxor (a, b) ->
- Format.fprintf fmt "(%a) ⊕ (%a)" Cl.print a Cl.print b
- | Bor (a, b) ->
- Format.fprintf fmt "(%a) | (%a)" Cl.print a Cl.print b
- | Band (a, b) ->
- Format.fprintf fmt "(%a) & (%a)" Cl.print a Cl.print b
+ | Binop (bop, a, b) ->
+ Format.fprintf fmt ("(%a) %s (%a)") Cl.print a (op_to_string bop) Cl.print b
| Bnot a ->
Format.fprintf fmt "~(%a)" Cl.print a
- | Bsr (a, b) ->
- Format.fprintf fmt "(%a) >> (%a)" Cl.print a Cl.print b
- | Bsl (a, b) ->
- Format.fprintf fmt "(%a) << (%a)" Cl.print a Cl.print b
| Cst i -> D.print_cnst fmt i
end
@@ -288,7 +262,7 @@ type expprop =
let expprop : expprop Explanation.exp =
Explanation.Exp.create_key "Bv.prop"
-module ExpProp = struct
+module ExpProp = struct (* TODO *)
open D
type t = expprop
let key = expprop
@@ -389,11 +363,11 @@ module DaemonPropa = struct
let pexp1 = Delayed.mk_pexp d expprop (ExpInvBV (clsem, Up)) in
D.set_dom_bv d pexp cl ndcl;
D.set_dom_bv d pexp1 c ndc
- | Bor (c1, c2) -> generic_prop d or_prop clsem c1 c2
- | Band (c1, c2) -> generic_prop d and_prop clsem c1 c2
- | Bxor (c1, c2) -> generic_prop d xor_prop clsem c1 c2
- | Bsl (c, off) -> generic_shift d (Z.shift_left) (Z.shift_right) clsem c off
- | Bsr (c, off) -> generic_shift d (Z.shift_right) (Z.shift_left) clsem c off
+ | Binop (Bor, a, b) -> generic_prop d or_prop clsem a b
+ | Binop (Band, a, b) -> generic_prop d and_prop clsem a b
+ | Binop (Bxor, a, b) -> generic_prop d xor_prop clsem a b
+ | Binop (Bsl, c, off) -> generic_shift d (Z.shift_left) (Z.shift_right) clsem c off
+ | Binop (Bsr, c, off) -> generic_shift d (Z.shift_right) (Z.shift_left) clsem c off
| _ -> failwith "should be impossible"
end
| _ -> raise UnwaitedEvent
@@ -402,13 +376,9 @@ module DaemonPropa = struct
let v = ThE.sem clsem in
let ctxt = ThE.cl clsem in
match v with
- | Bor (c1,c2)
- | Band (c1, c2)
- | Bxor (c1,c2)
- | Bsr (c1,c2)
- | Bsl (c1,c2) ->
- let events = [Demon.Create.EventDom (c1,dom,clsem);
- Demon.Create.EventDom (c2,dom,clsem);
+ | Binop (_, a, b) ->
+ let events = [Demon.Create.EventDom (a,dom,clsem);
+ Demon.Create.EventDom (b,dom,clsem);
Demon.Create.EventDom (ctxt,dom,clsem)] in
Demon.Fast.attach d key events;
wakeup d (Events.Fired.EventDom(ctxt, dom, clsem))
@@ -445,7 +415,7 @@ end
module RDaemonInit = Demon.Fast.Register(DaemonInit)
-module ExpMerge = struct
+module ExpMerge = struct (* TODO *)
open D
type t = expmerge
@@ -467,7 +437,7 @@ module EM = Conflict.RegisterExp(ExpMerge)
let chobv = Explanation.Cho.create_key "Bv.cho"
-module ChoBv = struct
+module ChoBv = struct (* TODO ? *)
open Conflict
module Key = Cl
@@ -497,9 +467,9 @@ let th_register ?(with_other_theories=false) env =
(* Utilities *)
let _cnst c = index_aux (Cst (Z.of_int c))
-let _band a b = index_aux (Band (a,b))
-let _bor a b = index_aux (Bor (a,b))
-let _bxor a b = index_aux (Bxor (a,b))
-let _bsr a b = index_aux (Bsr (a,b))
-let _bsl a b = index_aux (Bsl (a,b))
+let _band a b = index_aux (Binop (Band ,a, b))
+let _bor a b = index_aux (Binop (Bor, a, b))
+let _bxor a b = index_aux (Binop (Bxor, a, b))
+let _bsr a b = index_aux (Binop (Bsr, a, b))
+let _bsl a b = index_aux (Binop (Bsl, a, b))
let _bnot a = index_aux (Bnot a)