Add handling of function definition

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)

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

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

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

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

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

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}))))

src_colibri2/tests/solve/smt_uf/unsat/fundef.smt2

+(set-logic ALL)
+
+(define-fun foo ((x Int)) Bool (= x 1))
+
+(assert (foo 0))
+
+(check-sat)