Use Expr.definition as input of pred_def

Author: Halbaroth

src/lib/frontend/frontend.ml

@@ -352,8 +352,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
 
   let internal_pred_def ?(loc = DStd.Loc.dummy) (E.{ name; axiom; _ } as def) env =
     if not (unused_context name env.used_context) then
-      let expl = mk_root_dep name def.E.axiom loc in
-      SAT.pred_def env.sat_env axiom name expl loc;
+      let expl = mk_root_dep name axiom loc in
+      SAT.pred_def env.sat_env def expl;
       env.expl <- expl
 
   let internal_query ?(loc = DStd.Loc.dummy) (n, f, sort) env =

src/lib/reasoners/fun_sat.ml

@@ -1766,13 +1766,11 @@ module Make (Th : Theory.S) = struct
          'unknown' right away. *)
       {env with unknown_reason = Some (Step_limit n)}
 
-  let pred_def env f name dep _loc =
-    Debug.pred_def f;
-    let gf = mk_gf f name true false in
+  let pred_def env def dep =
+    Debug.pred_def def.E.axiom;
     let guard = env.guards.current_guard in
-    { env with
-      inst =
-        Inst.add_predicate env.inst ~guard ~name gf dep }
+    let inst = Inst.add_predicate env.inst ~guard def dep in
+    { env with inst }
 
   let unsat env fg =
     Timers.with_timer Timers.M_Sat Timers.F_unsat @@ fun () ->

src/lib/reasoners/fun_sat.mli

@@ -50,8 +50,7 @@ module Make (_ : Theory.S) : sig
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
 
-  val pred_def :
-    t -> Expr.t -> string -> Explanation.t -> Dolmen.Std.Loc.loc -> t
+  val pred_def : t -> Expr.def -> Explanation.t -> t
 
   val unsat : t -> Expr.gformula -> Explanation.t
 

src/lib/reasoners/fun_sat_frontend.ml

@@ -48,8 +48,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   let assume_th_elt t th expl =
     exn_handler (fun env -> t := FS.assume_th_elt env th expl) t
 
-  let pred_def t expr n expl loc =
-    exn_handler (fun env -> t := FS.pred_def env expr n expl loc) t
+  let pred_def t def expl =
+    exn_handler (fun env -> t := FS.pred_def env def expl) t
 
   let unsat t g =
     exn_handler (fun env -> FS.unsat env g) t

src/lib/reasoners/instances.ml

@@ -43,8 +43,7 @@ module type S = sig
   val add_predicate :
     t ->
     guard:Expr.t ->
-    name:string ->
-    Expr.gformula ->
+    Expr.def ->
     Ex.t ->
     t
 
@@ -162,11 +161,9 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct
                guards = ME.add guard guarded env.guards
     }
 
-
-  let add_predicate env ~guard ~name gf ex =
-    let { Expr.ff = f; age = age; _ } = gf in
-    let env = { env with
-                matching = EM.max_term_depth env.matching (E.depth f) } in
+  let add_predicate env ~guard E.{ name; axiom = f; _ } ex =
+    let matching = EM.max_term_depth env.matching (E.depth f) in
+    let env = { env with matching } in
     match E.form_view f with
     | E.Iff(f1, f2) ->
       let p = E.mk_term (Symbols.name name) [] Ty.Tbool in
@@ -191,7 +188,7 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct
     | E.Lemma _ ->
       let guarded = try ME.find guard env.guards with Not_found -> [] in
       { env with
-        predicates = ME.add f (guard, age, ex) env.predicates;
+        predicates = ME.add f (guard, 0, ex) env.predicates;
         guards = ME.add guard ((f, false) :: guarded) env.guards
       }
     | E.Unit _ | E.Clause _ | E.Xor _
@@ -409,9 +406,9 @@ module Make(X : Theory.S) : S with type tbox = X.t = struct
     Timers.with_timer Timers.M_Match Timers.F_add_lemma @@ fun () ->
     add_lemma env gf dep
 
-  let add_predicate env ~guard ~name gf =
+  let add_predicate env ~guard def dep =
     Timers.with_timer Timers.M_Match Timers.F_add_predicate @@ fun () ->
-    add_predicate env ~guard ~name gf
+    add_predicate env ~guard def dep
 
   let m_lemmas mconf env tbox selector ilvl =
     Timers.with_timer Timers.M_Match Timers.F_m_lemmas @@ fun () ->

src/lib/reasoners/instances.mli

@@ -36,8 +36,7 @@ module type S = sig
   val add_predicate :
     t ->
     guard:Expr.t ->
-    name:string ->
-    Expr.gformula ->
+    Expr.def ->
     Explanation.t ->
     t
 

src/lib/reasoners/sat_solver_sig.ml

@@ -109,13 +109,7 @@ module type S = sig
   (** [assume env f exp] assumes a new formula [f] with the explanation [exp]
       in the theory environment of [env]. *)
 
-  val pred_def :
-    t ->
-    Expr.t ->
-    string ->
-    Explanation.t ->
-    Dolmen.Std.Loc.loc ->
-    unit
+  val pred_def : t -> Expr.def -> Explanation.t -> unit
   (** [pred_def env f] assumes a new predicate definition [f] in [env]. *)
 
   val optimize : t -> Objective.Function.t -> unit

src/lib/reasoners/sat_solver_sig.mli

@@ -89,13 +89,7 @@ module type S = sig
   (** [assume env f exp] assumes a new formula [f] with the explanation [exp]
       in the theory environment of [env]. *)
 
-  val pred_def :
-    t ->
-    Expr.t ->
-    string ->
-    Explanation.t ->
-    Dolmen.Std.Loc.loc ->
-    unit
+  val pred_def : t -> Expr.def -> Explanation.t -> unit
   (** [pred_def env f] assumes a new predicate definition [f] in [env]. *)
 
   val optimize : t -> Objective.Function.t -> unit

src/lib/reasoners/satml_frontend.ml

@@ -456,11 +456,11 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       )acc l
 
 
-  let pred_def env f name dep _loc =
+  let pred_def env def dep =
     (* dep currently not used. No unsat-cores in satML yet *)
-    Debug.pred_def f;
+    Debug.pred_def def.E.axiom;
     let guard = env.guards.current_guard in
-    env.inst <- Inst.add_predicate env.inst ~guard ~name (mk_gf f) dep
+    env.inst <- Inst.add_predicate env.inst ~guard def dep
 
   let axiom_def env gf ex =
     env.inst <- Inst.add_lemma env.inst gf ex