diff --git a/dolmen b/dolmen
index 57c66b6b6de28af0a7b9d0fe429bfacdca05f8d9..660c77c855d8b7441f6aec56c84c54e46229bc15 160000
--- a/dolmen
+++ b/dolmen
@@ -1 +1 @@
-Subproject commit 57c66b6b6de28af0a7b9d0fe429bfacdca05f8d9
+Subproject commit 660c77c855d8b7441f6aec56c84c54e46229bc15
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index 3031ec4dd9db7c5af4b85b034ab92b9d4a5cc61e..61c249fd4e4dc77a5ea9f8ac1bce44658a59c675 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -89,7 +89,9 @@ module Ty = struct
(fun i ->
assert (i > 0);
Expr.(
- Id.mk ~builtin:Arrow "arrow" { arity = i + 1; alias = No_alias }))
+ Id.mk ~builtin:Arrow
+ (Dolmen_std.Path.global "arrow")
+ { arity = i + 1; alias = No_alias }))
cache i
in
match ret.app.builtin with
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index d3ed0f98a08990a1001f6f656f47935a00e75888..f5a2c0905bfc8d88529e726ef9878fb25c4e3415 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -314,7 +314,12 @@ let handle_stmt ?(show_check_sat_result = true) ?(show_steps = false)
Term.term =
App
( {
- term = Symbol { Id.ns = Id.Attr; Id.name = ":status-colibri2" };
+ term =
+ Symbol
+ {
+ Id.ns = Namespace.Attr;
+ Id.name = Simple ":status-colibri2";
+ };
_;
},
args );
@@ -322,13 +327,13 @@ let handle_stmt ?(show_check_sat_result = true) ?(show_steps = false)
_;
} -> (
match args with
- | [ { term = Symbol { name = "sat"; _ }; _ } ] ->
+ | [ { term = Symbol { name = Simple "sat"; _ }; _ } ] ->
Context.Ref.set st.solve_state.status_colibri `Sat
- | [ { term = Symbol { name = "unsat"; _ }; _ } ] ->
+ | [ { term = Symbol { name = Simple "unsat"; _ }; _ } ] ->
Context.Ref.set st.solve_state.status_colibri `Unsat
- | [ { term = Symbol { name = "unknown"; _ }; _ } ] ->
+ | [ { term = Symbol { name = Simple "unknown"; _ }; _ } ] ->
Context.Ref.set st.solve_state.status_colibri `Unknown
- | [ { term = Symbol { name = "steplimitreached"; _ }; _ } ] ->
+ | [ { term = Symbol { name = Simple "steplimitreached"; _ }; _ } ] ->
Context.Ref.set st.solve_state.status_colibri `StepLimitReached
| _ -> error st loc "Expected sat|unsat|unknown")
| `Set_info _ -> ()
diff --git a/src_colibri2/tests/tests_lib.ml b/src_colibri2/tests/tests_lib.ml
index 7ba0f3c77d9d833e2c2a2f44267040636d5009f2..59675e82ecee0bde4a5cd39599da3b00a8ca93ca 100644
--- a/src_colibri2/tests/tests_lib.ml
+++ b/src_colibri2/tests/tests_lib.ml
@@ -24,8 +24,8 @@ open Colibri2_core
let debug = Debug.register_flag
~desc:" Run the test in verbose mode." "ounit"
-let fresht ty s = Expr.Term.apply_cst (Expr.Term.Const.mk s ty) [] []
-let fresh ty s = Ground.convert (Expr.Term.apply_cst (Expr.Term.Const.mk s ty) [] [])
+let fresht ty s = Expr.Term.apply_cst (Expr.Term.Const.mk (Dolmen_std.Path.global s) ty) [] []
+let fresh ty s = Ground.convert (Expr.Term.apply_cst (Expr.Term.Const.mk (Dolmen_std.Path.global s) ty) [] [])
let (&:) s l = s >::: (List.map (fun f -> OUnit2.test_case f) l)
diff --git a/src_colibri2/tests/tests_uf.ml b/src_colibri2/tests/tests_uf.ml
index ef8848c21e5e599da856cd9f5d17d5fd577fc532..3cc921045f89ac8021062f4b6c1a9dc1929ea897 100644
--- a/src_colibri2/tests/tests_uf.ml
+++ b/src_colibri2/tests/tests_uf.ml
@@ -80,7 +80,7 @@ let noteq _ =
let basic = "Uf.Basic" >::: ["empty" >:: empty; "tauto" >:: tauto;
"trans" >:: trans; "noteq" >:: noteq]
-let f = Expr.Term.Const.mk "f" (Expr.Ty.arrow [Ty.bool] Ty.bool)
+let f = Expr.Term.Const.mk (Dolmen_std.Path.global "f") (Expr.Ty.arrow [Ty.bool] Ty.bool)
let f x = Expr.Term.apply_cst f [] [x]
let fa = Ground.convert @@ f ta
let fb = Ground.convert @@ f tb
@@ -157,7 +157,7 @@ let congru1 = "Uf.Congru 1 arg" >::: ["refl" >:: refl;"congru" >:: congru;
"2level" >:: _2level; "2level'" >:: _2level';
"bigger" >:: bigger]
let (!!) = Ground.convert
-let g = Expr.Term.Const.mk "g" (Expr.Ty.arrow [Ty.bool;Ty.bool] Ty.bool)
+let g = Expr.Term.Const.mk (Dolmen_std.Path.global "g") (Expr.Ty.arrow [Ty.bool;Ty.bool] Ty.bool)
let g a b = Expr.Term.apply_cst g [] [a;b]
let gab = g ta tb
let gaa = g ta ta
@@ -217,9 +217,9 @@ let x = fresht Ty.bool "x"
let y = fresht Ty.bool "y"
let altergo0 _ =
- let h = Expr.Term.Const.mk "h" (Expr.Ty.arrow [Ty.bool] Ty.bool) in
+ let h = Expr.Term.Const.mk (Dolmen_std.Path.global "h") (Expr.Ty.arrow [Ty.bool] Ty.bool) in
let h x = Expr.Term.apply_cst h [] [x] in
- let g = Expr.Term.Const.mk "g" (Expr.Ty.arrow [Ty.bool;Ty.bool] Ty.bool) in
+ let g = Expr.Term.Const.mk (Dolmen_std.Path.global "g") (Expr.Ty.arrow [Ty.bool;Ty.bool] Ty.bool) in
let g x y = Expr.Term.apply_cst g [] [x;y] in
let gax = g ta x in
let hx = h x in
@@ -235,7 +235,7 @@ let altergo0 _ =
(is_equal env !!ggahxx a)
let altergo1 _ =
- let h = Expr.Term.Const.mk "h" (Expr.Ty.arrow [Ty.bool;Ty.bool] Ty.bool) in
+ let h = Expr.Term.Const.mk (Dolmen_std.Path.global "h") (Expr.Ty.arrow [Ty.bool;Ty.bool] Ty.bool) in
let h x y = Expr.Term.apply_cst h [] [x;y] in
let rec bf n = if n < 1 then ta else f (bf (n-1)) in
let fffa = bf 3 in
@@ -259,7 +259,7 @@ let altergo1 _ =
(is_equal env !!hggxyya !!hxfa)
let altergo2 _ =
- let h = Expr.Term.Const.mk "h" (Expr.Ty.arrow [Ty.bool;Ty.bool] Ty.bool) in
+ let h = Expr.Term.Const.mk (Dolmen_std.Path.global "h") (Expr.Ty.arrow [Ty.bool;Ty.bool] Ty.bool) in
let h x y = Expr.Term.apply_cst h [] [x;y] in
let gxy = g x y in
let fa = f ta in
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 62dd5b8c003c4ffd77c2a113d8d9a22bee59ff46..d4002abf082b0aacbcf710f8c00c3cfcfc3de019 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -26,17 +26,19 @@ module Builtin = struct
type _ Expr.t += Abs_real
let abs_real =
- Expr.Id.mk ~name:"colibri_abs_real" ~builtin:Abs_real "Abs"
+ 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 () =
Expr.add_builtins (fun env s ->
match s with
- | Dolmen_loop.Typer.T.Id { ns = Term; name = "colibri_abs_real" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "colibri_abs_real" }
+ ->
`Term
(Dolmen_type.Base.term_app1
(module Dolmen_loop.Typer.T)
- env "colibri_abs_real"
+ env s
(fun a -> Expr.Term.apply_cst abs_real [] [ a ]))
| _ -> `Not_found)
end
@@ -157,7 +159,7 @@ module Check = struct
| { app = { builtin = Expr.Geq }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
!<<(Q.geq !>a !>b)
- | { app = { builtin = Expr.Floor }; tyargs = []; args; _ } ->
+ | { app = { builtin = Expr.Floor_to_int }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
!<(Q.floor !>a)
| { app = { builtin = Expr.Abs | Builtin.Abs_real }; tyargs = []; args; _ }
@@ -331,7 +333,7 @@ let converter d (f : Ground.t) =
let a, b = IArray.extract2_exn args in
cmp Q.ge a b;
Check.attach d f
- | { app = { builtin = Expr.Floor }; tyargs = []; args; _ } ->
+ | { app = { builtin = Expr.Floor_to_int }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
reg a;
Check.attach d f
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index c1dff258d955d2a8da91b6a67bd3e14e8d2ad809..31b233b9d18eefad60f2a3daf3838a44ea93bd98 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -198,7 +198,7 @@ let skolemize d (e : Ground.ClosedQuantifier.s) =
let subst_term =
List.fold_left
(fun acc v ->
- let id = Expr.Term.Const.mk v.Expr.name v.id_ty in
+ let id = Expr.Term.Const.mk v.Expr.path v.id_ty in
let t = Expr.Term.apply_cst id [] [] in
Expr.Term.Var.M.add v (Ground.convert ~subst:e.subst t) acc)
e.subst.term e.term_vars