diff --git a/src_colibri2/core/datastructure.ml b/src_colibri2/core/datastructure.ml
index e28c7200245e7a5f647b837d5daa074646e99d14..f5f416cc99adf9364f780ecaeb078a7645eacf6d 100644
--- a/src_colibri2/core/datastructure.ml
+++ b/src_colibri2/core/datastructure.ml
@@ -87,3 +87,4 @@ module Hashtbl(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key :
end
module HNode = Hashtbl(Nodes.Node)
+module HTermConst = Hashtbl(Expr.Term.Const)
diff --git a/src_colibri2/core/datastructure.mli b/src_colibri2/core/datastructure.mli
index 86dd3cf6b61f6735117ab2743daefe7213f5e58f..f9bb3ee6e3219e579bef38c7bfbde32b0f89b45b 100644
--- a/src_colibri2/core/datastructure.mli
+++ b/src_colibri2/core/datastructure.mli
@@ -34,3 +34,4 @@ end
module Hashtbl (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key := S.t
module HNode : Sig with type key := Nodes.Node.t
+module HTermConst : Sig with type key := Expr.Term.Const.t
diff --git a/src_colibri2/core/structures/expr.ml b/src_colibri2/core/structures/expr.ml
index d6b5be6b667047dc406e443cffde02a5627932d1..70062664e9da5f5250bbe9733e4ec44655026fb7 100644
--- a/src_colibri2/core/structures/expr.ml
+++ b/src_colibri2/core/structures/expr.ml
@@ -32,5 +32,13 @@ module Term = struct
include Dolmen_std.Expr.Term.Const
let pp fmt (t:t) = Dolmen_std.Expr.Id.print fmt t
let hash_fold_t state t = Base.Hash.fold_int state (hash 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
+ end)
end
end
diff --git a/src_colibri2/core/synTerm.ml b/src_colibri2/core/synTerm.ml
index 9a053bfc13522777a92b2c19d4560949d9234957..a266f15f9c111c2b8b86acb754a1ccd3dfd0c74b 100644
--- a/src_colibri2/core/synTerm.ml
+++ b/src_colibri2/core/synTerm.ml
@@ -34,6 +34,41 @@ module ThTerm = RegisterThTerm(struct
let node_of_term x = ThTerm.node (ThTerm.index x)
+(** Definitions *)
+module Defs = struct
+
+ type fundef = {
+ tyl: Expr.Ty.Var.t list;
+ tvl: Expr.Term.Var.t list;
+ body: Expr.Term.t
+ }
+
+ let pp_fundef _ _ = ()
+
+ let fundefs = Datastructure.HTermConst.create pp_fundef "SynTerm.fundefs"
+
+ let add d tc tyl tvl body =
+ Datastructure.HTermConst.set fundefs d tc {tyl;tvl;body}
+
+ let converter d (v:Expr.Term.t) cl =
+ match v with
+ | { descr = App(tc,tyl,tvl); _ } ->
+ begin match Datastructure.HTermConst.find fundefs d tc with
+ | exception Not_found -> ()
+ | fundef ->
+ let mk_subst vl l =
+ List.fold_left2
+ (fun subst var v -> Expr.Subst.Var.bind subst var v)
+ Expr.Subst.empty vl l
+ in
+ let subst_ty = mk_subst fundef.tyl tyl in
+ let subst_term = mk_subst fundef.tvl tvl in
+ let body = Expr.Term.subst subst_ty subst_term fundef.body in
+ Egraph.set_thterm d cl (ThTerm.thterm (ThTerm.index body))
+ end
+ | _ -> ()
+end
+
type env = {
converters: (Egraph.t -> Expr.Term.t -> Node.t -> unit) list;
}
@@ -74,7 +109,8 @@ module DaemonConvertTerm = struct
| _ ->
let cl = ThTerm.node thterm in
let iter conv = conv d v cl in
- List.iter iter e.converters
+ List.iter iter e.converters;
+ Defs.converter d v cl
in
handle v
end with Exit -> () end
@@ -84,10 +120,13 @@ end
module RDaemonConvertTerm = Demon.Fast.Register(DaemonConvertTerm)
+(* Not added in default theories because Solver.input requires it. So scheduler
+ always add it *)
let init env =
Egraph.set_env env converters {converters=[]};
RDaemonConvertTerm.init env;
Demon.Fast.attach env
- DaemonConvertTerm.key [Demon.Create.EventRegSem(ThTerm.key,())];
+ DaemonConvertTerm.key [Demon.Create.EventRegSem(ThTerm.key,())]
+
include ThTerm
diff --git a/src_colibri2/core/synTerm.mli b/src_colibri2/core/synTerm.mli
index 7645b601a631094720f3e2f95a932f1cd7ac40bd..837449fd3f21d12541285abfac41781fd2b1cb96 100644
--- a/src_colibri2/core/synTerm.mli
+++ b/src_colibri2/core/synTerm.mli
@@ -36,3 +36,14 @@ val register_converter:
(Egraph.t -> Expr.Term.t -> Node.t -> unit) ->
unit
(** register converters between syntactic terms *)
+
+module Defs: sig
+
+ val add:
+ Egraph.t ->
+ Expr.Term.Const.t ->
+ Expr.Ty.Var.t list ->
+ Expr.Term.Var.t list ->
+ Expr.Term.t ->
+ unit
+end
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index 4d5d445056a7fa7f45cbfd91e17eaa103c9f16fc..9d3a19a83220d02ba4caeab05759772aa0bfcf9c 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -172,7 +172,13 @@ let debug_pipe st c =
Dolmen.Std.Statement.print c;
st, c
-let def _st _d = invalid_arg "unimplemented"
+let def st (d:Typer.def) =
+ match d with
+ | `Type_def _ -> () (* handled by dolmen *)
+ | `Term_def (_, tc, tyl, tvl, b) ->
+ Scheduler.add_assertion st.scheduler (fun d ->
+ SynTerm.Defs.add d tc tyl tvl b
+ )
let set_term_true ~set_true d t =
let t = SynTerm.node_of_term t in
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
index 5e8a4d4979f43fd9dfb437d3e29e112d73b3b150..36caad8d4996674d751b573dd3356a18f400638e 100644
--- a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
@@ -13,6 +13,8 @@
(rule (alias runtest) (action (diff oracle eq_diamond2.smt2.res)))
(rule (action (with-stdout-to equality_norm_set.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:equality_norm_set.smt2}))))
(rule (alias runtest) (action (diff oracle equality_norm_set.smt2.res)))
+(rule (action (with-stdout-to fundef.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:fundef.smt2}))))
+(rule (alias runtest) (action (diff oracle fundef.smt2.res)))
(rule (action (with-stdout-to get_repr_at__instead_of__equal_CRepr.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:get_repr_at__instead_of__equal_CRepr.smt2}))))
(rule (alias runtest) (action (diff oracle get_repr_at__instead_of__equal_CRepr.smt2.res)))
(rule (action (with-stdout-to many_distinct.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:many_distinct.smt2}))))
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/fundef.smt2 b/src_colibri2/tests/solve/smt_uf/unsat/fundef.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..99ba9585229d92cf32a438d296d60c3bc51ab324
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_uf/unsat/fundef.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+
+(define-fun foo ((x Int)) Bool (= x 1))
+
+(assert (foo 0))
+
+(check-sat)