From 4c6d44f974d16210436c51b07c3f57ab8f0e649d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Jan 2023 18:58:18 -0800
Subject: [PATCH] add ocaml signature for simplifier

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/ml/z3.ml  | 29 +++++++++++++++++++++++++++++
 src/api/ml/z3.mli | 37 +++++++++++++++++++++++++++++++++++++
 2 files changed, 66 insertions(+)

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 2fa4acc65..ffb815233 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -1734,6 +1734,34 @@ struct
   let interrupt = Z3native.interrupt
 end
 
+module Simplifier =
+struct
+  type simplifier = Z3native.simplifier
+  let gc = Z3native.context_of_simplifier
+  let mk_simplifier = Z3native.mk_simplifier
+
+  let get_num_simplifiers = Z3native.get_num_simplifiers
+
+  let get_simplifier_names (ctx:context) =
+    let n = get_num_simplifiers ctx in
+    let f i = Z3native.get_simplifier_name ctx i in
+    mk_list f n
+
+  let get_help (x:simplifier) = Z3native.simplifier_get_help (gc x) x
+  let get_param_descrs (x:simplifier) = Z3native.simplifier_get_param_descrs (gc x) x
+
+  let and_then (ctx:context) (t1:simplifier) (t2:simplifier) (ts:simplifier list) =
+    let f p c = (match p with
+        | None -> Some c
+        | Some(x) -> Some (Z3native.simplifier_and_then ctx c x)) in
+    match (List.fold_left f None ts) with
+    | None -> Z3native.simplifier_and_then ctx t1 t2
+    | Some(x) -> let o = Z3native.simplifier_and_then ctx t2 x in
+      Z3native.simplifier_and_then ctx t1 o
+  let using_params = Z3native.simplifier_using_params
+  let with_ = using_params
+
+end
 
 module Statistics =
 struct
@@ -1868,6 +1896,7 @@ struct
   let mk_solver_s ctx logic = mk_solver ctx (Some (Symbol.mk_string ctx logic))
   let mk_simple_solver = Z3native.mk_simple_solver
   let mk_solver_t = Z3native.mk_solver_from_tactic
+  let add_simplifier = Z3native.solver_add_simplifier
   let translate x = Z3native.solver_translate (gc x) x
   let to_string x = Z3native.solver_to_string (gc x) x
 end
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index b7fa27b5e..6c0f0f60b 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -3102,6 +3102,40 @@ sig
   val interrupt : context -> unit
 end
 
+moduls Simplifier :
+sig
+  type simplifier
+
+  (** A string containing a description of parameters accepted by the simplifier. *)
+  val get_help : simplifier -> string
+
+  (** Retrieves parameter descriptions for Simplifiers. *)
+  val get_param_descrs : simplifier -> Params.ParamDescrs.param_descrs
+
+  (** Apply the simplifier to the goal. *)
+  val apply : simplifier -> Goal.goal -> Params.params option -> ApplyResult.apply_result
+
+  (** The number of supported simplifiers. *)
+  val get_num_simplifiers : context -> int
+
+  (** The names of all supported simplifiers. *)
+  val get_simplifier_names : context -> string list
+
+  (** Returns a string containing a description of the simplifier with the given name. *)
+  val get_simplifier_description : context -> string -> string
+
+  (** Creates a new Simplifier. *)
+  val mk_simplifier : context -> string -> simplifier
+
+  (** Create a simplifier that applies one simplifier to a Goal and
+      then another one to every subgoal produced by the first one. *)
+  val and_then : context -> simplifier -> simplifier -> simplifier list -> simplifier
+
+  (** Create a simplifier that applies a simplifier using the given set of parameters. *)
+  val using_params : context -> simplifier -> Params.params -> simplifier
+
+end
+
 (** Objects that track statistical information. *)
 module Statistics :
 sig
@@ -3265,6 +3299,9 @@ sig
       will always solve each check from scratch. *)
   val mk_solver_t : context -> Tactic.tactic -> solver
 
+  (** Create a solver with simplifying pre-processing **)
+  val add_simplifier : context -> solver -> Simplifier.simplifier -> solver
+
   (** Create a clone of the current solver with respect to a context. *)
   val translate : solver -> context -> solver