From 94e2197df5e909c34f1a66bc0d95c163ad81c661 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 16 Nov 2020 15:24:09 +0100
Subject: [PATCH] Add handling of function definition
---
src_colibri2/core/datastructure.ml | 1 +
src_colibri2/core/datastructure.mli | 1 +
src_colibri2/core/structures/expr.ml | 8 ++++
src_colibri2/core/synTerm.ml | 43 ++++++++++++++++++-
src_colibri2/core/synTerm.mli | 11 +++++
src_colibri2/solver/input.ml | 8 +++-
.../tests/solve/smt_uf/unsat/dune.inc | 2 +
.../tests/solve/smt_uf/unsat/fundef.smt2 | 7 +++
8 files changed, 78 insertions(+), 3 deletions(-)
create mode 100644 src_colibri2/tests/solve/smt_uf/unsat/fundef.smt2
diff --git a/src_colibri2/core/datastructure.ml b/src_colibri2/core/datastructure.ml
index e28c72002..f5f416cc9 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 86dd3cf6b..f9bb3ee6e 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 d6b5be6b6..70062664e 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 9a053bfc1..a266f15f9 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 7645b601a..837449fd3 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 4d5d44505..9d3a19a83 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 5e8a4d497..36caad8d4 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 000000000..99ba95852
--- /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)
--
GitLab