mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
cleanning solver initialization, and fixing named assertion support
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
181bdb6815
commit
b70687acc9
|
@ -33,14 +33,29 @@ Revision History:
|
|||
|
||||
extern "C" {
|
||||
|
||||
static void init_solver_core(Z3_context c, Z3_solver _s) {
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
Z3_solver_ref * s = to_solver(_s);
|
||||
s->m_solver->set_produce_proofs(m.proofs_enabled());
|
||||
s->m_solver->set_produce_unsat_cores(s->m_params.get_bool(":unsat-core", false));
|
||||
s->m_solver->set_produce_models(s->m_params.get_bool(":model", true));
|
||||
s->m_solver->set_front_end_params(mk_c(c)->fparams());
|
||||
s->m_solver->updt_params(s->m_params);
|
||||
s->m_solver->init(m, s->m_logic);
|
||||
s->m_initialized = true;
|
||||
}
|
||||
|
||||
static void init_solver(Z3_context c, Z3_solver s) {
|
||||
if (!to_solver(s)->m_initialized)
|
||||
init_solver_core(c, s);
|
||||
}
|
||||
|
||||
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_simple_solver(c);
|
||||
RESET_ERROR_CODE();
|
||||
Z3_solver_ref * s = alloc(Z3_solver_ref);
|
||||
s->m_solver = mk_smt_solver();
|
||||
s->m_solver->set_front_end_params(mk_c(c)->fparams());
|
||||
s->m_solver->init(mk_c(c)->m(), symbol::null);
|
||||
mk_c(c)->save_object(s);
|
||||
Z3_solver r = of_solver(s);
|
||||
RETURN_Z3(r);
|
||||
|
@ -53,8 +68,6 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
Z3_solver_ref * s = alloc(Z3_solver_ref);
|
||||
s->m_solver = mk_smt_strategic_solver();
|
||||
s->m_solver->set_front_end_params(mk_c(c)->fparams());
|
||||
s->m_solver->init(mk_c(c)->m(), symbol::null);
|
||||
mk_c(c)->save_object(s);
|
||||
Z3_solver r = of_solver(s);
|
||||
RETURN_Z3(r);
|
||||
|
@ -65,10 +78,8 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_mk_solver_for_logic(c, logic);
|
||||
RESET_ERROR_CODE();
|
||||
Z3_solver_ref * s = alloc(Z3_solver_ref);
|
||||
Z3_solver_ref * s = alloc(Z3_solver_ref, to_symbol(logic));
|
||||
s->m_solver = mk_smt_strategic_solver(true /* force solver to use tactics even when auto_config is disabled */);
|
||||
s->m_solver->set_front_end_params(mk_c(c)->fparams());
|
||||
s->m_solver->init(mk_c(c)->m(), to_symbol(logic));
|
||||
mk_c(c)->save_object(s);
|
||||
Z3_solver r = of_solver(s);
|
||||
RETURN_Z3(r);
|
||||
|
@ -81,8 +92,6 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
Z3_solver_ref * s = alloc(Z3_solver_ref);
|
||||
s->m_solver = alloc(tactic2solver, to_tactic_ref(t));
|
||||
s->m_solver->set_front_end_params(mk_c(c)->fparams());
|
||||
s->m_solver->init(mk_c(c)->m(), symbol::null);
|
||||
mk_c(c)->save_object(s);
|
||||
Z3_solver r = of_solver(s);
|
||||
RETURN_Z3(r);
|
||||
|
@ -117,7 +126,13 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_set_params(c, s, p);
|
||||
RESET_ERROR_CODE();
|
||||
to_solver_ref(s)->updt_params(to_param_ref(p));
|
||||
if (to_solver(s)->m_initialized) {
|
||||
bool old_model = to_solver(s)->m_params.get_bool(":model", true);
|
||||
bool new_model = to_param_ref(p).get_bool(":model", true);
|
||||
if (old_model != new_model)
|
||||
to_solver_ref(s)->set_produce_models(new_model);
|
||||
to_solver_ref(s)->updt_params(to_param_ref(p));
|
||||
}
|
||||
to_solver(s)->m_params = to_param_ref(p);
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
@ -142,6 +157,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_push(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
to_solver_ref(s)->push();
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
@ -150,6 +166,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_pop(c, s, n);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
if (n > to_solver_ref(s)->get_scope_level()) {
|
||||
SET_ERROR_CODE(Z3_IOB);
|
||||
return;
|
||||
|
@ -164,7 +181,7 @@ extern "C" {
|
|||
LOG_Z3_solver_reset(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
to_solver_ref(s)->reset();
|
||||
to_solver_ref(s)->init(mk_c(c)->m(), symbol::null);
|
||||
to_solver(s)->m_initialized = false;
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
|
@ -172,6 +189,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_get_num_scopes(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
return to_solver_ref(s)->get_scope_level();
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
@ -180,7 +198,8 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_assert(c, s, a);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_FORMULA(a,);
|
||||
init_solver(c, s);
|
||||
CHECK_FORMULA(a,);
|
||||
to_solver_ref(s)->assert_expr(to_expr(a));
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
@ -189,6 +208,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_get_assertions(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
|
||||
mk_c(c)->save_object(v);
|
||||
unsigned sz = to_solver_ref(s)->get_num_assertions();
|
||||
|
@ -207,9 +227,6 @@ extern "C" {
|
|||
}
|
||||
}
|
||||
expr * const * _assumptions = to_exprs(assumptions);
|
||||
to_solver_ref(s)->set_produce_models(to_solver(s)->m_params.get_bool(":model", true));
|
||||
to_solver_ref(s)->set_produce_proofs(mk_c(c)->m().proofs_enabled());
|
||||
to_solver_ref(s)->set_produce_unsat_cores(num_assumptions > 0);
|
||||
unsigned timeout = to_solver(s)->m_params.get_uint(":timeout", UINT_MAX);
|
||||
bool use_ctrl_c = to_solver(s)->m_params.get_bool(":ctrl-c", false);
|
||||
cancel_eh<solver> eh(*to_solver_ref(s));
|
||||
|
@ -233,6 +250,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_check(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
return _solver_check(c, s, 0, 0);
|
||||
Z3_CATCH_RETURN(Z3_L_UNDEF);
|
||||
}
|
||||
|
@ -241,6 +259,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_check_assumptions(c, s, num_assumptions, assumptions);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
return _solver_check(c, s, num_assumptions, assumptions);
|
||||
Z3_CATCH_RETURN(Z3_L_UNDEF);
|
||||
}
|
||||
|
@ -249,6 +268,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_get_model(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
model_ref _m;
|
||||
to_solver_ref(s)->get_model(_m);
|
||||
if (!_m) {
|
||||
|
@ -266,6 +286,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_get_proof(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
proof * p = to_solver_ref(s)->get_proof();
|
||||
if (!p) {
|
||||
SET_ERROR_CODE(Z3_INVALID_USAGE);
|
||||
|
@ -280,6 +301,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_get_unsat_core(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
ptr_vector<expr> core;
|
||||
to_solver_ref(s)->get_unsat_core(core);
|
||||
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
|
||||
|
@ -295,6 +317,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_get_reason_unknown(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
return mk_c(c)->mk_external_string(to_solver_ref(s)->reason_unknown());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
@ -303,6 +326,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_get_statistics(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
Z3_stats_ref * st = alloc(Z3_stats_ref);
|
||||
to_solver_ref(s)->collect_statistics(st->m_stats);
|
||||
mk_c(c)->save_object(st);
|
||||
|
@ -315,6 +339,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_solver_to_string(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
std::ostringstream buffer;
|
||||
to_solver_ref(s)->display(buffer);
|
||||
return mk_c(c)->mk_external_string(buffer.str());
|
||||
|
|
|
@ -24,7 +24,10 @@ Revision History:
|
|||
struct Z3_solver_ref : public api::object {
|
||||
solver * m_solver;
|
||||
params_ref m_params;
|
||||
Z3_solver_ref():m_solver(0) {}
|
||||
bool m_initialized;
|
||||
symbol m_logic;
|
||||
Z3_solver_ref():m_solver(0), m_initialized(false), m_logic(symbol::null) {}
|
||||
Z3_solver_ref(symbol const & logic):m_solver(0), m_initialized(false), m_logic(logic) {}
|
||||
virtual ~Z3_solver_ref() { dealloc(m_solver); }
|
||||
};
|
||||
|
||||
|
|
|
@ -359,14 +359,14 @@ class set_option_cmd : public set_get_option_cmd {
|
|||
}
|
||||
else if (m_option == m_produce_proofs) {
|
||||
check_not_initialized(ctx, m_produce_proofs);
|
||||
ctx.params().m_proof_mode = to_bool(value) ? PGM_FINE : PGM_DISABLED;
|
||||
ctx.set_produce_proofs(to_bool(value));
|
||||
}
|
||||
else if (m_option == m_produce_unsat_cores) {
|
||||
check_not_initialized(ctx, m_produce_unsat_cores);
|
||||
ctx.set_produce_unsat_cores(to_bool(value));
|
||||
}
|
||||
else if (m_option == m_produce_models) {
|
||||
ctx.params().m_model = to_bool(value);
|
||||
ctx.set_produce_models(to_bool(value));
|
||||
}
|
||||
else if (m_option == m_produce_assignments) {
|
||||
ctx.set_produce_assignments(to_bool(value));
|
||||
|
|
|
@ -348,6 +348,24 @@ cmd_context::~cmd_context() {
|
|||
}
|
||||
}
|
||||
|
||||
void cmd_context::set_produce_models(bool f) {
|
||||
params().m_model = f;
|
||||
if (m_solver)
|
||||
m_solver->set_produce_models(f);
|
||||
}
|
||||
|
||||
void cmd_context::set_produce_unsat_cores(bool f) {
|
||||
// can only be set before initialization
|
||||
SASSERT(!has_manager());
|
||||
m_produce_unsat_cores = f;
|
||||
}
|
||||
|
||||
void cmd_context::set_produce_proofs(bool f) {
|
||||
// can only be set before initialization
|
||||
SASSERT(!has_manager());
|
||||
params().m_proof_mode = f ? PGM_FINE : PGM_DISABLED;
|
||||
}
|
||||
|
||||
bool cmd_context::is_smtlib2_compliant() const {
|
||||
return params().m_smtlib2_compliant;
|
||||
}
|
||||
|
@ -540,8 +558,12 @@ void cmd_context::init_manager_core(bool new_manager) {
|
|||
// it prevents clashes with builtin types.
|
||||
insert(pm().mk_plist_decl());
|
||||
}
|
||||
if (m_solver)
|
||||
if (m_solver) {
|
||||
m_solver->set_produce_unsat_cores(m_produce_unsat_cores);
|
||||
m_solver->set_produce_models(params().m_model);
|
||||
m_solver->set_produce_proofs(params().m_proof_mode == PGM_FINE);
|
||||
m_solver->init(m(), m_logic);
|
||||
}
|
||||
m_check_logic.set_logic(m(), m_logic);
|
||||
}
|
||||
|
||||
|
@ -1258,9 +1280,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
|
|||
m_check_sat_result = m_solver.get(); // solver itself stores the result.
|
||||
m_solver->set_front_end_params(params());
|
||||
m_solver->set_progress_callback(this);
|
||||
m_solver->set_produce_proofs(produce_proofs());
|
||||
m_solver->set_produce_models(produce_models());
|
||||
m_solver->set_produce_unsat_cores(produce_unsat_cores());
|
||||
scoped_watch sw(*this);
|
||||
cancel_eh<solver> eh(*m_solver);
|
||||
scoped_ctrl_c ctrlc(eh);
|
||||
|
@ -1405,6 +1424,9 @@ void cmd_context::set_solver(solver * s) {
|
|||
m_solver = s;
|
||||
m_solver->set_front_end_params(params());
|
||||
if (has_manager() && s != 0) {
|
||||
m_solver->set_produce_unsat_cores(m_produce_unsat_cores);
|
||||
m_solver->set_produce_models(params().m_model);
|
||||
m_solver->set_produce_proofs(params().m_proof_mode == PGM_FINE);
|
||||
m_solver->init(m(), m_logic);
|
||||
// assert formulas and create scopes in the new solver.
|
||||
unsigned lim = 0;
|
||||
|
|
|
@ -270,7 +270,9 @@ public:
|
|||
bool produce_models() const;
|
||||
bool produce_proofs() const;
|
||||
bool produce_unsat_cores() const { return m_produce_unsat_cores; }
|
||||
void set_produce_unsat_cores(bool flag) { m_produce_unsat_cores = flag; }
|
||||
void set_produce_models(bool flag);
|
||||
void set_produce_unsat_cores(bool flag);
|
||||
void set_produce_proofs(bool flag);
|
||||
bool produce_assignments() const { return m_produce_assignments; }
|
||||
void set_produce_assignments(bool flag) { m_produce_assignments = flag; }
|
||||
void set_status(status st) { m_status = st; }
|
||||
|
|
|
@ -107,6 +107,7 @@ namespace smt {
|
|||
|
||||
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
|
||||
SASSERT(m_context);
|
||||
TRACE("solver_na2as", tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";);
|
||||
return m_context->check(num_assumptions, assumptions);
|
||||
}
|
||||
|
||||
|
|
|
@ -64,19 +64,20 @@ public:
|
|||
/**
|
||||
\brief Enable/Disable proof production for this solver object.
|
||||
|
||||
It is invoked after init(m, logic).
|
||||
It is invoked before init(m, logic).
|
||||
*/
|
||||
virtual void set_produce_proofs(bool f) {}
|
||||
/**
|
||||
\brief Enable/Disable model generation for this solver object.
|
||||
|
||||
It is invoked after init(m, logic).
|
||||
It is invoked before init(m, logic).
|
||||
The user may optionally invoke it after init(m, logic).
|
||||
*/
|
||||
virtual void set_produce_models(bool f) {}
|
||||
/**
|
||||
\brief Enable/Disable unsat core generation for this solver object.
|
||||
|
||||
It is invoked after init(m, logic).
|
||||
It is invoked before init(m, logic).
|
||||
*/
|
||||
virtual void set_produce_unsat_cores(bool f) {}
|
||||
|
||||
|
|
|
@ -25,7 +25,13 @@ Notes:
|
|||
// minimum verbosity level for portfolio verbose messages
|
||||
#define PS_VB_LVL 15
|
||||
|
||||
strategic_solver_core::strategic_solver_core():
|
||||
|
||||
strategic_solver::ctx::ctx(ast_manager & m):
|
||||
m_assertions(m),
|
||||
m_assertion_names(m) {
|
||||
}
|
||||
|
||||
strategic_solver::strategic_solver():
|
||||
m_manager(0),
|
||||
m_fparams(0),
|
||||
m_force_tactic(false),
|
||||
|
@ -37,6 +43,7 @@ strategic_solver_core::strategic_solver_core():
|
|||
m_default_fct(0),
|
||||
m_curr_tactic(0),
|
||||
m_proof(0),
|
||||
m_core(0),
|
||||
m_callback(0) {
|
||||
m_use_inc_solver_results = false;
|
||||
DEBUG_CODE(m_num_scopes = 0;);
|
||||
|
@ -45,7 +52,7 @@ strategic_solver_core::strategic_solver_core():
|
|||
m_produce_unsat_cores = false;
|
||||
}
|
||||
|
||||
strategic_solver_core::~strategic_solver_core() {
|
||||
strategic_solver::~strategic_solver() {
|
||||
SASSERT(!m_curr_tactic);
|
||||
dictionary<tactic_factory*>::iterator it = m_logic2fct.begin();
|
||||
dictionary<tactic_factory*>::iterator end = m_logic2fct.end();
|
||||
|
@ -54,9 +61,11 @@ strategic_solver_core::~strategic_solver_core() {
|
|||
}
|
||||
if (m_proof)
|
||||
m().dec_ref(m_proof);
|
||||
if (m_core)
|
||||
m().dec_ref(m_core);
|
||||
}
|
||||
|
||||
bool strategic_solver_core::has_quantifiers() const {
|
||||
bool strategic_solver::has_quantifiers() const {
|
||||
unsigned sz = get_num_assertions();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
if (::has_quantifiers(get_assertion(i)))
|
||||
|
@ -68,7 +77,7 @@ bool strategic_solver_core::has_quantifiers() const {
|
|||
/**
|
||||
\brief Return true if a tactic should be used when the incremental solver returns unknown.
|
||||
*/
|
||||
bool strategic_solver_core::use_tactic_when_undef() const {
|
||||
bool strategic_solver::use_tactic_when_undef() const {
|
||||
switch (m_inc_unknown_behavior) {
|
||||
case IUB_RETURN_UNDEF: return false;
|
||||
case IUB_USE_TACTIC_IF_QF: return !has_quantifiers();
|
||||
|
@ -79,7 +88,7 @@ bool strategic_solver_core::use_tactic_when_undef() const {
|
|||
}
|
||||
}
|
||||
|
||||
void strategic_solver_core::set_inc_solver(solver * s) {
|
||||
void strategic_solver::set_inc_solver(solver * s) {
|
||||
SASSERT(m_inc_solver == 0);
|
||||
SASSERT(m_num_scopes == 0);
|
||||
m_inc_solver = s;
|
||||
|
@ -87,7 +96,7 @@ void strategic_solver_core::set_inc_solver(solver * s) {
|
|||
m_inc_solver->set_progress_callback(m_callback);
|
||||
}
|
||||
|
||||
void strategic_solver_core::updt_params(params_ref const & p) {
|
||||
void strategic_solver::updt_params(params_ref const & p) {
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->updt_params(p);
|
||||
if (m_fparams)
|
||||
|
@ -95,7 +104,7 @@ void strategic_solver_core::updt_params(params_ref const & p) {
|
|||
}
|
||||
|
||||
|
||||
void strategic_solver_core::collect_param_descrs(param_descrs & r) {
|
||||
void strategic_solver::collect_param_descrs(param_descrs & r) {
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->collect_param_descrs(r);
|
||||
}
|
||||
|
@ -105,7 +114,7 @@ void strategic_solver_core::collect_param_descrs(param_descrs & r) {
|
|||
timeout == UINT_MAX means infinite
|
||||
After the timeout a strategy is used.
|
||||
*/
|
||||
void strategic_solver_core::set_inc_solver_timeout(unsigned timeout) {
|
||||
void strategic_solver::set_inc_solver_timeout(unsigned timeout) {
|
||||
m_inc_solver_timeout = timeout;
|
||||
}
|
||||
|
||||
|
@ -113,14 +122,14 @@ void strategic_solver_core::set_inc_solver_timeout(unsigned timeout) {
|
|||
\brief Set the default tactic factory.
|
||||
It is used if there is no tactic for a given logic.
|
||||
*/
|
||||
void strategic_solver_core::set_default_tactic(tactic_factory * fct) {
|
||||
void strategic_solver::set_default_tactic(tactic_factory * fct) {
|
||||
m_default_fct = fct;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Set a tactic factory for a given logic.
|
||||
*/
|
||||
void strategic_solver_core::set_tactic_for(symbol const & logic, tactic_factory * fct) {
|
||||
void strategic_solver::set_tactic_for(symbol const & logic, tactic_factory * fct) {
|
||||
tactic_factory * old_fct;
|
||||
if (m_logic2fct.find(logic, old_fct)) {
|
||||
dealloc(old_fct);
|
||||
|
@ -128,31 +137,77 @@ void strategic_solver_core::set_tactic_for(symbol const & logic, tactic_factory
|
|||
m_logic2fct.insert(logic, fct);
|
||||
}
|
||||
|
||||
void strategic_solver_core::init_core(ast_manager & m, symbol const & logic) {
|
||||
void strategic_solver::init(ast_manager & m, symbol const & logic) {
|
||||
m_manager = &m;
|
||||
m_logic = logic;
|
||||
if (m_inc_mode) {
|
||||
SASSERT(m_inc_solver);
|
||||
m_inc_solver->init(m, logic);
|
||||
}
|
||||
m_ctx = alloc(ctx, m);
|
||||
TRACE("strategic_solver", tout << "strategic_solver was initialized.\n";);
|
||||
}
|
||||
|
||||
unsigned strategic_solver::get_num_assertions() const {
|
||||
if (m_ctx == 0)
|
||||
return 0;
|
||||
return m_ctx->m_assertions.size();
|
||||
}
|
||||
|
||||
expr * strategic_solver::get_assertion(unsigned idx) const {
|
||||
SASSERT(m_ctx);
|
||||
return m_ctx->m_assertions.get(idx);
|
||||
}
|
||||
|
||||
expr * strategic_solver::get_assertion_name(unsigned idx) const {
|
||||
SASSERT(m_ctx);
|
||||
SASSERT(m_produce_unsat_cores);
|
||||
return m_ctx->m_assertion_names.get(idx);
|
||||
}
|
||||
|
||||
void strategic_solver::set_produce_proofs(bool f) {
|
||||
m_produce_proofs = f;
|
||||
// do not need to propagate to inc_solver since flag cannot be changed after initialization
|
||||
}
|
||||
|
||||
void strategic_solver::set_produce_models(bool f) {
|
||||
m_produce_models = f;
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->set_produce_models(f);
|
||||
}
|
||||
|
||||
void strategic_solver::set_produce_unsat_cores(bool f) {
|
||||
m_produce_unsat_cores = f;
|
||||
// do not need to propagate to inc_solver since flag cannot be changed after initialization
|
||||
}
|
||||
|
||||
// delayed inc solver initialization
|
||||
void strategic_solver_core::init_inc_solver() {
|
||||
void strategic_solver::init_inc_solver() {
|
||||
if (m_inc_mode)
|
||||
return; // solver was already initialized
|
||||
if (!m_inc_solver)
|
||||
return; // inc solver was not installed
|
||||
m_inc_mode = true;
|
||||
m_inc_solver->set_produce_proofs(m_produce_proofs);
|
||||
m_inc_solver->set_produce_models(m_produce_models);
|
||||
m_inc_solver->set_produce_unsat_cores(m_produce_unsat_cores);
|
||||
m_inc_solver->set_front_end_params(*m_fparams);
|
||||
m_inc_solver->init(m(), m_logic);
|
||||
unsigned sz = get_num_assertions();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
m_inc_solver->assert_expr(get_assertion(i));
|
||||
if (m_produce_unsat_cores) {
|
||||
SASSERT(m_ctx->m_assertions.size() == m_ctx->m_assertion_names.size());
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
m_inc_solver->assert_expr(get_assertion(i), get_assertion_name(i));
|
||||
}
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
m_inc_solver->assert_expr(get_assertion(i));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void strategic_solver_core::collect_statistics(statistics & st) const {
|
||||
void strategic_solver::collect_statistics(statistics & st) const {
|
||||
if (m_use_inc_solver_results) {
|
||||
SASSERT(m_inc_solver);
|
||||
m_inc_solver->collect_statistics(st);
|
||||
|
@ -165,7 +220,8 @@ void strategic_solver_core::collect_statistics(statistics & st) const {
|
|||
}
|
||||
}
|
||||
|
||||
void strategic_solver_core::reset_core() {
|
||||
void strategic_solver::reset() {
|
||||
m_ctx = 0;
|
||||
m_logic = symbol::null;
|
||||
m_inc_mode = false;
|
||||
m_check_sat_executed = false;
|
||||
|
@ -176,18 +232,22 @@ void strategic_solver_core::reset_core() {
|
|||
reset_results();
|
||||
}
|
||||
|
||||
void strategic_solver_core::reset_results() {
|
||||
void strategic_solver::reset_results() {
|
||||
m_use_inc_solver_results = false;
|
||||
m_model = 0;
|
||||
if (m_proof) {
|
||||
m().dec_ref(m_proof);
|
||||
m_proof = 0;
|
||||
}
|
||||
if (m_core) {
|
||||
m().dec_ref(m_core);
|
||||
m_core = 0;
|
||||
}
|
||||
m_reason_unknown.clear();
|
||||
m_stats.reset();
|
||||
}
|
||||
|
||||
void strategic_solver_core::assert_expr(expr * t) {
|
||||
void strategic_solver::assert_expr(expr * t) {
|
||||
if (m_check_sat_executed && !m_inc_mode) {
|
||||
// a check sat was already executed --> switch to incremental mode
|
||||
init_inc_solver();
|
||||
|
@ -197,16 +257,37 @@ void strategic_solver_core::assert_expr(expr * t) {
|
|||
SASSERT(m_inc_solver);
|
||||
m_inc_solver->assert_expr(t);
|
||||
}
|
||||
SASSERT(m_ctx);
|
||||
m_ctx->m_assertions.push_back(t);
|
||||
if (m_produce_unsat_cores)
|
||||
m_ctx->m_assertion_names.push_back(0);
|
||||
}
|
||||
|
||||
void strategic_solver_core::push_core() {
|
||||
void strategic_solver::assert_expr(expr * t, expr * a) {
|
||||
if (m_check_sat_executed && !m_inc_mode) {
|
||||
// a check sat was already executed --> switch to incremental mode
|
||||
init_inc_solver();
|
||||
SASSERT(m_inc_solver == 0 || m_inc_mode);
|
||||
}
|
||||
if (m_inc_mode) {
|
||||
SASSERT(m_inc_solver);
|
||||
m_inc_solver->assert_expr(t, a);
|
||||
}
|
||||
SASSERT(m_ctx);
|
||||
m_ctx->m_assertions.push_back(t);
|
||||
if (m_produce_unsat_cores)
|
||||
m_ctx->m_assertion_names.push_back(a);
|
||||
}
|
||||
|
||||
void strategic_solver::push() {
|
||||
DEBUG_CODE(m_num_scopes++;);
|
||||
init_inc_solver();
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->push();
|
||||
m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
|
||||
}
|
||||
|
||||
void strategic_solver_core::pop_core(unsigned n) {
|
||||
void strategic_solver::pop(unsigned n) {
|
||||
DEBUG_CODE({
|
||||
SASSERT(n <= m_num_scopes);
|
||||
m_num_scopes -= n;
|
||||
|
@ -214,6 +295,20 @@ void strategic_solver_core::pop_core(unsigned n) {
|
|||
init_inc_solver();
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->pop(n);
|
||||
|
||||
SASSERT(m_ctx);
|
||||
unsigned new_lvl = m_ctx->m_scopes.size() - n;
|
||||
unsigned old_sz = m_ctx->m_scopes[new_lvl];
|
||||
m_ctx->m_assertions.shrink(old_sz);
|
||||
if (m_produce_unsat_cores)
|
||||
m_ctx->m_assertion_names.shrink(old_sz);
|
||||
m_ctx->m_scopes.shrink(new_lvl);
|
||||
}
|
||||
|
||||
unsigned strategic_solver::get_scope_level() const {
|
||||
if (m_ctx == 0)
|
||||
return 0;
|
||||
return m_ctx->m_assertions.size();
|
||||
}
|
||||
|
||||
struct aux_timeout_eh : public event_handler {
|
||||
|
@ -226,10 +321,10 @@ struct aux_timeout_eh : public event_handler {
|
|||
}
|
||||
};
|
||||
|
||||
struct strategic_solver_core::mk_tactic {
|
||||
strategic_solver_core * m_solver;
|
||||
struct strategic_solver::mk_tactic {
|
||||
strategic_solver * m_solver;
|
||||
|
||||
mk_tactic(strategic_solver_core * s, tactic_factory * f):m_solver(s) {
|
||||
mk_tactic(strategic_solver * s, tactic_factory * f):m_solver(s) {
|
||||
ast_manager & m = s->m();
|
||||
params_ref p;
|
||||
front_end_params2params(*s->m_fparams, p);
|
||||
|
@ -252,14 +347,14 @@ struct strategic_solver_core::mk_tactic {
|
|||
}
|
||||
};
|
||||
|
||||
tactic_factory * strategic_solver_core::get_tactic_factory() const {
|
||||
tactic_factory * strategic_solver::get_tactic_factory() const {
|
||||
tactic_factory * f = 0;
|
||||
if (m_logic2fct.find(m_logic, f))
|
||||
return f;
|
||||
return m_default_fct.get();
|
||||
}
|
||||
|
||||
lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions) {
|
||||
lbool strategic_solver::check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions) {
|
||||
if (!m_inc_solver) {
|
||||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "incremental solver was not installed, returning unknown...\n";);
|
||||
m_use_inc_solver_results = false;
|
||||
|
@ -268,15 +363,16 @@ lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions
|
|||
}
|
||||
init_inc_solver();
|
||||
m_use_inc_solver_results = true;
|
||||
TRACE("solver_na2as", tout << "invoking inc_solver with " << num_assumptions << " assumptions\n";);
|
||||
TRACE("strategic_solver", tout << "invoking inc_solver with " << num_assumptions << " assumptions\n";);
|
||||
return m_inc_solver->check_sat(num_assumptions, assumptions);
|
||||
}
|
||||
|
||||
lbool strategic_solver_core::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
|
||||
TRACE("solver_na2as", tout << "assumptions at strategic_solver_core:\n";
|
||||
lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
|
||||
TRACE("strategic_solver", tout << "assumptions at strategic_solver:\n";
|
||||
for (unsigned i = 0; i < num_assumptions; i++) {
|
||||
tout << mk_ismt2_pp(assumptions[i], m()) << "\n";
|
||||
});
|
||||
}
|
||||
tout << "m_produce_unsat_cores: " << m_produce_unsat_cores << ", m_inc_mode: " << m_inc_mode << "\n";);
|
||||
reset_results();
|
||||
m_check_sat_executed = true;
|
||||
if (num_assumptions > 0 || // assumptions were provided
|
||||
|
@ -331,10 +427,18 @@ lbool strategic_solver_core::check_sat_core(unsigned num_assumptions, expr * con
|
|||
|
||||
goal_ref g = alloc(goal, m(), m_produce_proofs, m_produce_models, m_produce_unsat_cores);
|
||||
unsigned sz = get_num_assertions();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
g->assert_expr(get_assertion(i));
|
||||
if (m_produce_unsat_cores) {
|
||||
SASSERT(m_ctx->m_assertions.size() == m_ctx->m_assertion_names.size());
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
g->assert_expr(get_assertion(i), get_assertion_name(i));
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
g->assert_expr(get_assertion(i));
|
||||
}
|
||||
expr_dependency_ref core(m());
|
||||
|
||||
TRACE("strategic_solver", tout << "using goal...\n"; g->display_with_dependencies(tout););
|
||||
|
||||
mk_tactic tct_maker(this, factory);
|
||||
SASSERT(m_curr_tactic);
|
||||
|
@ -346,10 +450,14 @@ lbool strategic_solver_core::check_sat_core(unsigned num_assumptions, expr * con
|
|||
m_proof = pr;
|
||||
m().inc_ref(m_proof);
|
||||
}
|
||||
if (core) {
|
||||
m_core = core;
|
||||
m().inc_ref(m_core);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
void strategic_solver_core::set_cancel(bool f) {
|
||||
void strategic_solver::set_cancel(bool f) {
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->set_cancel(f);
|
||||
#pragma omp critical (strategic_solver)
|
||||
|
@ -359,15 +467,18 @@ void strategic_solver_core::set_cancel(bool f) {
|
|||
}
|
||||
}
|
||||
|
||||
void strategic_solver_core::get_unsat_core(ptr_vector<expr> & r) {
|
||||
TRACE("solver_na2as", tout << "get_unsat_core, m_use_inc_solver_results: " << m_use_inc_solver_results << "\n";);
|
||||
void strategic_solver::get_unsat_core(ptr_vector<expr> & r) {
|
||||
TRACE("strategic_solver", tout << "get_unsat_core, m_use_inc_solver_results: " << m_use_inc_solver_results << "\n";);
|
||||
if (m_use_inc_solver_results) {
|
||||
SASSERT(m_inc_solver);
|
||||
m_inc_solver->get_unsat_core(r);
|
||||
}
|
||||
else {
|
||||
m().linearize(m_core, r);
|
||||
}
|
||||
}
|
||||
|
||||
void strategic_solver_core::get_model(model_ref & m) {
|
||||
void strategic_solver::get_model(model_ref & m) {
|
||||
if (m_use_inc_solver_results) {
|
||||
SASSERT(m_inc_solver);
|
||||
m_inc_solver->get_model(m);
|
||||
|
@ -377,7 +488,7 @@ void strategic_solver_core::get_model(model_ref & m) {
|
|||
}
|
||||
}
|
||||
|
||||
proof * strategic_solver_core::get_proof() {
|
||||
proof * strategic_solver::get_proof() {
|
||||
if (m_use_inc_solver_results) {
|
||||
SASSERT(m_inc_solver);
|
||||
return m_inc_solver->get_proof();
|
||||
|
@ -387,7 +498,7 @@ proof * strategic_solver_core::get_proof() {
|
|||
}
|
||||
}
|
||||
|
||||
std::string strategic_solver_core::reason_unknown() const {
|
||||
std::string strategic_solver::reason_unknown() const {
|
||||
if (m_use_inc_solver_results) {
|
||||
SASSERT(m_inc_solver);
|
||||
return m_inc_solver->reason_unknown();
|
||||
|
@ -395,20 +506,20 @@ std::string strategic_solver_core::reason_unknown() const {
|
|||
return m_reason_unknown;
|
||||
}
|
||||
|
||||
void strategic_solver_core::get_labels(svector<symbol> & r) {
|
||||
void strategic_solver::get_labels(svector<symbol> & r) {
|
||||
if (m_use_inc_solver_results) {
|
||||
SASSERT(m_inc_solver);
|
||||
m_inc_solver->get_labels(r);
|
||||
}
|
||||
}
|
||||
|
||||
void strategic_solver_core::set_progress_callback(progress_callback * callback) {
|
||||
void strategic_solver::set_progress_callback(progress_callback * callback) {
|
||||
m_callback = callback;
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->set_progress_callback(callback);
|
||||
}
|
||||
|
||||
void strategic_solver_core::display(std::ostream & out) const {
|
||||
void strategic_solver::display(std::ostream & out) const {
|
||||
if (m_manager) {
|
||||
unsigned num = get_num_assertions();
|
||||
out << "(solver";
|
||||
|
@ -423,50 +534,7 @@ void strategic_solver_core::display(std::ostream & out) const {
|
|||
}
|
||||
|
||||
|
||||
strategic_solver::ctx::ctx(ast_manager & m):m_assertions(m) {
|
||||
}
|
||||
|
||||
void strategic_solver::init_core(ast_manager & m, symbol const & logic) {
|
||||
strategic_solver_core::init_core(m, logic);
|
||||
m_ctx = alloc(ctx, m);
|
||||
}
|
||||
|
||||
unsigned strategic_solver::get_num_assertions() const {
|
||||
if (m_ctx == 0)
|
||||
return 0;
|
||||
return m_ctx->m_assertions.size();
|
||||
}
|
||||
|
||||
expr * strategic_solver::get_assertion(unsigned idx) const {
|
||||
SASSERT(m_ctx);
|
||||
return m_ctx->m_assertions.get(idx);
|
||||
}
|
||||
|
||||
void strategic_solver::assert_expr(expr * t) {
|
||||
SASSERT(m_ctx);
|
||||
strategic_solver_core::assert_expr(t);
|
||||
m_ctx->m_assertions.push_back(t);
|
||||
}
|
||||
|
||||
void strategic_solver::push_core() {
|
||||
SASSERT(m_ctx);
|
||||
strategic_solver_core::push_core();
|
||||
m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
|
||||
}
|
||||
|
||||
void strategic_solver::pop_core(unsigned n) {
|
||||
SASSERT(m_ctx);
|
||||
unsigned new_lvl = m_ctx->m_scopes.size() - n;
|
||||
unsigned old_sz = m_ctx->m_scopes[new_lvl];
|
||||
m_ctx->m_assertions.shrink(old_sz);
|
||||
m_ctx->m_scopes.shrink(new_lvl);
|
||||
strategic_solver_core::pop_core(n);
|
||||
}
|
||||
|
||||
void strategic_solver::reset_core() {
|
||||
m_ctx = 0;
|
||||
strategic_solver_core::reset_core();
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
|
@ -19,7 +19,7 @@ Notes:
|
|||
#ifndef _STRATEGIC_SOLVER_H_
|
||||
#define _STRATEGIC_SOLVER_H_
|
||||
|
||||
#include"solver_na2as.h"
|
||||
#include"solver.h"
|
||||
#include"tactic.h"
|
||||
|
||||
class progress_callback;
|
||||
|
@ -46,7 +46,7 @@ struct front_end_params;
|
|||
It goes back to non_incremental mode when:
|
||||
- reset is invoked.
|
||||
*/
|
||||
class strategic_solver_core : public solver_na2as {
|
||||
class strategic_solver : public solver {
|
||||
public:
|
||||
// Behavior when the incremental solver returns unknown.
|
||||
enum inc_unknown_behavior {
|
||||
|
@ -73,9 +73,18 @@ private:
|
|||
bool m_use_inc_solver_results;
|
||||
model_ref m_model;
|
||||
proof * m_proof;
|
||||
expr_dependency * m_core;
|
||||
std::string m_reason_unknown;
|
||||
statistics m_stats;
|
||||
|
||||
struct ctx {
|
||||
expr_ref_vector m_assertions;
|
||||
expr_ref_vector m_assertion_names;
|
||||
unsigned_vector m_scopes;
|
||||
ctx(ast_manager & m);
|
||||
};
|
||||
scoped_ptr<ctx> m_ctx;
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
unsigned m_num_scopes;
|
||||
#endif
|
||||
|
@ -97,8 +106,8 @@ private:
|
|||
bool use_tactic_when_undef() const;
|
||||
|
||||
public:
|
||||
strategic_solver_core();
|
||||
~strategic_solver_core();
|
||||
strategic_solver();
|
||||
~strategic_solver();
|
||||
|
||||
ast_manager & m() const { SASSERT(m_manager); return *m_manager; }
|
||||
|
||||
|
@ -114,22 +123,25 @@ public:
|
|||
virtual void updt_params(params_ref const & p);
|
||||
virtual void collect_param_descrs(param_descrs & r);
|
||||
|
||||
virtual void set_produce_proofs(bool f) { m_produce_proofs = f; }
|
||||
virtual void set_produce_models(bool f) { m_produce_models = f; }
|
||||
virtual void set_produce_unsat_cores(bool f) { m_produce_unsat_cores = f; }
|
||||
virtual void set_produce_proofs(bool f);
|
||||
virtual void set_produce_models(bool f);
|
||||
virtual void set_produce_unsat_cores(bool f);
|
||||
|
||||
unsigned get_num_assertions() const;
|
||||
expr * get_assertion(unsigned idx) const;
|
||||
expr * get_assertion_name(unsigned idx) const;
|
||||
|
||||
virtual unsigned get_num_assertions() const = 0;
|
||||
virtual expr * get_assertion(unsigned idx) const = 0;
|
||||
|
||||
virtual void display(std::ostream & out) const;
|
||||
|
||||
virtual void init_core(ast_manager & m, symbol const & logic);
|
||||
virtual void init(ast_manager & m, symbol const & logic);
|
||||
virtual void collect_statistics(statistics & st) const;
|
||||
virtual void reset_core();
|
||||
virtual void reset();
|
||||
virtual void assert_expr(expr * t);
|
||||
virtual void push_core();
|
||||
virtual void pop_core(unsigned n);
|
||||
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions);
|
||||
virtual void assert_expr(expr * t, expr * a);
|
||||
virtual void push();
|
||||
virtual void pop(unsigned n);
|
||||
virtual unsigned get_scope_level() const;
|
||||
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
|
||||
virtual void get_unsat_core(ptr_vector<expr> & r);
|
||||
virtual void get_model(model_ref & m);
|
||||
virtual proof * get_proof();
|
||||
|
@ -139,30 +151,4 @@ public:
|
|||
virtual void set_progress_callback(progress_callback * callback);
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Default implementation of strategic_solver_core
|
||||
*/
|
||||
class strategic_solver : public strategic_solver_core {
|
||||
struct ctx {
|
||||
expr_ref_vector m_assertions;
|
||||
unsigned_vector m_scopes;
|
||||
ctx(ast_manager & m);
|
||||
};
|
||||
scoped_ptr<ctx> m_ctx;
|
||||
public:
|
||||
strategic_solver() {}
|
||||
|
||||
virtual void init_core(ast_manager & m, symbol const & logic);
|
||||
|
||||
virtual void assert_expr(expr * t);
|
||||
virtual void push_core();
|
||||
virtual void pop_core(unsigned n);
|
||||
virtual void reset_core();
|
||||
|
||||
virtual unsigned get_num_assertions() const;
|
||||
virtual expr * get_assertion(unsigned idx) const;
|
||||
};
|
||||
|
||||
|
||||
|
||||
#endif
|
||||
|
|
|
@ -209,6 +209,7 @@ class propagate_values_tactic : public tactic {
|
|||
result.push_back(m_goal);
|
||||
SASSERT(m_goal->is_well_sorted());
|
||||
TRACE("propagate_values", m_goal->display(tout););
|
||||
TRACE("propagate_values_core", m_goal->display_with_dependencies(tout););
|
||||
m_goal = 0;
|
||||
}
|
||||
};
|
||||
|
|
|
@ -233,6 +233,10 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
|
|||
quick_process(false, f, d);
|
||||
}
|
||||
|
||||
void goal::assert_expr(expr * f, expr_dependency * d) {
|
||||
assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, d);
|
||||
}
|
||||
|
||||
void goal::get_formulas(ptr_vector<expr> & result) {
|
||||
unsigned sz = size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
|
|
|
@ -105,9 +105,9 @@ public:
|
|||
void copy_from(goal const & src) { src.copy_to(*this); }
|
||||
|
||||
void assert_expr(expr * f, proof * pr, expr_dependency * d);
|
||||
void assert_expr(expr * f) {
|
||||
assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, 0);
|
||||
}
|
||||
void assert_expr(expr * f, expr_dependency * d);
|
||||
void assert_expr(expr * f, expr * d) { assert_expr(f, m().mk_leaf(d)); }
|
||||
void assert_expr(expr * f) { assert_expr(f, static_cast<expr_dependency*>(0)); }
|
||||
|
||||
unsigned size() const { return m().size(m_forms); }
|
||||
|
||||
|
|
|
@ -55,7 +55,7 @@ MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p));
|
|||
MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p));
|
||||
|
||||
static void init(strategic_solver_core * s) {
|
||||
static void init(strategic_solver * s) {
|
||||
s->set_default_tactic(alloc(default_fct));
|
||||
s->set_tactic_for(symbol("QF_UF"), alloc(qfuf_fct));
|
||||
s->set_tactic_for(symbol("QF_BV"), alloc(qfbv_fct));
|
||||
|
|
Loading…
Reference in a new issue