Naive normalization of bitvector operators

lib/expr.ml

@@ -94,23 +94,6 @@ let get_symbols (hte : ht_expr list) =
   List.iter symbols hte;
   Hashtbl.fold (fun k () acc -> k :: acc) tbl []
 
-let negate_relop (hte : ht_expr) : (ht_expr, string) Result.t =
-  let e =
-    match hte.node.e with
-    | Relop (Eq, e1, e2) -> Ok (Relop (Ne, e1, e2))
-    | Relop (Ne, e1, e2) -> Ok (Relop (Eq, e1, e2))
-    | Relop (Lt, e1, e2) -> Ok (Relop (Ge, e1, e2))
-    | Relop (LtU, e1, e2) -> Ok (Relop (GeU, e1, e2))
-    | Relop (Le, e1, e2) -> Ok (Relop (Gt, e1, e2))
-    | Relop (LeU, e1, e2) -> Ok (Relop (GtU, e1, e2))
-    | Relop (Gt, e1, e2) -> Ok (Relop (Le, e1, e2))
-    | Relop (GtU, e1, e2) -> Ok (Relop (LeU, e1, e2))
-    | Relop (Ge, e1, e2) -> Ok (Relop (Lt, e1, e2))
-    | Relop (GeU, e1, e2) -> Ok (Relop (LtU, e1, e2))
-    | _ -> Error "negate_relop: not a relop."
-  in
-  Result.map (fun relop -> relop @: hte.node.ty) e
-
 module Pp = struct
   open Format
 
@@ -310,12 +293,22 @@ let rec simplify ?(extract = true) (hte : ht_expr) : ht_expr =
 module Bool = struct
   let v b = (match b with true -> Val True | false -> Val False) @: Ty_bool
 
