3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00

set solver on simplify command

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-27 15:35:44 -07:00
parent 0997eba700
commit b7de813c63
5 changed files with 48 additions and 3 deletions

View file

@ -149,6 +149,9 @@ public:
void updt_params(params_ref const & p) {}
static void get_param_descrs(param_descrs & r) {}
void set_solver(expr_solver* solver) { m_re2aut.set_solver(solver); }
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);

View file

@ -692,6 +692,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
return false;
}
};
template class rewriter_tpl<th_rewriter_cfg>;
@ -705,6 +706,10 @@ struct th_rewriter::imp : public rewriter_tpl<th_rewriter_cfg> {
expr_ref mk_app(func_decl* f, unsigned sz, expr* const* args) {
return m_cfg.mk_app(f, sz, args);
}
void set_solver(expr_solver* solver) {
m_cfg.m_seq_rw.set_solver(solver);
}
};
th_rewriter::th_rewriter(ast_manager & m, params_ref const & p):
@ -790,3 +795,7 @@ void th_rewriter::reset_used_dependencies() {
expr_ref th_rewriter::mk_app(func_decl* f, unsigned num_args, expr* const* args) {
return m_imp->mk_app(f, num_args, args);
}
void th_rewriter::set_solver(expr_solver* solver) {
m_imp->set_solver(solver);
}

View file

@ -25,6 +25,8 @@ Notes:
class expr_substitution;
class expr_solver;
class th_rewriter {
struct imp;
imp * m_imp;
@ -58,6 +60,9 @@ public:
// Remark: reset_used_dependecies will reset the internal cache if get_used_dependencies() != 0
expr_dependency * get_used_dependencies();
void reset_used_dependencies();
void set_solver(expr_solver* solver);
};
#endif

View file

@ -24,9 +24,30 @@ Notes:
#include"scoped_timer.h"
#include"scoped_ctrl_c.h"
#include"cancel_eh.h"
#include"seq_rewriter.h"
#include<iomanip>
class simplify_cmd : public parametric_cmd {
class th_solver : public expr_solver {
cmd_context& m_ctx;
params_ref m_params;
ref<solver> m_solver;
public:
th_solver(cmd_context& ctx): m_ctx(ctx) {}
virtual lbool check_sat(expr* e) {
if (!m_solver) {
m_solver = m_ctx.get_solver_factory()(m_ctx.m(), m_params, false, true, false, symbol::null);
}
m_solver->push();
m_solver->assert_expr(e);
lbool r = m_solver->check_sat(0,0);
m_solver->pop(1);
return r;
}
};
expr * m_target;
public:
simplify_cmd(char const * name = "simplify"):parametric_cmd(name) {}
@ -70,10 +91,12 @@ public:
if (m_params.get_bool("som", false))
m_params.set_bool("flat", true);
th_rewriter s(ctx.m(), m_params);
th_solver solver(ctx);
s.set_solver(alloc(th_solver, ctx));
unsigned cache_sz;
unsigned num_steps = 0;
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
unsigned rlimit = m_params.get_uint("rlimit", UINT_MAX);
unsigned rlimit = m_params.get_uint("rlimit", UINT_MAX);
bool failed = false;
cancel_eh<reslimit> eh(ctx.m().limit());
{

View file

@ -149,8 +149,13 @@ public:
*/
virtual expr * get_assumption(unsigned idx) const = 0;
/**
\brief under assumptions, asms, retrieve set of consequences that fix values for expressions that can be
built from fns. For functions that take 0 arguments, we require that the function returns all consequences
that mention these functions. The consequences are clauses whose first literal constrain one of the
functions from fns and the other literals are negations of literals from asms.
*/
//virtual lbool get_consequences(expr_ref_vector const& asms, func_ref_vector const& fns, expr_ref_vector& consequences);
/**
\brief Display the content of this solver.