diff --git a/dolmen b/dolmen
index 365eeab891d19457e8cc8cc103ce21d3e50b33dc..b3a925b8c352497a06fe4565ed57d98ab1d8f85a 160000
--- a/dolmen
+++ b/dolmen
@@ -1 +1 @@
-Subproject commit 365eeab891d19457e8cc8cc103ce21d3e50b33dc
+Subproject commit b3a925b8c352497a06fe4565ed57d98ab1d8f85a
diff --git a/src_colibri2/stdlib/std.ml b/src_colibri2/stdlib/std.ml
index b2d2b158674aeeb7ba71ae40eb748ac4dac46ae6..3b063ca174711efbdad51c4d54e002f30edcc09d 100644
--- a/src_colibri2/stdlib/std.ml
+++ b/src_colibri2/stdlib/std.ml
@@ -117,6 +117,23 @@ module Q = struct
let ceil x = Q.of_bigint (Z.cdiv x.Q.num x.Q.den)
+ let truncate d = if Int.(Q.sign d > 0) then floor d else ceil d
+
+ let div_e a b =
+ let s = Q.sign b in
+ let d = Q.div a b in
+ if Int.(s > 0) then floor d else ceil d
+
+ let div_t a b = truncate (div a b)
+
+ let div_f a b = floor (div a b)
+
+ let mod_e a b = Q.sub a (div_e a b)
+
+ let mod_t a b = Q.sub a (div_t a b)
+
+ let mod_f a b = Q.sub a (div_f a b)
+
let none_zero c = if Q.equal Q.zero c then None else Some c
let is_zero c = Int.equal (Q.sign c) 0
diff --git a/src_colibri2/stdlib/std.mli b/src_colibri2/stdlib/std.mli
index 54ec732367da2c1307d5ed48242aacb94548b7b8..cf7a9e7c21f2e3d61ea930c725f467adb136b2f4 100644
--- a/src_colibri2/stdlib/std.mli
+++ b/src_colibri2/stdlib/std.mli
@@ -66,6 +66,20 @@ module Q : sig
val ceil : t -> t
+ val truncate : t -> t
+
+ val div_t : t -> t -> t
+
+ val div_e : t -> t -> t
+
+ val div_f : t -> t -> t
+
+ val mod_t : t -> t -> t
+
+ val mod_e : t -> t -> t
+
+ val mod_f : t -> t -> t
+
val is_integer : t -> bool
val is_unsigned_integer : int -> t -> bool
diff --git a/src_colibri2/theories/LRA/pivot.ml b/src_colibri2/theories/LRA/pivot.ml
index d060abb99a976099634a06e69a7125ac12a2b6df..afcc44c928273ee55c431555732c25b4899d01b4 100644
--- a/src_colibri2/theories/LRA/pivot.ml
+++ b/src_colibri2/theories/LRA/pivot.ml
@@ -314,7 +314,7 @@ end = struct
let () = Dom.register (module Th)
let get_repr d n =
- let open CCOpt in
+ let open CCOption in
let+ p = Egraph.get_dom d dom n in
p.repr
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 197eb6a1890256df90f3f7b1de210063db918a04..18a8e58ba907bda83863d6e634acd6d56f118539 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -23,14 +23,27 @@ open Colibri2_popop_lib
open Colibri2_stdlib.Std
module Builtin = struct
- type _ Expr.t += Abs_real
+ type _ Expr.t += Abs_real | BV2Nat of int
let abs_real =
Expr.Id.mk ~name:"colibri_abs_real" ~builtin:Abs_real
(Dolmen_std.Path.global "Abs")
(Expr.Ty.arrow [ Expr.Ty.real ] Expr.Ty.real)
+ let bv2nat =
+ Popop_stdlib.DInt.H.memo
+ (fun n ->
+ Expr.Id.mk ~name:"bv2nat" ~builtin:(BV2Nat n)
+ (Dolmen_std.Path.global "bv2nat")
+ (Expr.Ty.arrow [ Expr.Ty.bitv n ] Expr.Ty.int))
+ (Popop_stdlib.DInt.H.create 10)
+
let () =
+ let match_bitv_type t =
+ match Expr.Ty.expand_head (Expr.Term.ty t) with
+ | { ty_descr = Expr.TyApp ({ builtin = Builtin.Bitv i; _ }, _) } -> i
+ | _ -> raise (Expr.Term.Wrong_type (t, Expr.Ty.bitv 0))
+ in
Expr.add_builtins (fun env s ->
match s with
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "colibri_abs_real" }
@@ -40,6 +53,13 @@ module Builtin = struct
(module Dolmen_loop.Typer.T)
env s
(fun a -> Expr.Term.apply_cst abs_real [] [ a ]))
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "bv2nat" } ->
+ `Term
+ (Dolmen_type.Base.term_app1
+ (module Dolmen_loop.Typer.T)
+ env s
+ (fun a ->
+ Expr.Term.apply_cst (bv2nat (match_bitv_type a)) [] [ a ]))
| _ -> `Not_found)
end
@@ -180,6 +200,36 @@ module Check = struct
| { app = { builtin = Expr.Div }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
if Q.is_zero !>b then `Uninterp else !<(Q.div !>a !>b)
+ | { app = { builtin = Expr.Div_e }; tyargs = []; args; ty = _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = !>b in
+ let s = Q.sign b in
+ if s = 0 then `Uninterp else !<(Q.div_e !>a b)
+ | { app = { builtin = Expr.Div_f }; tyargs = []; args; ty = _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = !>b in
+ let s = Q.sign b in
+ if s = 0 then `Uninterp else !<(Q.div_f !>a b)
+ | { app = { builtin = Expr.Div_t }; tyargs = []; args; ty = _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = !>b in
+ let s = Q.sign b in
+ if s = 0 then `Uninterp else !<(Q.div_t !>a b)
+ | { app = { builtin = Expr.Modulo_e }; tyargs = []; args; ty = _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = !>b in
+ let s = Q.sign b in
+ if s = 0 then `Uninterp else !<(Q.mod_e !>a b)
+ | { app = { builtin = Expr.Modulo_f }; tyargs = []; args; ty = _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = !>b in
+ let s = Q.sign b in
+ if s = 0 then `Uninterp else !<(Q.mod_f !>a b)
+ | { app = { builtin = Expr.Modulo_t }; tyargs = []; args; ty = _ } ->
+ let a, b = IArray.extract2_exn args in
+ let b = !>b in
+ let s = Q.sign b in
+ if s = 0 then `Uninterp else !<(Q.mod_t !>a b)
| { app = { builtin = Expr.Lt }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
!<<(Q.lt !>a !>b)
@@ -345,6 +395,9 @@ module Check = struct
| { 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))
+ | { app = { builtin = Builtin.BV2Nat n }; tyargs = []; args; _ } ->
+ let a = IArray.extract1_exn args in
+ !<(Q.of_bigint (bitv n a))
| _ -> `None
let init d =
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index 3b93be733d8f436af82696e94cf1f2664bf57604..46489b54dfc1fd9b93ed8c62fcc2a9e267a7d2f9 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -155,7 +155,7 @@ let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
let s =
Opt.get_def Ground.S.empty
@@
- let open CCOpt in
+ let open CCOption in
let* info = Egraph.get_dom d Info.dom (Egraph.find_def d n) in
F.M.find_opt pf info.apps
in
@@ -198,7 +198,7 @@ let rec check_term d (subst : Ground.Subst.t) (n : Node.t) (p : t) : bool =
let s =
Opt.get_def Ground.S.empty
@@
- let open CCOpt in
+ let open CCOption in
let* info = Egraph.get_dom d Info.dom (Egraph.find_def d n) in
F.M.find_opt pf info.apps
in
@@ -239,7 +239,7 @@ let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t =
let find_app pos n =
Opt.get_def Ground.S.empty
@@
- let open CCOpt in
+ let open CCOption in
let* info = Egraph.get_dom d Info.dom (Egraph.find_def d n) in
F_Pos.M.find_opt { f = pf; pos } info.parents
in
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index 937c2285f26e29c6a3f70e1822b7835bd2b47d8a..f300a9d44a30e3a984eb974383e0e915cb5416a5 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -253,7 +253,7 @@ let application_useless d thg =
let apps =
Opt.get_def Ground.S.empty
@@
- let open CCOpt in
+ let open CCOption in
let* info = Egraph.get_dom d Info.dom (Egraph.find_def d n) in
F.M.find_opt g.app info.apps
in