-  let not (v : ht_expr) =
-    ( match v.node.e with
-    | Val True -> Val False
-    | Val False -> Val True
-    | _ -> Unop (Not, v) )
-    @: Ty_bool
+  let not (hte : ht_expr) =
+    let ty = hte.node.ty in
+    match hte.node.e with
+    | Val True -> Val False @: Ty_bool
+    | Val False -> Val True @: Ty_bool
+    | Relop (Eq, e1, e2) -> Relop (Ne, e1, e2) @: ty
+    | Relop (Ne, e1, e2) -> Relop (Eq, e1, e2) @: ty
+    | Relop (Lt, e1, e2) -> Relop (Ge, e1, e2) @: ty
+    | Relop (LtU, e1, e2) -> Relop (GeU, e1, e2) @: ty
+    | Relop (Le, e1, e2) -> Relop (Gt, e1, e2) @: ty
+    | Relop (LeU, e1, e2) -> Relop (GtU, e1, e2) @: ty
+    | Relop (Gt, e1, e2) -> Relop (Le, e1, e2) @: ty
+    | Relop (GtU, e1, e2) -> Relop (LeU, e1, e2) @: ty
+    | Relop (Ge, e1, e2) -> Relop (Lt, e1, e2) @: ty
+    | Relop (GeU, e1, e2) -> Relop (LtU, e1, e2) @: ty
+    | _ -> Unop (Not, hte) @: Ty_bool
 
   let ( = ) (b1 : ht_expr) (b2 : ht_expr) =
     ( match (b1.node.e, b2.node.e) with
@@ -345,60 +338,107 @@ module Bool = struct
     @: Ty_bool
 end
 
-module Make (T : sig
+module Make_bitv (T : sig
   type elt
 
   val ty : Ty.t
-  val num : elt -> Num.t
+  val zero : ht_expr
+  val one : ht_expr
+  val value : elt -> ht_expr
 end) =
 struct
-  let v i = Val (Num (T.num i)) @: T.ty
+  let v i = T.value i
   let sym x = mk_symbol Symbol.(x @: T.ty)
   let ( ~- ) e = Unop (Neg, e) @: T.ty
-  let ( = ) e1 e2 = Relop (Eq, e1, e2) @: T.ty
-  let ( != ) e1 e2 = Relop (Ne, e1, e2) @: T.ty
-  let ( > ) e1 e2 = Relop (Gt, e1, e2) @: T.ty
-  let ( >= ) e1 e2 = Relop (Ge, e1, e2) @: T.ty
-  let ( < ) e1 e2 = Relop (Lt, e1, e2) @: T.ty
-  let ( <= ) e1 e2 = Relop (Le, e1, e2) @: T.ty
+
+  (* TODO: Do not normalize expressions such as x <= 0 or x = 0*)
+  (* TODO: Do not create concrete abstract expressions *)
+  (* TODO: pre-processing step to order variables *)
+  (* I.e., (x > y) = (y < x) *)
+
+  (* Normalize (x = y) = (x - y = 0) *)
+  let ( = ) e1 e2 = Relop (Eq, Binop (Sub, e1, e2) @: T.ty, T.zero) @: T.ty
+
+  (* Canonize (x != y) = (x - y != 0) *)
+  let ( != ) e1 e2 = Relop (Ne, Binop (Sub, e1, e2) @: T.ty, T.zero) @: T.ty
+
+  (* Canonize (x > y) = (-x < -y) = (y - x + 1 <= 0) *)
+  let ( > ) e1 e2 =
+    let lhs = Binop (Add, Binop (Sub, e2, e1) @: T.ty, T.one) @: T.ty in
+    Relop (Le, lhs, T.zero) @: T.ty
+
+  (* Canonize (x >= y) = (-x <= -y) = (y - x <= 0) *)
+  let ( >= ) e1 e2 = Relop (Le, Binop (Sub, e2, e1) @: T.ty, T.zero) @: T.ty
+
+  (* Canonize (x < y) = (x - y + 1 <= 0) *)
+  let ( < ) e1 e2 =
+    let lhs = Binop (Add, Binop (Sub, e1, e2) @: T.ty, T.one) @: T.ty in
+    Relop (Le, lhs, T.zero) @: T.ty
+
+  (* Canonize (x <= y) = (x - y <= 0) *)
+  let ( <= ) e1 e2 = Relop (Le, Binop (Sub, e1, e2) @: T.ty, T.zero) @: T.ty
 end
 
 module Bitv = struct
-  module I8 = Make (struct
+  module I8 = Make_bitv (struct
     type elt = int
 
     let ty = Ty_bitv S8
-    let num i = Num.I8 i
+    let value i = Val (Num (I8 i)) @: ty
+    let zero = value 0
+    let one = value 1
   end)
 
-  module I32 = Make (struct
+  module I32 = Make_bitv (struct
     type elt = int32
 
     let ty = Ty_bitv S32
-    let num i = Num.I32 i
+    let value i = Val (Num (I32 i)) @: ty
+    let zero = value 0l
+    let one = value 1l
   end)
 
-  module I64 = Make (struct
+  module I64 = Make_bitv (struct
     type elt = int64
 
     let ty = Ty_bitv S64
-    let num i = Num.I64 i
+    let value i = Val (Num (I64 i)) @: ty
+    let zero = value 0L
+    let one = value 1L
   end)
 end
 
+module Make_fp (T : sig
+  type elt
+
+  val ty : Ty.t
+  val value : elt -> ht_expr
+end) =
+struct
+  let v i = T.value i
+  let sym x = mk_symbol Symbol.(x @: T.ty)
+  let ( ~- ) e = Unop (Neg, e) @: T.ty
+  let ( = ) e1 e2 = Relop (Eq, e1, e2) @: T.ty
+  let ( != ) e1 e2 = Relop (Ne, e1, e2) @: T.ty
+  let ( > ) e1 e2 = Relop (Gt, e1, e2) @: T.ty
+  let ( >= ) e1 e2 = Relop (Ge, e1, e2) @: T.ty
+  let ( < ) e1 e2 = Relop (Lt, e1, e2) @: T.ty
+  let ( <= ) e1 e2 = Relop (Le, e1, e2) @: T.ty
+end
+
 module Fpa = struct
-  module F32 = Make (struct
+  module F32 = Make_fp (struct
     type elt = float
 
     let ty = Ty_fp S32
-    let num f = Num.F32 (Int32.bits_of_float f)
+    let value f = Val (Num (F32 (Int32.bits_of_float f))) @: ty
   end)
 
-  module F64 = Make (struct
+  module F64 = Make_fp (struct
     type elt = float
 
     let ty = Ty_fp S64
-    let num f = Num.F64 (Int64.bits_of_float f)
+    let value f = Val (Num (F64 (Int64.bits_of_float f))) @: ty
   end)
 end
 

lib/expr.mli

@@ -23,7 +23,6 @@ val equal : t -> t -> bool
 val hash : t -> int
 val mk_symbol : Symbol.t -> t
 val get_symbols : t list -> Symbol.t list
-val negate_relop : t -> (t, string) Result.t
 val pp : Format.formatter -> t -> unit
 val pp_smt : Format.formatter -> t list -> unit
 val pp_list : Format.formatter -> t list -> unit

test/unit/dune

@@ -5,5 +5,6 @@
   test_hash_consing
   test_optimizer
   test_params
-  test_solver)
+  test_solver
+  test_normalization)
  (libraries encoding))

test/unit/test_normalization.ml

@@ -0,0 +1,11 @@
+open Encoding
+open Expr
+
+let () =
+  let x = Bitv.I32.sym "x" in
+  let y = Bitv.I32.sym "y" in
+  let e1 = Bitv.I32.(x > y) in
+  let e2 = Bitv.I32.(y < x) in
+  Format.printf "e1: %[email protected]: %a@." pp e1 pp e2;
+  (* Hash-consing not working?! *)
+  assert (e1 == e2)