diff --git a/dolmen b/dolmen
index 7cd59bbeaa536056d19facdbdc724b104e891732..365eeab891d19457e8cc8cc103ce21d3e50b33dc 160000
--- a/dolmen
+++ b/dolmen
@@ -1 +1 @@
-Subproject commit 7cd59bbeaa536056d19facdbdc724b104e891732
+Subproject commit 365eeab891d19457e8cc8cc103ce21d3e50b33dc
diff --git a/src_colibri2/stdlib/std.ml b/src_colibri2/stdlib/std.ml
index 2ef6d9b9e8be09ca77027f09dd0bae1f8e769e6c..b2d2b158674aeeb7ba71ae40eb748ac4dac46ae6 100644
--- a/src_colibri2/stdlib/std.ml
+++ b/src_colibri2/stdlib/std.ml
@@ -110,6 +110,9 @@ module Q = struct
let is_integer q = Z.equal Z.one q.Q.den
+ let is_unsigned_integer size q =
+ is_integer q && Int.(Z.sign q.Q.num >= 0) && Int.(Z.numbits q.Q.num <= size)
+
let floor x = Q.of_bigint (Z.fdiv x.Q.num x.Q.den)
let ceil x = Q.of_bigint (Z.cdiv x.Q.num x.Q.den)
diff --git a/src_colibri2/stdlib/std.mli b/src_colibri2/stdlib/std.mli
index ac11078198b9447ee7b1238ebb4e888eb3927c54..54ec732367da2c1307d5ed48242aacb94548b7b8 100644
--- a/src_colibri2/stdlib/std.mli
+++ b/src_colibri2/stdlib/std.mli
@@ -68,6 +68,10 @@ module Q : sig
val is_integer : t -> bool
+ val is_unsigned_integer : int -> t -> bool
+ (** [is_unsigned_integer size q] checks that [q] is an integer that fits in
+ [size] bits *)
+
val none_zero : t -> t option
(** return None if the input is zero otherwise Some of the value *)
diff --git a/src_colibri2/tests/solve/smt_bv/sat/bigHex.smt2 b/src_colibri2/tests/solve/smt_bv/sat/bigHex.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..b8ae738d44128a37228cfdeef0d8b332df7d90ea
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_bv/sat/bigHex.smt2
@@ -0,0 +1,12 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_BV)
+(set-info :source |
+ Constructed by Trevor Hansen to test that #x and #b literals are working. Allocation of big constants.
+ With explicit explicit constant added.
+|)
+(set-info :category "check")
+(set-info :status sat)
+(assert (= #b1111 #xf))
+(assert (= (_ bv114813069527425452423283320117768198402231770208869520047764273682576626139237031385665948631650626991844596463898746277344711896086305533142593135616665318539129989145312280000688779148240044871428926990063486244781615463646388363947317026040466353970904996558162398808944629605623311649536164221970332681344168908984458505602379484807914058900934776500429002716706625830522008132236281291761267883317206598995396418127021779858404042159853183251540889433902091920554957783589672039160081957216630582755380425583726015528348786419432054508915275783882625175435528800822842770817965453762184851149029375 2000) (bvnot (_ bv0 2000))))
+(check-sat)
+(exit)
diff --git a/src_colibri2/tests/solve/smt_bv/sat/dune b/src_colibri2/tests/solve/smt_bv/sat/dune
new file mode 100644
index 0000000000000000000000000000000000000000..87aec8cee7b54a9b5770453bb688a103592210ab
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_bv/sat/dune
@@ -0,0 +1,12 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+ (glob_files *.cnf)
+ (glob_files *.smt2))
+ (action
+ (with-stdout-to
+ dune.inc
+ (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_bv/sat/dune.inc b/src_colibri2/tests/solve/smt_bv/sat/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..59264bcbe717ae6ff954e43682c49f27c31809cb
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_bv/sat/dune.inc
@@ -0,0 +1,6 @@
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=30s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:bigHex.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bigHex.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=30s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:unit_test.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:unit_test.smt2})))
diff --git a/src_colibri2/tests/solve/smt_bv/sat/unit_test.smt2 b/src_colibri2/tests/solve/smt_bv/sat/unit_test.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..0cd82ae2a394a347ab1b4bed51d5d6ec10c17440
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_bv/sat/unit_test.smt2
@@ -0,0 +1,102 @@
+(set-logic QF_BV)
+
+(assert (= (bvnot #b1010) #b0101))
+(assert (= (bvand #b1010 #b0001) #b0000))
+(assert (= (bvor #b1010 #b0001) #b1011))
+(assert (= (bvnand #b1010 #b0001) #b1111))
+(assert (= (bvnor #b1010 #b0001) #b0100))
+(assert (= (bvxor #b1010 #b1001) #b0011))
+(assert (= (bvxnor #b1010 #b1001) #b1100))
+
+(assert (= (bvneg (_ bv4 3)) (_ bv4 3)))
+(assert (= (bvneg (_ bv3 3)) (_ bv5 3)))
+
+(assert (= (bvcomp (_ bv3 3) (_ bv5 3)) #b0))
+(assert (= (bvcomp (_ bv4 3) (_ bv4 3)) #b1))
+
+(assert (= (bvadd (_ bv3 2) (_ bv2 2)) (_ bv1 2)))
+(assert (= (bvmul (_ bv3 2) (_ bv2 2)) (_ bv2 2)))
+
+
+(assert (= (bvudiv (_ bv3 2) (_ bv2 2)) (_ bv1 2)))
+(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
+
+(assert (= (bvudiv (_ bv7 3) (_ bv0 3)) (_ bv7 3)))
+(assert (= (bvudiv (_ bv7 3) (_ bv1 3)) (_ bv7 3)))
+(assert (= (bvudiv (_ bv7 3) (_ bv2 3)) (_ bv3 3)))
+(assert (= (bvudiv (_ bv7 3) (_ bv3 3)) (_ bv2 3)))
+(assert (= (bvudiv (_ bv7 3) (_ bv4 3)) (_ bv1 3)))
+(assert (= (bvudiv (_ bv7 3) (_ bv5 3)) (_ bv1 3)))
+(assert (= (bvudiv (_ bv7 3) (_ bv6 3)) (_ bv1 3)))
+(assert (= (bvudiv (_ bv7 3) (_ bv7 3)) (_ bv1 3)))
+
+(assert (= (bvurem (_ bv7 3) (_ bv0 3)) (_ bv7 3)))
+(assert (= (bvurem (_ bv7 3) (_ bv1 3)) (_ bv0 3)))
+(assert (= (bvurem (_ bv7 3) (_ bv2 3)) (_ bv1 3)))
+(assert (= (bvurem (_ bv7 3) (_ bv3 3)) (_ bv1 3)))
+(assert (= (bvurem (_ bv7 3) (_ bv4 3)) (_ bv3 3)))
+(assert (= (bvurem (_ bv7 3) (_ bv5 3)) (_ bv2 3)))
+(assert (= (bvurem (_ bv7 3) (_ bv6 3)) (_ bv1 3)))
+(assert (= (bvurem (_ bv7 3) (_ bv7 3)) (_ bv0 3)))
+
+(assert (= (bvsdiv (_ bv7 3) (_ bv0 3)) (_ bv1 3)))
+(assert (= (bvsdiv (_ bv7 3) (_ bv1 3)) (_ bv7 3)))
+(assert (= (bvsdiv (_ bv7 3) (_ bv2 3)) (_ bv0 3)))
+(assert (= (bvsdiv (_ bv7 3) (_ bv3 3)) (_ bv0 3)))
+(assert (= (bvsdiv (_ bv7 3) (_ bv4 3)) (_ bv0 3)))
+(assert (= (bvsdiv (_ bv7 3) (_ bv5 3)) (_ bv0 3)))
+(assert (= (bvsdiv (_ bv7 3) (_ bv6 3)) (_ bv0 3)))
+(assert (= (bvsdiv (_ bv7 3) (_ bv7 3)) (_ bv1 3)))
+
+(assert (= (bvsdiv (_ bv4 3) (_ bv0 3)) (_ bv1 3)))
+(assert (= (bvsdiv (_ bv4 3) (_ bv1 3)) (_ bv4 3)))
+(assert (= (bvsdiv (_ bv4 3) (_ bv2 3)) (_ bv6 3)))
+(assert (= (bvsdiv (_ bv4 3) (_ bv3 3)) (_ bv7 3)))
+(assert (= (bvsdiv (_ bv4 3) (_ bv4 3)) (_ bv1 3)))
+(assert (= (bvsdiv (_ bv4 3) (_ bv5 3)) (_ bv1 3)))
+(assert (= (bvsdiv (_ bv4 3) (_ bv6 3)) (_ bv2 3)))
+(assert (= (bvsdiv (_ bv4 3) (_ bv7 3)) (_ bv4 3)))
+
+(assert (= (bvsrem (_ bv4 3) (_ bv0 3)) (_ bv4 3)))
+(assert (= (bvsrem (_ bv4 3) (_ bv1 3)) (_ bv0 3)))
+(assert (= (bvsrem (_ bv4 3) (_ bv2 3)) (_ bv0 3)))
+(assert (= (bvsrem (_ bv4 3) (_ bv3 3)) (_ bv7 3)))
+(assert (= (bvsrem (_ bv4 3) (_ bv4 3)) (_ bv0 3)))
+(assert (= (bvsrem (_ bv4 3) (_ bv5 3)) (_ bv7 3)))
+(assert (= (bvsrem (_ bv4 3) (_ bv6 3)) (_ bv0 3)))
+(assert (= (bvsrem (_ bv4 3) (_ bv7 3)) (_ bv0 3)))
+
+(assert (= (bvsmod (_ bv4 3) (_ bv0 3)) (_ bv4 3)))
+(assert (= (bvsmod (_ bv4 3) (_ bv1 3)) (_ bv0 3)))
+(assert (= (bvsmod (_ bv4 3) (_ bv2 3)) (_ bv0 3)))
+(assert (= (bvsmod (_ bv4 3) (_ bv3 3)) (_ bv2 3)))
+(assert (= (bvsmod (_ bv4 3) (_ bv4 3)) (_ bv0 3)))
+(assert (= (bvsmod (_ bv4 3) (_ bv5 3)) (_ bv7 3)))
+(assert (= (bvsmod (_ bv4 3) (_ bv6 3)) (_ bv0 3)))
+(assert (= (bvsmod (_ bv4 3) (_ bv7 3)) (_ bv0 3)))
+
+(assert (= (bvshl #b100 #b001) #b000))
+(assert (= (bvlshr #b100 #b001) #b010))
+(assert (= (bvashr #b000 #b001) #b000))
+(assert (= (bvashr #b010 #b001) #b001))
+(assert (= (bvashr #b100 #b001) #b110))
+(assert (= (bvashr #b110 #b001) #b111))
+
+(assert (= ((_ sign_extend 1) #b1000) #b11000))
+(assert (= ((_ sign_extend 1) #b0100) #b00100))
+(assert (= ((_ zero_extend 1) #b1000) #b01000))
+(assert (= ((_ zero_extend 1) #b0100) #b00100))
+
+(assert (= ((_ repeat 1) #b1011) #b1011))
+(assert (= ((_ repeat 2) #b1011) #b10111011))
+
+(assert (= ((_ extract 3 2) #b1011) #b10))
+(assert (= ((_ extract 3 1) #b1011) #b101))
+
+(assert (= ((_ rotate_left 2) #b1011) #b1110))
+(assert (= ((_ rotate_right 2) #b1011) #b1110))
+(assert (= ((_ rotate_left 1) #b1011) #b0111))
+(assert (= ((_ rotate_right 1) #b1011) #b1101))
+
+(check-sat)
+(exit)
diff --git a/src_colibri2/tests/solve/smt_bv/unsat/dune b/src_colibri2/tests/solve/smt_bv/unsat/dune
new file mode 100644
index 0000000000000000000000000000000000000000..959922d115ac3b89aec38904a6221b2730b37e08
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_bv/unsat/dune
@@ -0,0 +1,12 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+ (glob_files *.cnf)
+ (glob_files *.smt2))
+ (action
+ (with-stdout-to
+ dune.inc
+ (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_bv/unsat/dune.inc b/src_colibri2/tests/solve/smt_bv/unsat/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index bc8acb837e3b4e68ba836339dec317d3aec442fd..197eb6a1890256df90f3f7b1de210063db918a04 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -100,18 +100,46 @@ let init_ty d =
else Yield (nodevalue (cst' v), Q.S.add v s))
in
Some seq
+ | { app = { builtin = Expr.Bitv n; _ }; _ } ->
+ let open Base.Sequence.Generator in
+ let rec loop i =
+ if Z.numbits i <= n then
+ yield (nodevalue (cst' (Q.of_bigint i))) >>= fun () ->
+ loop (Z.succ i)
+ else return ()
+ in
+ let seq = Interp.SeqLim.of_seq d (run (loop Z.zero)) in
+ Some seq
| _ -> None)
module Check = struct
let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
+ exception Wrong_arg
+
let compute_ground d t =
let ( !> ) t = RealValue.value (RealValue.coerce_nodevalue (interp d t)) in
+ let bitv n t =
+ let t = !>t in
+ if not (Q.is_unsigned_integer n t) then raise Wrong_arg;
+ t.Q.num
+ in
+ let signed_bitv n t = Z.signed_extract (bitv n t) 0 n in
let ( !< ) v = `Some (RealValue.nodevalue (RealValue.index v)) in
let ( !<< ) b =
let r = if b then Boolean.values_true else Boolean.values_false in
`Some r
in
+ let extract n t = !<(Q.of_bigint (Z.extract t 0 n)) in
+ let from_bitv n t =
+ let t' = Q.of_bigint t in
+ if not (Q.is_unsigned_integer n t') then
+ Fmt.epr "@[[BV] %s(%a) is not of size %i@]@."
+ (Z.format (Fmt.str "%%0+#%ib" n) t)
+ Z.pp_print t n;
+ assert (Q.is_unsigned_integer n t');
+ !<t'
+ in
match Ground.sem t with
| {
app = { builtin = Expr.Coercion };
@@ -171,27 +199,182 @@ module Check = struct
->
let a = IArray.extract1_exn args in
!<(Q.abs !>a)
+ | { app = { builtin = Expr.Bitvec s }; tyargs = []; args; ty = _ } ->
+ assert (IArray.is_empty args);
+ from_bitv (String.length s) (Z.of_string_base 2 s)
+ | { app = { builtin = Expr.Bitv_concat (n, m) }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ from_bitv (n + m) (Z.logor (Z.shift_left (bitv n a) m) (bitv m b))
+ | { app = { builtin = Expr.Bitv_extract (n, i, j) }; tyargs = []; args; _ }
+ ->
+ let a = IArray.extract1_exn args in
+ from_bitv (i - j + 1) (Z.extract (bitv n a) j (i - j + 1))
+ | { app = { builtin = Expr.Bitv_repeat (n, k) }; tyargs = []; args; _ } ->
+ let a = IArray.extract1_exn args in
+ let rec loop n k acc z =
+ if k = 0 then acc
+ else
+ let acc = Z.logor (Z.shift_left acc n) z in
+ loop n (k - 1) acc z
+ in
+ let a = bitv n a in
+ from_bitv (n * k) (loop n k Z.zero a)
+ | { app = { builtin = Expr.Bitv_zero_extend (n, k) }; tyargs = []; args; _ }
+ ->
+ let a = IArray.extract1_exn args in
+ from_bitv (n + k) (bitv n a)
+ | { app = { builtin = Expr.Bitv_sign_extend (n, k) }; tyargs = []; args; _ }
+ ->
+ let a = IArray.extract1_exn args in
+ let a = bitv n a in
+ if Z.testbit a (n - 1) then
+ extract (n + k) (Z.logor (Z.shift_left Z.minus_one n) a)
+ else from_bitv (n + k) a
+ | { app = { builtin = Expr.Bitv_rotate_left (n, k) }; tyargs = []; args; _ }
+ ->
+ let a = IArray.extract1_exn args in
+ let a = bitv n a in
+ let k = k mod n in
+ extract n (Z.logor (Z.shift_left a k) (Z.extract a (n - k) k))
+ | {
+ app = { builtin = Expr.Bitv_rotate_right (n, k) };
+ tyargs = [];
+ args;
+ _;
+ } ->
+ let a = IArray.extract1_exn args in
+ let a = bitv n a in
+ let k = k mod n in
+ extract n (Z.logor (Z.shift_left a (n - k)) (Z.shift_right a k))
+ | { app = { builtin = Expr.Bitv_not n }; tyargs = []; args; _ } ->
+ let a = IArray.extract1_exn args in
+ extract n (Z.lognot (bitv n a))
+ | { app = { builtin = Expr.Bitv_and n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ from_bitv n (Z.logand (bitv n a) (bitv n b))
+ | { app = { builtin = Expr.Bitv_or n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ from_bitv n (Z.logor (bitv n a) (bitv n b))
+ | { app = { builtin = Expr.Bitv_nand n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ extract n (Z.lognot (Z.logand (bitv n a) (bitv n b)))
+ | { app = { builtin = Expr.Bitv_nor n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ extract n (Z.lognot (Z.logor (bitv n a) (bitv n b)))
+ | { app = { builtin = Expr.Bitv_xor n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ extract n (Z.logxor (bitv n a) (bitv n b))
+ | { app = { builtin = Expr.Bitv_xnor n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ extract n (Z.logxor (bitv n a) (Z.lognot (bitv n b)))
+ | { app = { builtin = Expr.Bitv_comp n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ if Z.equal (bitv n a) (bitv n b) then extract 1 Z.minus_one
+ else from_bitv 1 Z.zero
+ | { app = { builtin = Expr.Bitv_neg n }; tyargs = []; args; _ } ->
+ let a = IArray.extract1_exn args in
+ from_bitv n (Z.sub (Z.shift_left Z.one n) (bitv n a))
+ | { app = { builtin = Expr.Bitv_add n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ extract n (Z.add (bitv n a) (bitv n b))
+ | { app = { builtin = Expr.Bitv_mul n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ extract n (Z.mul (bitv n a) (bitv n b))
+ | { app = { builtin = Expr.Bitv_udiv n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = bitv n b in
+ if Z.equal b Z.zero then extract n Z.minus_one
+ else extract n (Z.div (bitv n a) b)
+ | { app = { builtin = Expr.Bitv_urem n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = bitv n b in
+ if Z.equal b Z.zero then from_bitv n (bitv n a)
+ else extract n (Z.rem (bitv n a) b)
+ | { app = { builtin = Expr.Bitv_sdiv n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = signed_bitv n b in
+ if Z.equal b Z.zero then extract n Z.one
+ else extract n (Z.div (signed_bitv n a) b)
+ | { app = { builtin = Expr.Bitv_srem n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = signed_bitv n b in
+ if Z.equal b Z.zero then from_bitv n (bitv n a)
+ else extract n (Z.rem (signed_bitv n a) b)
+ | { app = { builtin = Expr.Bitv_smod n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = signed_bitv n b in
+ let a = signed_bitv n a in
+ if Z.equal b Z.zero then `Uninterp
+ else extract n (Z.sub a (Z.mul (Z.fdiv a b) b))
+ | { app = { builtin = Expr.Bitv_shl n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = bitv n b in
+ if Z.leq (Z.of_int n) b then from_bitv n Z.zero
+ else extract n (Z.shift_left (bitv n a) (Z.to_int b))
+ | { app = { builtin = Expr.Bitv_lshr n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = bitv n b in
+ if Z.leq (Z.of_int n) b then from_bitv n Z.zero
+ else extract n (Z.shift_right (bitv n a) (Z.to_int b))
+ | { app = { builtin = Expr.Bitv_ashr n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = bitv n b in
+ let b = if Z.leq (Z.of_int n) b then n else Z.to_int b in
+ extract n (Z.shift_right (signed_bitv n a) b)
+ | { app = { builtin = Expr.Bitv_ult n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(Z.lt (bitv n a) (bitv n b))
+ | { app = { builtin = Expr.Bitv_ule n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(Z.leq (bitv n a) (bitv n b))
+ | { app = { builtin = Expr.Bitv_ugt n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(Z.gt (bitv n a) (bitv n b))
+ | { app = { builtin = Expr.Bitv_uge n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(Z.geq (bitv n a) (bitv n b))
+ | { app = { builtin = Expr.Bitv_slt n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(Z.lt (signed_bitv n a) (signed_bitv n b))
+ | { app = { builtin = Expr.Bitv_sle n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(Z.leq (signed_bitv n a) (signed_bitv n b))
+ | { app = { builtin = Expr.Bitv_sgt n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(Z.gt (signed_bitv n a) (signed_bitv n b))
+ | { app = { builtin = Expr.Bitv_sge n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<<(Z.geq (signed_bitv n a) (signed_bitv n b))
| _ -> `None
let init d =
Interp.Register.check d (fun d t ->
- if
- Ground.Ty.equal Ground.Ty.int (Ground.sem t).ty
- && Base.Option.for_all
- ~f:(fun q -> not (Q.is_integer (RealValue.value q)))
- (RealValue.of_nodevalue (interp d (Ground.node t)))
- then Wrong
- else
- let check r = Value.equal r (interp d (Ground.node t)) in
- match compute_ground d t with
- | `None -> NA
- | `Some v -> Interp.check_of_bool (check v)
- | `Uninterp ->
- Interp.check_of_bool
- (Colibri2_theories_quantifiers.Uninterp.On_uninterpreted_domain
- .check d t));
+ match
+ ( (Ground.sem t).ty.app,
+ RealValue.of_nodevalue (interp d (Ground.node t)) )
+ with
+ | { builtin = Expr.Int; _ }, None -> Wrong
+ | { builtin = Expr.Int; _ }, Some v
+ when not (Q.is_integer (RealValue.value v)) ->
+ Wrong
+ | { builtin = Expr.Bitv _; _ }, None -> Wrong
+ | { builtin = Expr.Bitv n; _ }, Some v
+ when not (Q.is_unsigned_integer n (RealValue.value v)) ->
+ Wrong
+ | _ -> (
+ let check r = Value.equal r (interp d (Ground.node t)) in
+ match compute_ground d t with
+ | exception Wrong_arg -> Wrong
+ | `None -> NA
+ | `Some v -> Interp.check_of_bool (check v)
+ | `Uninterp ->
+ Interp.check_of_bool
+ (Colibri2_theories_quantifiers.Uninterp
+ .On_uninterpreted_domain
+ .check d t)));
Interp.Register.compute d (fun d t ->
match compute_ground d t with
+ | exception Wrong_arg -> raise Impossible
| `None -> NA
| `Some v -> Value v
| `Uninterp ->
@@ -201,6 +384,7 @@ module Check = struct
let attach d g =
let f d g =
match compute_ground d g with
+ | exception Wrong_arg -> Egraph.contradiction d
| `None -> raise Impossible
| `Some v -> Egraph.set_value d (Ground.node g) v
| `Uninterp ->
@@ -353,6 +537,175 @@ let converter d (f : Ground.t) =
let a = IArray.extract1_exn args in
reg a;
Check.attach d f
+ | { app = { builtin = Expr.Bitvec s }; tyargs = []; args; ty = _ } ->
+ assert (IArray.is_empty args);
+ merge (cst (Q.of_bigint (Z.of_string_base 2 s)))
+ | { app = { builtin = Expr.Bitv_concat (_n, _m) }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_extract (_n, _i, _j) }; tyargs = []; args; _ }
+ ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_repeat (_n, _k) }; tyargs = []; args; _ } ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_zero_extend (_n, _k) }; tyargs = []; args; _ }
+ ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_sign_extend (_n, _k) }; tyargs = []; args; _ }
+ ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_rotate_left (_n, _k) }; tyargs = []; args; _ }
+ ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ Check.attach d f
+ | {
+ app = { builtin = Expr.Bitv_rotate_right (_n, _k) };
+ tyargs = [];
+ args;
+ _;
+ } ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_not _n }; tyargs = []; args; _ } ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_and _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_or _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_nand _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_nor _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_xnor _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_comp _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_neg _n }; tyargs = []; args; _ } ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_add _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_mul _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_udiv _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_urem _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_sdiv _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_srem _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_smod _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_shl _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_lshr _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_ashr _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_ult _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_ule _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_ugt _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_uge _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_slt _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_sle _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_sgt _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
+ | { app = { builtin = Expr.Bitv_sge _n }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ Check.attach d f
| _ -> ()
let init env =