mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Removed dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
bee783fdd1
commit
13dda76ddb
|
|
@ -1,535 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
strategic_solver.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Strategies -> Solver
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-05-19
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#if 0
|
||||
#include"strategic_solver.h"
|
||||
#include"scoped_timer.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
|
||||
// minimum verbosity level for portfolio verbose messages
|
||||
#define PS_VB_LVL 15
|
||||
|
||||
|
||||
strategic_solver::ctx::ctx(ast_manager & m):
|
||||
m_assertions(m),
|
||||
m_assertion_names(m) {
|
||||
}
|
||||
|
||||
strategic_solver::strategic_solver():
|
||||
m_manager(0),
|
||||
m_force_tactic(false),
|
||||
m_inc_mode(false),
|
||||
m_check_sat_executed(false),
|
||||
m_inc_solver(0),
|
||||
m_inc_solver_timeout(UINT_MAX),
|
||||
m_inc_unknown_behavior(IUB_USE_TACTIC_IF_QF),
|
||||
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;);
|
||||
m_produce_proofs = false;
|
||||
m_produce_models = false;
|
||||
m_produce_unsat_cores = false;
|
||||
m_auto_config = true;
|
||||
}
|
||||
|
||||
strategic_solver::~strategic_solver() {
|
||||
SASSERT(!m_curr_tactic);
|
||||
dictionary<tactic_factory*>::iterator it = m_logic2fct.begin();
|
||||
dictionary<tactic_factory*>::iterator end = m_logic2fct.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->m_value);
|
||||
}
|
||||
if (m_proof)
|
||||
m().dec_ref(m_proof);
|
||||
if (m_core)
|
||||
m().dec_ref(m_core);
|
||||
}
|
||||
|
||||
bool strategic_solver::has_quantifiers() const {
|
||||
unsigned sz = get_num_assertions();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
if (::has_quantifiers(get_assertion(i)))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return true if a tactic should be used when the incremental solver returns unknown.
|
||||
*/
|
||||
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();
|
||||
case IUB_USE_TACTIC: return true;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
void strategic_solver::set_inc_solver(solver * s) {
|
||||
SASSERT(m_inc_solver == 0);
|
||||
SASSERT(m_num_scopes == 0);
|
||||
m_inc_solver = s;
|
||||
if (m_callback)
|
||||
m_inc_solver->set_progress_callback(m_callback);
|
||||
}
|
||||
|
||||
void strategic_solver::updt_params(params_ref const & p) {
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->updt_params(p);
|
||||
m_params = p;
|
||||
m_auto_config = p.get_bool("auto_config", true);
|
||||
}
|
||||
|
||||
void strategic_solver::collect_param_descrs(param_descrs & r) {
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->collect_param_descrs(r);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Set a timeout for each check_sat query that is processed by the inc_solver.
|
||||
timeout == UINT_MAX means infinite
|
||||
After the timeout a strategy is used.
|
||||
*/
|
||||
void strategic_solver::set_inc_solver_timeout(unsigned timeout) {
|
||||
m_inc_solver_timeout = timeout;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Set the default tactic factory.
|
||||
It is used if there is no tactic for a given logic.
|
||||
*/
|
||||
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::set_tactic_for(symbol const & logic, tactic_factory * fct) {
|
||||
tactic_factory * old_fct;
|
||||
if (m_logic2fct.find(logic, old_fct)) {
|
||||
dealloc(old_fct);
|
||||
}
|
||||
m_logic2fct.insert(logic, fct);
|
||||
}
|
||||
|
||||
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::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->init(m(), m_logic);
|
||||
unsigned sz = get_num_assertions();
|
||||
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::collect_statistics(statistics & st) const {
|
||||
if (m_use_inc_solver_results) {
|
||||
SASSERT(m_inc_solver);
|
||||
m_inc_solver->collect_statistics(st);
|
||||
}
|
||||
else {
|
||||
if (m_curr_tactic)
|
||||
m_curr_tactic->collect_statistics(st); // m_curr_tactic is still being executed.
|
||||
else
|
||||
st.copy(m_stats);
|
||||
}
|
||||
}
|
||||
|
||||
void strategic_solver::reset() {
|
||||
m_ctx = 0;
|
||||
m_logic = symbol::null;
|
||||
m_inc_mode = false;
|
||||
m_check_sat_executed = false;
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->reset();
|
||||
SASSERT(!m_curr_tactic);
|
||||
m_use_inc_solver_results = false;
|
||||
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::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();
|
||||
SASSERT(m_inc_solver == 0 || m_inc_mode);
|
||||
}
|
||||
if (m_inc_mode) {
|
||||
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::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::pop(unsigned n) {
|
||||
DEBUG_CODE({
|
||||
SASSERT(n <= m_num_scopes);
|
||||
m_num_scopes -= 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_scopes.size();
|
||||
}
|
||||
|
||||
struct aux_timeout_eh : public event_handler {
|
||||
solver * m_solver;
|
||||
volatile bool m_canceled;
|
||||
aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {}
|
||||
virtual void operator()() {
|
||||
m_solver->cancel();
|
||||
m_canceled = true;
|
||||
}
|
||||
};
|
||||
|
||||
struct strategic_solver::mk_tactic {
|
||||
strategic_solver * m_solver;
|
||||
|
||||
mk_tactic(strategic_solver * s, tactic_factory * f, params_ref const & p):m_solver(s) {
|
||||
ast_manager & m = s->m();
|
||||
tactic * tct = (*f)(m, p);
|
||||
tct->set_logic(s->m_logic);
|
||||
if (s->m_callback)
|
||||
tct->set_progress_callback(s->m_callback);
|
||||
#pragma omp critical (strategic_solver)
|
||||
{
|
||||
s->m_curr_tactic = tct;
|
||||
}
|
||||
}
|
||||
|
||||
~mk_tactic() {
|
||||
#pragma omp critical (strategic_solver)
|
||||
{
|
||||
m_solver->m_curr_tactic = 0;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
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::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;
|
||||
m_reason_unknown = "incomplete";
|
||||
return l_undef;
|
||||
}
|
||||
init_inc_solver();
|
||||
m_use_inc_solver_results = true;
|
||||
TRACE("strategic_solver", tout << "invoking inc_solver with " << num_assumptions << " assumptions\n";);
|
||||
return m_inc_solver->check_sat(num_assumptions, assumptions);
|
||||
}
|
||||
|
||||
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
|
||||
(!m_auto_config && !m_force_tactic) // auto config and force_tactic are turned off
|
||||
) {
|
||||
// must use incremental solver
|
||||
return check_sat_with_assumptions(num_assumptions, assumptions);
|
||||
}
|
||||
|
||||
tactic_factory * factory = get_tactic_factory();
|
||||
if (factory == 0)
|
||||
init_inc_solver(); // try to switch to incremental solver
|
||||
|
||||
if (m_inc_mode) {
|
||||
SASSERT(m_inc_solver);
|
||||
unsigned timeout = m_inc_solver_timeout;
|
||||
if (factory == 0)
|
||||
timeout = UINT_MAX; // there is no tactic available
|
||||
if (timeout == UINT_MAX) {
|
||||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "using incremental solver (without a timeout).\n";);
|
||||
m_use_inc_solver_results = true;
|
||||
lbool r = m_inc_solver->check_sat(0, 0);
|
||||
if (r != l_undef || factory == 0 || !use_tactic_when_undef()) {
|
||||
m_use_inc_solver_results = true;
|
||||
return r;
|
||||
}
|
||||
}
|
||||
else {
|
||||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "using incremental solver (with timeout).\n";);
|
||||
SASSERT(factory != 0);
|
||||
aux_timeout_eh eh(m_inc_solver.get());
|
||||
lbool r;
|
||||
{
|
||||
scoped_timer timer(m_inc_solver_timeout, &eh);
|
||||
r = m_inc_solver->check_sat(0, 0);
|
||||
}
|
||||
if ((r != l_undef || !use_tactic_when_undef()) && !eh.m_canceled) {
|
||||
m_use_inc_solver_results = true;
|
||||
return r;
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "incremental solver failed, trying tactic.\n";);
|
||||
}
|
||||
|
||||
m_use_inc_solver_results = false;
|
||||
|
||||
if (factory == 0) {
|
||||
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "there is no tactic available for the current logic.\n";);
|
||||
m_reason_unknown = "incomplete";
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
goal_ref g = alloc(goal, m(), m_produce_proofs, m_produce_models, m_produce_unsat_cores);
|
||||
unsigned sz = get_num_assertions();
|
||||
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, m_params);
|
||||
SASSERT(m_curr_tactic);
|
||||
|
||||
proof_ref pr(m());
|
||||
lbool r = ::check_sat(*(m_curr_tactic.get()), g, m_model, pr, core, m_reason_unknown);
|
||||
m_curr_tactic->collect_statistics(m_stats);
|
||||
if (pr) {
|
||||
m_proof = pr;
|
||||
m().inc_ref(m_proof);
|
||||
}
|
||||
if (core) {
|
||||
m_core = core;
|
||||
m().inc_ref(m_core);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
void strategic_solver::set_cancel(bool f) {
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->set_cancel(f);
|
||||
#pragma omp critical (strategic_solver)
|
||||
{
|
||||
if (m_curr_tactic)
|
||||
m_curr_tactic->set_cancel(f);
|
||||
}
|
||||
}
|
||||
|
||||
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::get_model(model_ref & m) {
|
||||
if (m_use_inc_solver_results) {
|
||||
SASSERT(m_inc_solver);
|
||||
m_inc_solver->get_model(m);
|
||||
}
|
||||
else {
|
||||
m = m_model;
|
||||
}
|
||||
}
|
||||
|
||||
proof * strategic_solver::get_proof() {
|
||||
if (m_use_inc_solver_results) {
|
||||
SASSERT(m_inc_solver);
|
||||
return m_inc_solver->get_proof();
|
||||
}
|
||||
else {
|
||||
return m_proof;
|
||||
}
|
||||
}
|
||||
|
||||
std::string strategic_solver::reason_unknown() const {
|
||||
if (m_use_inc_solver_results) {
|
||||
SASSERT(m_inc_solver);
|
||||
return m_inc_solver->reason_unknown();
|
||||
}
|
||||
return m_reason_unknown;
|
||||
}
|
||||
|
||||
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::set_progress_callback(progress_callback * callback) {
|
||||
m_callback = callback;
|
||||
if (m_inc_solver)
|
||||
m_inc_solver->set_progress_callback(callback);
|
||||
}
|
||||
|
||||
void strategic_solver::display(std::ostream & out) const {
|
||||
if (m_manager) {
|
||||
unsigned num = get_num_assertions();
|
||||
out << "(solver";
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
out << "\n " << mk_ismt2_pp(get_assertion(i), m(), 2);
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
else {
|
||||
out << "(solver)";
|
||||
}
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
@ -1,154 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
strategic_solver.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Strategies -> Solver
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-05-19
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _STRATEGIC_SOLVER_H_
|
||||
#define _STRATEGIC_SOLVER_H_
|
||||
|
||||
#include"solver.h"
|
||||
#include"tactic.h"
|
||||
|
||||
class progress_callback;
|
||||
|
||||
/**
|
||||
\brief Implementation of the solver API that supports:
|
||||
- a different tactic for each logic
|
||||
- a general purpose tactic
|
||||
- a default incremental solver
|
||||
|
||||
The strategic solver has two modes:
|
||||
- non-incremental
|
||||
- incremental
|
||||
In non-incremental mode, tactics are used.
|
||||
In incremental model, the incremental (general purpose) solver is used.
|
||||
|
||||
A timeout for the incremental solver can be specified.
|
||||
If the timeout is reached, then the strategic_solver tries to solve the problem using tactics.
|
||||
|
||||
The strategic_solver switches to incremental when:
|
||||
- push is used
|
||||
- assertions are peformed after a check_sat
|
||||
It goes back to non_incremental mode when:
|
||||
- reset is invoked.
|
||||
*/
|
||||
class strategic_solver : public solver {
|
||||
public:
|
||||
// Behavior when the incremental solver returns unknown.
|
||||
enum inc_unknown_behavior {
|
||||
IUB_RETURN_UNDEF, // just return unknown
|
||||
IUB_USE_TACTIC_IF_QF, // invoke tactic if problem is quantifier free
|
||||
IUB_USE_TACTIC // invoke tactic
|
||||
};
|
||||
|
||||
private:
|
||||
ast_manager * m_manager;
|
||||
params_ref m_params;
|
||||
symbol m_logic;
|
||||
bool m_force_tactic; // use tactics even when auto_config = false
|
||||
bool m_inc_mode;
|
||||
bool m_check_sat_executed;
|
||||
scoped_ptr<solver_factory> m_inc_solver_factory;
|
||||
ref<solver> m_inc_solver;
|
||||
unsigned m_inc_solver_timeout;
|
||||
inc_unknown_behavior m_inc_unknown_behavior;
|
||||
scoped_ptr<tactic_factory> m_default_fct;
|
||||
dictionary<tactic_factory*> m_logic2fct;
|
||||
|
||||
ref<tactic> m_curr_tactic;
|
||||
|
||||
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
|
||||
|
||||
bool m_produce_proofs;
|
||||
bool m_produce_models;
|
||||
bool m_produce_unsat_cores;
|
||||
|
||||
bool m_auto_config;
|
||||
|
||||
progress_callback * m_callback;
|
||||
|
||||
void reset_results();
|
||||
void init_inc_solver();
|
||||
tactic_factory * get_tactic_factory() const;
|
||||
lbool check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions);
|
||||
|
||||
struct mk_tactic;
|
||||
|
||||
bool has_quantifiers() const;
|
||||
bool use_tactic_when_undef() const;
|
||||
|
||||
public:
|
||||
strategic_solver(ast_manager & m, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic);
|
||||
~strategic_solver();
|
||||
|
||||
ast_manager & m() const { SASSERT(m_manager); return *m_manager; }
|
||||
|
||||
void set_inc_solver_factory(solver_factory * s);
|
||||
void set_inc_solver_timeout(unsigned timeout);
|
||||
void set_default_tactic(tactic_factory * fct);
|
||||
void set_tactic_for(symbol const & logic, tactic_factory * fct);
|
||||
void set_inc_unknown_behavior(inc_unknown_behavior b) { m_inc_unknown_behavior = b; }
|
||||
void force_tactic(bool f) { m_force_tactic = f; }
|
||||
|
||||
virtual void updt_params(params_ref const & p);
|
||||
virtual void collect_param_descrs(param_descrs & r);
|
||||
|
||||
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 void display(std::ostream & out) const;
|
||||
|
||||
virtual void init(ast_manager & m, symbol const & logic);
|
||||
virtual void collect_statistics(statistics & st) const;
|
||||
virtual void reset();
|
||||
virtual void assert_expr(expr * t);
|
||||
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();
|
||||
virtual std::string reason_unknown() const;
|
||||
virtual void get_labels(svector<symbol> & r);
|
||||
virtual void set_cancel(bool f);
|
||||
virtual void set_progress_callback(progress_callback * callback);
|
||||
};
|
||||
|
||||
#endif
|
||||
Loading…
Reference in a new issue