add API for creating and attaching simplifiers

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

scripts/update_api.py

@@ -312,7 +312,7 @@ NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
 Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
 Unchecked = frozenset([ 'Z3_dec_ref', 'Z3_params_dec_ref', 'Z3_model_dec_ref',
                         'Z3_func_interp_dec_ref', 'Z3_func_entry_dec_ref',
-                        'Z3_goal_dec_ref', 'Z3_tactic_dec_ref', 'Z3_probe_dec_ref',
+                        'Z3_goal_dec_ref', 'Z3_tactic_dec_ref', 'Z3_simplifier_dec_ref', 'Z3_probe_dec_ref',
                         'Z3_fixedpoint_dec_ref', 'Z3_param_descrs_dec_ref',
                         'Z3_ast_vector_dec_ref', 'Z3_ast_map_dec_ref', 
                         'Z3_apply_result_dec_ref', 'Z3_solver_dec_ref',
@@ -1176,6 +1176,8 @@ def ml_plus_type(ts):
         return 'Z3_goal_plus'
     elif ts == 'Z3_tactic':
         return 'Z3_tactic_plus'
+    elif ts == 'Z3_simplifier':
+        return 'Z3_simplifier_plus'
     elif ts == 'Z3_probe':
         return 'Z3_probe_plus'
     elif ts == 'Z3_apply_result':
@@ -1220,6 +1222,8 @@ def ml_minus_type(ts):
         return 'Z3_goal'
     elif ts == 'Z3_tactic_plus':
         return 'Z3_tactic'
+    elif ts == 'Z3_simplifier_plus':
+        return 'Z3_simplifier'
     elif ts == 'Z3_probe_plus':
         return 'Z3_probe'
     elif ts == 'Z3_apply_result_plus':

src/api/api_solver.cpp

@@ -44,6 +44,7 @@ Revision History:
 #include "sat/tactic/goal2sat.h"
 #include "sat/tactic/sat2goal.h"
 #include "cmd_context/extra_cmds/proof_cmds.h"
+#include "solver/simplifier_solver.h"
 
 
 extern "C" {
@@ -232,12 +233,26 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier) {
+        Z3_TRY;
+        LOG_Z3_solver_add_simplifier(c, solver, simplifier); 
+        init_solver(c, solver);
+        auto simp = to_simplifier_ref(simplifier);
+        auto* slv = mk_simplifier_solver(to_solver_ref(solver), simp);
+        Z3_solver_ref* sr = alloc(Z3_solver_ref, *mk_c(c), slv);
+        mk_c(c)->save_object(sr);
+        // ?? init_solver_log(c, sr)
+        RETURN_Z3(of_solver(sr));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+
     Z3_solver Z3_API Z3_solver_translate(Z3_context c, Z3_solver s, Z3_context target) {
         Z3_TRY;
         LOG_Z3_solver_translate(c, s, target);
         RESET_ERROR_CODE();
         params_ref const& p = to_solver(s)->m_params; 
-        Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(target), nullptr);
+        Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(target), (solver_factory *)nullptr);
         init_solver(c, s);
         sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
         mk_c(target)->save_object(sr);

src/api/api_solver.h

@@ -52,6 +52,9 @@ struct Z3_solver_ref : public api::object {
     Z3_solver_ref(api::context& c, solver_factory * f): 
         api::object(c), m_solver_factory(f), m_solver(nullptr), m_logic(symbol::null), m_eh(nullptr) {}
 
+    Z3_solver_ref(api::context& c, solver * s): 
+        api::object(c), m_solver_factory(nullptr), m_solver(s), m_logic(symbol::null), m_eh(nullptr) {}
+
     void assert_expr(expr* e);
     void assert_expr(expr* e, expr* t);
     void set_eh(event_handler* eh);

src/api/api_tactic.cpp

@@ -20,9 +20,11 @@ Revision History:
 #include "api/api_context.h"
 #include "api/api_tactic.h"
 #include "api/api_model.h"
+#include "api/api_solver.h"
 #include "util/scoped_ctrl_c.h"
 #include "util/cancel_eh.h"
 #include "util/scoped_timer.h"
+#include "ast/simplifiers/seq_simplifier.h"
 
 Z3_apply_result_ref::Z3_apply_result_ref(api::context& c, ast_manager & m): api::object(c) {
 }
@@ -45,6 +47,14 @@ extern "C" {
         RETURN_Z3(_result_);                                    \
 }
 
+#define RETURN_SIMPLIFIER(_t_) {                                    \
+        Z3_simplifier_ref * _ref_ = alloc(Z3_simplifier_ref, *mk_c(c)); \
+        _ref_->m_simplifier   = _t_;                                \
+        mk_c(c)->save_object(_ref_);                            \
+        Z3_simplifier _result_  = of_simplifier(_ref_);                 \
+        RETURN_Z3(_result_);                                    \
+}
+
     Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name) {
         Z3_TRY;
         LOG_Z3_mk_tactic(c, name);
@@ -517,6 +527,146 @@ extern "C" {
         RETURN_Z3(result);
         Z3_CATCH_RETURN(nullptr);
     }
+
+
+
+    Z3_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name) {
+        Z3_TRY;
+        LOG_Z3_mk_simplifier(c, name);
+        RESET_ERROR_CODE();
+        simplifier_cmd * t = mk_c(c)->find_simplifier_cmd(symbol(name));
+        if (t == nullptr) {
+            std::stringstream err;
+            err << "unknown simplifier " << name;
+            SET_ERROR_CODE(Z3_INVALID_ARG, err.str());
+            RETURN_Z3(nullptr);
+        }
+        simplifier_factory new_t = t->factory();
+        RETURN_SIMPLIFIER(new_t);
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t) {
+        Z3_TRY;
+        LOG_Z3_simplifier_inc_ref(c, t);
+        RESET_ERROR_CODE();
+        to_simplifier(t)->inc_ref();
+        Z3_CATCH;
+    }
+
+    void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier t) {
+        Z3_TRY;
+        LOG_Z3_simplifier_dec_ref(c, t);
+        if (t)
+            to_simplifier(t)->dec_ref();
+        Z3_CATCH;
+    }
+
+    unsigned Z3_API Z3_get_num_simplifiers(Z3_context c) {
+        Z3_TRY;
+        LOG_Z3_get_num_simplifiers(c);
+        RESET_ERROR_CODE();
+        return mk_c(c)->num_simplifiers();
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_string Z3_API Z3_get_simplifier_name(Z3_context c, unsigned idx) {
+        Z3_TRY;
+        LOG_Z3_get_simplifier_name(c, idx);
+        RESET_ERROR_CODE();
+        if (idx >= mk_c(c)->num_simplifiers()) {
+            SET_ERROR_CODE(Z3_IOB, nullptr);
+            return "";
+        }        
+        return mk_c(c)->mk_external_string(mk_c(c)->get_simplifier(idx)->get_name().str().c_str());
+        Z3_CATCH_RETURN("");
+    }
+
+    Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2) {
+        Z3_TRY;
+        LOG_Z3_simplifier_and_then(c, t1, t2);
+        RESET_ERROR_CODE();
+        auto fac1 = *to_simplifier_ref(t1);
+        auto fac2 = *to_simplifier_ref(t2);
+        auto new_s = [fac1, fac2](auto& m, auto& p, auto& st) {
+            auto* r = alloc(seq_simplifier, m, p, st);
+            r->add_simplifier(fac1(m, p, st));
+            r->add_simplifier(fac2(m, p, st));
+            return r;
+    };
+        RETURN_SIMPLIFIER(new_s);
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p) {
+        Z3_TRY;
+        LOG_Z3_simplifier_using_params(c, t, p);
+        RESET_ERROR_CODE();
+        param_descrs r;
+        ast_manager& m = mk_c(c)->m();
+        default_dependent_expr_state st(m);
+        params_ref p1;
+        auto fac = (*to_simplifier_ref(t));
+        scoped_ptr<dependent_expr_simplifier> simp = fac(m, p1, st);
+        simp->collect_param_descrs(r);
+        auto params = to_param_ref(p);
+        params.validate(r);
+        auto new_s = [params, fac](auto& m, auto& p, auto& st) {
+            params_ref pp;
+            pp.append(params);
+            pp.append(p);
+            return fac(m, pp, st);
+        };
+        RETURN_SIMPLIFIER(new_s);
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+
+    Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t) {
+        Z3_TRY;
+        LOG_Z3_simplifier_get_help(c, t);
+        RESET_ERROR_CODE();
+        std::ostringstream buffer;
+        param_descrs descrs;
+        ast_manager& m = mk_c(c)->m();
+        default_dependent_expr_state st(m);
+        params_ref p;
+        scoped_ptr<dependent_expr_simplifier> simp = (*to_simplifier_ref(t))(m, p, st);
+        simp->collect_param_descrs(descrs);
+        descrs.display(buffer);
+        return mk_c(c)->mk_external_string(buffer.str());
+        Z3_CATCH_RETURN("");
+    }
+
+    Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t) {
+        Z3_TRY;
+        LOG_Z3_simplifier_get_param_descrs(c, t);
+        RESET_ERROR_CODE();
+        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
+        mk_c(c)->save_object(d);
+        ast_manager& m = mk_c(c)->m();
+        default_dependent_expr_state st(m);
+        params_ref p;
+        scoped_ptr<dependent_expr_simplifier> simp = (*to_simplifier_ref(t))(m, p, st);
+        simp->collect_param_descrs(d->m_descrs);
+        Z3_param_descrs r = of_param_descrs(d);
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_string Z3_API Z3_simplifier_get_descr(Z3_context c, Z3_string name) {
+        Z3_TRY;
+        LOG_Z3_simplifier_get_descr(c, name);
+        RESET_ERROR_CODE();
+        simplifier_cmd * t = mk_c(c)->find_simplifier_cmd(symbol(name));
+        if (t == nullptr) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+            return "";
+        }
+        return t->get_descr();
+        Z3_CATCH_RETURN("");
+    }
+
     
 
 };

