diff --git a/src_colibri2/core/dune b/src_colibri2/core/dune
index 2709e1eb32e3118144f1a3b502c865a9be1b09fa..b258dddedc50d2f414b7bc6226c13296f5ea3605 100644
--- a/src_colibri2/core/dune
+++ b/src_colibri2/core/dune
@@ -2,7 +2,7 @@
(name colibri2_core)
(public_name colibri2.core)
(synopsis "core for colibri2, e.g. trail, egraph")
- (libraries containers ocamlgraph str colibri2.stdlib colibri2.popop_lib dolmen.std)
+ (libraries containers ocamlgraph str colibri2.stdlib colibri2.popop_lib dolmen.std dolmen_loop)
(preprocess
(pps ppx_deriving.std ppx_hash))
(flags :standard -w +a-4-42-44-48-50-58-60-40-9@8 -color always -open
diff --git a/src_colibri2/core/structures/expr.ml b/src_colibri2/core/structures/expr.ml
index b5c34015fcfd3e4398682819d3321f4ff41b4a41..f4674eb6cd6412727eb8f3677b72f6dc3d8d1c09 100644
--- a/src_colibri2/core/structures/expr.ml
+++ b/src_colibri2/core/structures/expr.ml
@@ -26,28 +26,38 @@ module Ty = struct
let pp = print
- include Colibri2_popop_lib.Popop_stdlib.MkDatatype(struct
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype (struct
+ type nonrec t = t
+
+ let equal = equal
+
+ let compare = compare
+
+ let hash = hash
+
+ let pp = pp
+
+ let hash_fold_t s t = Base.Hash.fold_int s (hash t)
+ end)
+
+ module Var = struct
+ include Dolmen_std.Expr.Ty.Var
+
+ let pp = Dolmen_std.Expr.Print.ty_var
+
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype (struct
type nonrec t = t
+
let equal = equal
+
let compare = compare
+
let hash = hash
+
let pp = pp
+
let hash_fold_t s t = Base.Hash.fold_int s (hash t)
end)
-
- module Var = struct
- include Dolmen_std.Expr.Ty.Var
-
- let pp = Dolmen_std.Expr.Print.ty_var
-
- include Colibri2_popop_lib.Popop_stdlib.MkDatatype(struct
- type nonrec t = t
- let equal = equal
- let compare = compare
- let hash = hash
- let pp = pp
- let hash_fold_t s t = Base.Hash.fold_int s (hash t)
- end)
end
let rec free_vars acc (t : t) =
@@ -56,117 +66,160 @@ module Ty = struct
| TyApp (_, l) -> List.fold_left free_vars acc l
| Arrow (args, ret) -> List.fold_left free_vars (free_vars acc ret) args
| Pi (vars, body) ->
- let fv = free_vars Var.S.empty body in
- let fv = List.fold_left (fun acc v -> Var.S.remove v acc) fv vars in
- Var.S.union fv acc
+ let fv = free_vars Var.S.empty body in
+ let fv = List.fold_left (fun acc v -> Var.S.remove v acc) fv vars in
+ Var.S.union fv acc
module Const = struct
include Dolmen_std.Expr.Ty.Const
- let pp fmt (t:t) = Dolmen_std.Expr.Id.print fmt t
-
- include Colibri2_popop_lib.Popop_stdlib.MkDatatype(struct
- type nonrec t = t
- let equal = equal
- let compare = compare
- let hash = hash
- let pp = pp
- let hash_fold_t s t = Base.Hash.fold_int s (hash t)
- end)
- end
-end
+ let pp fmt (t : t) = Dolmen_std.Expr.Id.print fmt t
-module Term = struct
- include Dolmen_std.Expr.Term
- let pp = print
-
- include Colibri2_popop_lib.Popop_stdlib.MkDatatype(struct
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype (struct
type nonrec t = t
+
let equal = equal
+
let compare = compare
+
let hash = hash
+
let pp = pp
+
let hash_fold_t s t = Base.Hash.fold_int s (hash t)
end)
+ end
+end
- module Const = struct
+module Term = struct
+ include Dolmen_std.Expr.Term
+
+ let pp = print
+
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype (struct
+ type nonrec t = t
+
+ let equal = equal
+ let compare = compare
+
+ let hash = hash
+
+ let pp = pp
+
+ let hash_fold_t s t = Base.Hash.fold_int s (hash t)
+ end)
+
+ module Const = struct
module D = struct
- include Dolmen_std.Expr.Term.Const
- let pp fmt (t:t) = Dolmen_std.Expr.Id.print fmt t
- include Colibri2_popop_lib.Popop_stdlib.MkDatatype(struct
+ include Dolmen_std.Expr.Term.Const
+
+ let pp fmt (t : t) = Dolmen_std.Expr.Id.print fmt t
+
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype (struct
type nonrec t = t
+
let equal = equal
+
let compare = compare
+
let hash = hash
+
let pp = pp
+
let hash_fold_t s t = Base.Hash.fold_int s (hash t)
end)
end
include D
-
- module HC = Datastructure.Hashtbl(D)
-
+ module HC = Datastructure.Hashtbl (D)
end
module Var = struct
include Dolmen_std.Expr.Term.Var
- let pp fmt (t:t) = Dolmen_std.Expr.Id.print fmt t
- include Colibri2_popop_lib.Popop_stdlib.MkDatatype(struct
- type nonrec t = t
- let equal = equal
- let compare = compare
- let hash = hash
- let pp = pp
- let hash_fold_t s t = Base.Hash.fold_int s (hash t)
+ let pp fmt (t : t) = Dolmen_std.Expr.Id.print fmt t
+
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype (struct
+ type nonrec t = t
+
+ let equal = equal
+
+ let compare = compare
+
+ let hash = hash
+
+ let pp = pp
+
+ let hash_fold_t s t = Base.Hash.fold_int s (hash t)
end)
end
- let rec free_vars ((acc_ty,acc_term) as acc) (t : t) = match t.term_descr with
- | Var v -> (Ty.free_vars acc_ty v.id_ty,Var.S.add v acc_term)
+ let rec free_vars ((acc_ty, acc_term) as acc) (t : t) =
+ match t.term_descr with
+ | Var v -> (Ty.free_vars acc_ty v.id_ty, Var.S.add v acc_term)
| Cst _ -> acc
| App (f, tys, ts) ->
- let acc_ty, acc_term = free_vars acc f in
- List.fold_left free_vars (
- List.fold_left Ty.free_vars acc_ty tys, acc_term
- ) ts
+ let acc_ty, acc_term = free_vars acc f in
+ List.fold_left free_vars
+ (List.fold_left Ty.free_vars acc_ty tys, acc_term)
+ ts
| Binder ((Lambda (tys, ts) | Exists (tys, ts) | Forall (tys, ts)), body) ->
- let (fty,fv) = free_vars (Ty.Var.S.empty,Var.S.empty) body in
- let fty = List.fold_left (fun acc ty -> Ty.Var.S.remove ty acc) fty tys in
- let fv = List.fold_left (fun acc t -> Var.S.remove t acc) fv ts in
- (Ty.Var.S.union acc_ty fty, Var.S.union acc_term fv)
+ let fty, fv = free_vars (Ty.Var.S.empty, Var.S.empty) body in
+ let fty =
+ List.fold_left (fun acc ty -> Ty.Var.S.remove ty acc) fty tys
+ in
+ let fv = List.fold_left (fun acc t -> Var.S.remove t acc) fv ts in
+ (Ty.Var.S.union acc_ty fty, Var.S.union acc_term fv)
| Binder (Let_seq l, body) ->
- let (acc_ty,fv) = free_vars (acc_ty,Var.S.empty) body in
- let (acc_ty,fv) = List.fold_right (fun (v, t) (acc_ty,fv) ->
- let fv = Var.S.remove v fv in
- let (acc_ty,fv) = free_vars (acc_ty,fv) t in
- let acc_ty = Ty.free_vars acc_ty v.id_ty in
- (acc_ty,fv)
- ) l (acc_ty,fv) in
- (acc_ty, Var.S.union acc_term fv)
+ let acc_ty, fv = free_vars (acc_ty, Var.S.empty) body in
+ let acc_ty, fv =
+ List.fold_right
+ (fun (v, t) (acc_ty, fv) ->
+ let fv = Var.S.remove v fv in
+ let acc_ty, fv = free_vars (acc_ty, fv) t in
+ let acc_ty = Ty.free_vars acc_ty v.id_ty in
+ (acc_ty, fv))
+ l (acc_ty, fv)
+ in
+ (acc_ty, Var.S.union acc_term fv)
| Binder (Let_par l, body) ->
- let (acc_ty,fv) = free_vars (acc_ty,Var.S.empty) body in
- let fv = List.fold_right (fun (v, _) fv ->
- let fv = Var.S.remove v fv in
- fv
- ) l fv in
- let (acc_ty,fv) = List.fold_right (fun (v, t) (acc_ty,fv) ->
- let (acc_ty,fv) = free_vars (acc_ty,fv) t in
- let acc_ty = Ty.free_vars acc_ty v.id_ty in
- (acc_ty,fv)
- ) l (acc_ty,fv) in
- (acc_ty, Var.S.union acc_term fv)
+ let acc_ty, fv = free_vars (acc_ty, Var.S.empty) body in
+ let fv =
+ List.fold_right
+ (fun (v, _) fv ->
+ let fv = Var.S.remove v fv in
+ fv)
+ l fv
+ in
+ let acc_ty, fv =
+ List.fold_right
+ (fun (v, t) (acc_ty, fv) ->
+ let acc_ty, fv = free_vars (acc_ty, fv) t in
+ let acc_ty = Ty.free_vars acc_ty v.id_ty in
+ (acc_ty, fv))
+ l (acc_ty, fv)
+ in
+ (acc_ty, Var.S.union acc_term fv)
| Match (scrutinee, branches) ->
- let acc = free_vars (acc_ty,acc_term) scrutinee in
- List.fold_left (fun (acc_ty,acc_term) (pat, body) ->
- let (acc_ty,freet) = free_vars (acc_ty,Var.S.empty) body in
- let (acc_ty,boundt) = free_vars (acc_ty,Var.S.empty) pat in
- let bound = Var.S.diff freet boundt in
- (acc_ty, Var.S.union acc_term bound)
- ) acc branches
-
+ let acc = free_vars (acc_ty, acc_term) scrutinee in
+ List.fold_left
+ (fun (acc_ty, acc_term) (pat, body) ->
+ let acc_ty, freet = free_vars (acc_ty, Var.S.empty) body in
+ let acc_ty, boundt = free_vars (acc_ty, Var.S.empty) pat in
+ let bound = Var.S.diff freet boundt in
+ (acc_ty, Var.S.union acc_term bound))
+ acc branches
end
-let foo = 1
+let add_builtins, additional_builtins =
+ let q : Dolmen_loop.Typer.T.builtin_symbols Base.Queue.t =
+ Base.Queue.create ()
+ in
+ ( Base.Queue.enqueue q,
+ fun e t ->
+ let o =
+ Base.Queue.find_map q ~f:(fun f ->
+ match f e t with `Not_found -> None | x -> Some x)
+ in
+ Option.value ~default:`Not_found o )
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index 07ed927216150b2a36ac409fb7e13fbed9ef6827..a5cab114417c344e821fdfb4256b0eaf420e9892 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -63,6 +63,8 @@ module Typer = struct
Dolmen_loop.Typer.Pipe (Dolmen.Std.Expr) (Dolmen.Std.Expr.Print) (State) (T)
end
+let () = Typer.additional_builtins := Colibri2_core.Expr.additional_builtins
+
let split_input = function
| `Stdin -> (Sys.getcwd (), `Stdin)
| `File f -> (Filename.dirname f, `File (Filename.basename f))
diff --git a/src_colibri2/tests/solve/models/abs_real.smt2 b/src_colibri2/tests/solve/models/abs_real.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..509d830f5ba39243715e097c66dd9bba0efe3cf2
--- /dev/null
+++ b/src_colibri2/tests/solve/models/abs_real.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+(set-info :status-colibri2 sat)
+
+(declare-fun a () Int)
+(declare-fun b () Real)
+
+(assert (< a 0))
+(assert (< b 0))
+
+(check-sat)
+(get-model)
+(get-value ((abs a)))
+(get-value ((colibri_abs_real b)))
diff --git a/src_colibri2/tests/solve/models/abs_real.smt2.oracle b/src_colibri2/tests/solve/models/abs_real.smt2.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7b5c3b712725c9a9c61f70e38539c108d694ce1f
--- /dev/null
+++ b/src_colibri2/tests/solve/models/abs_real.smt2.oracle
@@ -0,0 +1,4 @@
+sat
+((a -1)(b -1))
+((abs a 1))
+((colibri_abs_real b 1))
diff --git a/src_colibri2/tests/solve/models/dune.inc b/src_colibri2/tests/solve/models/dune.inc
index 0ffbe69bc24028ef9b0cf0b7c4e79d4a40ddf5d4..c9eaba0f3712b7401bd9cbf990aa709bdf7bc93d 100644
--- a/src_colibri2/tests/solve/models/dune.inc
+++ b/src_colibri2/tests/solve/models/dune.inc
@@ -1,2 +1,4 @@
+(rule (action (with-stdout-to abs_real.smt2.res (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 %{dep:abs_real.smt2}))))
+(rule (alias runtest) (action (diff abs_real.smt2.oracle abs_real.smt2.res)))
(rule (action (with-stdout-to get_value.smt2.res (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 %{dep:get_value.smt2}))))
(rule (alias runtest) (action (diff get_value.smt2.oracle get_value.smt2.res)))
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 1656d81f4ea5a9c13e81390053db86fb32490167..ff7d8c648b2490e41edecd3177642249a2e764e1 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -22,6 +22,25 @@ open Colibri2_core
open Colibri2_popop_lib
open Colibri2_stdlib.Std
+module Builtin = struct
+ type _ Expr.t += Abs_real
+
+ let abs_real =
+ Expr.Id.mk ~name:"colibri_abs_real" ~builtin:Abs_real "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" } ->
+ `Term
+ (Dolmen_type.Base.term_app1
+ (module Dolmen_loop.Typer.T)
+ env "colibri_abs_real"
+ (fun a -> Expr.Term.apply_cst abs_real [] [ a ]))
+ | _ -> `Not_found)
+end
+
module RealValue = Value.Register (struct
include Q
@@ -141,6 +160,10 @@ module Check = struct
| { app = { builtin = Expr.Floor }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
!<(Q.floor !>a)
+ | { app = { builtin = Expr.Abs | Builtin.Abs_real }; tyargs = []; args; _ }
+ ->
+ let a = IArray.extract1_exn args in
+ !<(Q.abs !>a)
| _ -> `None
let init d =
@@ -312,6 +335,10 @@ let converter d (f : Ground.t) =
let a = IArray.extract1_exn args in
reg a;
Check.attach d f
+ | { app = { builtin = Expr.Abs | Builtin.Abs_real }; tyargs = []; args; _ } ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ Check.attach d f
| _ -> ()
let init env =
diff --git a/src_colibri2/theories/LRA/realValue.mli b/src_colibri2/theories/LRA/realValue.mli
index 0584e07e7fdd511918420706958925140b16bf92..c2862ae8aecb795c3673802d740f334f4c547623 100644
--- a/src_colibri2/theories/LRA/realValue.mli
+++ b/src_colibri2/theories/LRA/realValue.mli
@@ -18,6 +18,12 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
+module Builtin : sig
+ type _ Expr.t += Abs_real
+
+ val abs_real : Colibri2_core.Expr.Term.Const.t
+end
+
include Value.S with type s = Q.t
val cst' : Q.t -> t