diff --git a/scripts/update_api.py b/scripts/update_api.py index a9753ec23..62b961d67 100755 --- a/scripts/update_api.py +++ b/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': diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 2ca54a599..0a3b35aed 100644 --- a/src/api/api_solver.cpp +++ b/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); diff --git a/src/api/api_solver.h b/src/api/api_solver.h index 71b7f9a46..a24668e49 100644 --- a/src/api/api_solver.h +++ b/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); diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index b3e3ca922..4e5156ba9 100644 --- a/src/api/api_tactic.cpp +++ b/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 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 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 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(""); + } + }; diff --git a/src/api/api_tactic.h b/src/api/api_tactic.h index 91e2d76ab..4a1da24bd 100644 --- a/src/api/api_tactic.h +++ b/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(g); } inline Z3_tactic of_tactic(Z3_tactic_ref * g) { return reinterpret_cast(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(g); } +inline Z3_simplifier of_simplifier(Z3_simplifier_ref * g) { return reinterpret_cast(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(g); } inline Z3_probe of_probe(Z3_probe_ref * g) { return reinterpret_cast(g); } inline probe * to_probe_ref(Z3_probe g) { return g == nullptr ? nullptr : to_probe(g)->m_probe.get(); } diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 3f47b6637..820818168 100644 --- a/src/api/c++/z3++.h +++ b/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) { diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index cf5be3e07..0f7ef8999 100644 --- a/src/api/python/z3/z3.py +++ b/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 diff --git a/src/api/python/z3/z3types.py b/src/api/python/z3/z3types.py index 500e3606e..9244e37d9 100644 --- a/src/api/python/z3/z3types.py +++ b/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): diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 88aaa8938..0582ffa37 100644 --- a/src/api/z3_api.h +++ b/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. diff --git a/src/cmd_context/tactic_manager.h b/src/cmd_context/tactic_manager.h index ec60b0873..b1e48a5ed 100644 --- a/src/cmd_context/tactic_manager.h +++ b/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 const& simplifiers() const { return m_simplifiers; } ptr_vector const& tactics() const { return m_tactics; }