src/api/api_tactic.h

@@ -19,6 +19,7 @@ Revision History:
 
 #include "api/api_goal.h"
 #include "tactic/tactical.h"
+#include "ast/simplifiers/dependent_expr_state.h"
 
 namespace api {
     class context;
@@ -35,10 +36,19 @@ struct Z3_probe_ref : public api::object {
     Z3_probe_ref(api::context& c):api::object(c) {}
 };
 
+struct Z3_simplifier_ref : public api::object {
+    simplifier_factory m_simplifier;
+    Z3_simplifier_ref(api::context& c):api::object(c) {}
+};
+
 inline Z3_tactic_ref * to_tactic(Z3_tactic g) { return reinterpret_cast<Z3_tactic_ref *>(g); }
 inline Z3_tactic of_tactic(Z3_tactic_ref * g) { return reinterpret_cast<Z3_tactic>(g); }
 inline tactic * to_tactic_ref(Z3_tactic g) { return g == nullptr ? nullptr : to_tactic(g)->m_tactic.get(); }
 
+inline Z3_simplifier_ref * to_simplifier(Z3_simplifier g) { return reinterpret_cast<Z3_simplifier_ref *>(g); }
+inline Z3_simplifier of_simplifier(Z3_simplifier_ref * g) { return reinterpret_cast<Z3_simplifier>(g); }
+inline simplifier_factory * to_simplifier_ref(Z3_simplifier g) { return g == nullptr ? nullptr : &to_simplifier(g)->m_simplifier; }
+
 inline Z3_probe_ref * to_probe(Z3_probe g) { return reinterpret_cast<Z3_probe_ref *>(g); }
 inline Z3_probe of_probe(Z3_probe_ref * g) { return reinterpret_cast<Z3_probe>(g); }
 inline probe * to_probe_ref(Z3_probe g) { return g == nullptr ? nullptr : to_probe(g)->m_probe.get(); }

src/api/c++/z3++.h

@@ -63,6 +63,7 @@ namespace z3 {
     class solver;
     class goal;
     class tactic;
+    class simplifier;
     class probe;
     class model;
     class func_interp;
@@ -2695,6 +2696,7 @@ namespace z3 {
         solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); check_error(); }
         solver(context & c, solver const& src, translate): object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); }
         solver(solver const & s):object(s) { init(s.m_solver); }
+        solver(solver const& s, simplifier const& simp);
         ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
         operator Z3_solver() const { return m_solver; }
         solver & operator=(solver const & s) {
@@ -3065,6 +3067,47 @@ namespace z3 {
         return tactic(t1.ctx(), r);
     }
 
+    class simplifier : public object {
+        Z3_simplifier m_simplifier;
+        void init(Z3_simplifier s) {
+            m_simplifier = s;
+            Z3_simplifier_inc_ref(ctx(), s);
+        }
+    public:
+        simplifier(context & c, char const * name):object(c) { Z3_simplifier r = Z3_mk_simplifier(c, name); check_error(); init(r); }
+        simplifier(context & c, Z3_simplifier s):object(c) { init(s); }
+        simplifier(simplifier const & s):object(s) { init(s.m_simplifier); }
+        ~simplifier() { Z3_simplifier_dec_ref(ctx(), m_simplifier); }
+        operator Z3_simplifier() const { return m_simplifier; }
+        simplifier & operator=(simplifier const & s) {
+            Z3_simplifier_inc_ref(s.ctx(), s.m_simplifier);
+            Z3_simplifier_dec_ref(ctx(), m_simplifier);
+            object::operator=(s);
+            m_simplifier = s.m_simplifier;
+            return *this;
+        }
+        std::string help() const { char const * r = Z3_simplifier_get_help(ctx(), m_simplifier); check_error();  return r; }
+        friend simplifier operator&(simplifier const & t1, simplifier const & t2);
+        friend simplifier with(simplifier const & t, params const & p);
+        param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_simplifier_get_param_descrs(ctx(), m_simplifier)); }
+    };
+
+    inline solver::solver(solver const& s, simplifier const& simp):object(s) { init(Z3_solver_add_simplifier(s.ctx(), s, simp)); }
+
+
+    inline simplifier operator&(simplifier const & t1, simplifier const & t2) {
+        check_context(t1, t2);
+        Z3_simplifier r = Z3_simplifier_and_then(t1.ctx(), t1, t2);
+        t1.check_error();
+        return simplifier(t1.ctx(), r);
+    }
+
+    inline simplifier with(simplifier const & t, params const & p) {
+        Z3_simplifier r = Z3_simplifier_using_params(t.ctx(), t, p);
+        t.check_error();
+        return simplifier(t.ctx(), r);
+    }
+
     class probe : public object {
         Z3_probe m_probe;
         void init(Z3_probe s) {

src/api/python/z3/z3.py

@@ -8169,6 +8169,64 @@ class ApplyResult(Z3PPObject):
         else:
             return Or([self[i].as_expr() for i in range(len(self))])
 
+#########################################
+#
+# Simplifiers
+#
+#########################################
+
+class Simplifier:
+    """Simplifiers act as pre-processing utilities for solvers.
+    Build a custom simplifier and add it to a solver"""
+
+    def __init__(self, simplifier, ctx=None):
+        self.ctx = _get_ctx(ctx)
+        self.simplifier = None
+        if isinstance(simplifier, SimplifierObj):
+            self.simplifier = simplifier
+        elif isinstance(simplifier, list):
+            simps = [Simplifier(s, ctx) for s in simplifier]
+            self.simplifier = simps[0].simplifier
+            for i in range(1, len(simps)):
+                self.simplifier = Z3_simplifier_and_then(self.ctx.ref(), self.simplifier, simps[i].simplifier)
+            Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
+            return
+        else:
+            if z3_debug():
+                _z3_assert(isinstance(simplifier, str), "simplifier name expected")
+            try:
+                self.simplifier = Z3_mk_simplifier(self.ctx.ref(), str(simplifier))
+            except Z3Exception:
+                raise Z3Exception("unknown simplifier '%s'" % simplifier)
+        Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
+
+    def __deepcopy__(self, memo={}):
+        return Simplifier(self.simplifier, self.ctx)
+
+    def __del__(self):
+        if self.simplifier is not None and self.ctx.ref() is not None and Z3_simplifier_dec_ref is not None:
+            Z3_simplifier_dec_ref(self.ctx.ref(), self.simplifier)
+
+    def using_params(self, *args, **keys):
+        """Return a simplifier that uses the given configuration options"""
+        p = args2params(args, keys, self.ctx)
+        return Simplifier(Z3_simplifier_using_params(self.ctx.ref(), self.simplifier, p.params), self.ctx)
+
+    def add(self, solver):
+        """Return a solver that applies the simplification pre-processing specified by the simplifier"""
+        print(solver.solver)
+        print(self.simplifier)
+        return Solver(Z3_solver_add_simplifier(self.ctx.ref(), solver.solver, self.simplifier), self.ctx)
+
+    def help(self):
+        """Display a string containing a description of the available options for the `self` simplifier."""
+        print(Z3_simplifier_get_help(self.ctx.ref(), self.simplifier))
+
+    def param_descrs(self):
+        """Return the parameter description set."""
+        return ParamDescrsRef(Z3_simplifier_get_param_descrs(self.ctx.ref(), self.simplifier), self.ctx)
+        
+    
 #########################################
 #
 # Tactics

src/api/python/z3/z3types.py

@@ -120,6 +120,12 @@ class TacticObj(ctypes.c_void_p):
     def from_param(obj):
         return obj
 
+class SimplifierObj(ctypes.c_void_p):
+    def __init__(self, simplifier):
+        self._as_parameter_ = simplifier
+
+    def from_param(obj):
+        return obj
 
 class ProbeObj(ctypes.c_void_p):
     def __init__(self, probe):

src/api/z3_api.h

@@ -23,6 +23,7 @@ DEFINE_TYPE(Z3_param_descrs);
 DEFINE_TYPE(Z3_parser_context);
 DEFINE_TYPE(Z3_goal);
 DEFINE_TYPE(Z3_tactic);
+DEFINE_TYPE(Z3_simplifier);
 DEFINE_TYPE(Z3_probe);
 DEFINE_TYPE(Z3_stats);
 DEFINE_TYPE(Z3_solver);
@@ -69,6 +70,7 @@ DEFINE_TYPE(Z3_rcf_num);
    - \c Z3_ast_map: mapping from \c Z3_ast to \c Z3_ast objects.
    - \c Z3_goal: set of formulas that can be solved and/or transformed using tactics and solvers.
    - \c Z3_tactic: basic building block for creating custom solvers for specific problem domains.
+   - \c Z3_simplifier: basic building block for creating custom pre-processing simplifiers.
    - \c Z3_probe: function/predicate used to inspect a goal and collect information that may be used to decide which solver and/or preprocessing step will be used.
    - \c Z3_apply_result: collection of subgoals resulting from applying of a tactic to a goal.
    - \c Z3_solver: (incremental) solver, possibly specialized by a particular tactic or logic.
@@ -1403,6 +1405,7 @@ typedef enum
   def_Type('PARSER_CONTEXT',   'Z3_parser_context',   'ParserContextObj')
   def_Type('GOAL',             'Z3_goal',             'GoalObj')
   def_Type('TACTIC',           'Z3_tactic',           'TacticObj')
+  def_Type('SIMPLIFIER',       'Z3_simplifier',       'SimplifierObj')
   def_Type('PARAMS',           'Z3_params',           'Params')
   def_Type('PROBE',            'Z3_probe',            'ProbeObj')
   def_Type('STATS',            'Z3_stats',            'StatsObj')
@@ -6207,7 +6210,7 @@ extern "C" {
 
     /**@}*/
 
-    /** @name Tactics and Probes */
+    /** @name Tactics, Simplifiers and Probes */
     /**@{*/
     /**
        \brief Return a tactic associated with the given name.
@@ -6359,6 +6362,97 @@ extern "C" {
     */
     Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p);
 
+
+    /**
+       \brief Return a simplifier associated with the given name.
+       The complete list of simplifiers may be obtained using the procedures #Z3_get_num_simplifiers and #Z3_get_simplifier_name.
+       It may also be obtained using the command \ccode{(help-simplifier)} in the SMT 2.0 front-end.
+
+       Simplifiers are the basic building block for creating custom solvers for specific problem domains.
+
+       def_API('Z3_mk_simplifier', SIMPLIFIER, (_in(CONTEXT), _in(STRING)))
+    */
+    Z3_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name);
+
+    /**
+       \brief Increment the reference counter of the given simplifier.
+
+       def_API('Z3_simplifier_inc_ref', VOID, (_in(CONTEXT), _in(SIMPLIFIER)))
+    */
+    void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t);
+
+    /**
+       \brief Decrement the reference counter of the given simplifier.
+
+       def_API('Z3_simplifier_dec_ref', VOID, (_in(CONTEXT), _in(SIMPLIFIER)))
+    */
+    void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g);
+
+    /**
+     \brief Attach simplifier to a solver. The solver will use the simplifier for incremental pre-processing.
+    
+        def_API('Z3_solver_add_simplifier', SOLVER, (_in(CONTEXT), _in(SOLVER), _in(SIMPLIFIER)))
+    */
+    Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier);
+
+    /**
+       \brief Return a simplifier that applies \c t1 to a given goal and \c t2
+       to every subgoal produced by \c t1.
+
+       def_API('Z3_simplifier_and_then', SIMPLIFIER, (_in(CONTEXT), _in(SIMPLIFIER), _in(SIMPLIFIER)))
+    */
+    Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2);
+
+    /**
+       \brief Return a simplifier that applies \c t using the given set of parameters.
+
+       def_API('Z3_simplifier_using_params', SIMPLIFIER, (_in(CONTEXT), _in(SIMPLIFIER), _in(PARAMS)))
+    */
+    Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p);
+
+
+    /**
+       \brief Return the number of builtin simplifiers available in Z3.
+
+       \sa Z3_get_simplifier_name
+
+       def_API('Z3_get_num_simplifiers', UINT, (_in(CONTEXT),))
+    */
+    unsigned Z3_API Z3_get_num_simplifiers(Z3_context c);
+
+    /**
+       \brief Return the name of the idx simplifier.
+
+       \pre i < Z3_get_num_simplifiers(c)
+
+       \sa Z3_get_num_simplifiers
+
+       def_API('Z3_get_simplifier_name', STRING, (_in(CONTEXT), _in(UINT)))
+    */
+    Z3_string Z3_API Z3_get_simplifier_name(Z3_context c, unsigned i);
+
+    /**
+       \brief Return a string containing a description of parameters accepted by the given simplifier.
+
+       def_API('Z3_simplifier_get_help', STRING, (_in(CONTEXT), _in(SIMPLIFIER)))
+    */
+    Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t);
+
+    /**
+       \brief Return the parameter description set for the given simplifier object.
+
+       def_API('Z3_simplifier_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(SIMPLIFIER)))
+    */
+    Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t);
+
+    /**
+       \brief Return a string containing a description of the simplifier with the given name.
+
+       def_API('Z3_simplifier_get_descr', STRING, (_in(CONTEXT), _in(STRING)))
+    */
+    Z3_string Z3_API Z3_simplifier_get_descr(Z3_context c, Z3_string name);
+
+
     /**
        \brief Return a probe that always evaluates to val.
 

src/cmd_context/tactic_manager.h

@@ -37,13 +37,15 @@ public:
     void insert(simplifier_cmd* c);
     void insert(probe_info * p);
     tactic_cmd * find_tactic_cmd(symbol const & s) const; 
-    probe_info * find_probe(symbol const & s) const; 
+    probe_info * find_probe(symbol const & s) const;     
     simplifier_cmd* find_simplifier_cmd(symbol const& s) const;
 
     unsigned num_tactics() const { return m_tactics.size(); }
     unsigned num_probes() const { return m_probes.size(); }
+    unsigned num_simplifiers() const { return m_simplifiers.size(); }
     tactic_cmd * get_tactic(unsigned i) const { return m_tactics[i]; }
     probe_info * get_probe(unsigned i) const { return m_probes[i]; }
+    simplifier_cmd *get_simplifier(unsigned i) const { return m_simplifiers[i]; }
 
     ptr_vector<simplifier_cmd> const& simplifiers() const { return m_simplifiers; }
     ptr_vector<tactic_cmd> const& tactics() const { return m_tactics; }