mirror of
https://github.com/Z3Prover/z3
synced 2025-06-05 13:51:23 +00:00
checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
8a4f6d5719
commit
1ea606092c
50 changed files with 279 additions and 211 deletions
|
|
@ -21,6 +21,7 @@ Notes:
|
|||
#include"smt_solver.h"
|
||||
#include"front_end_params.h"
|
||||
#include"params2front_end_params.h"
|
||||
#include"rewriter_types.h"
|
||||
|
||||
class smt_tactic : public tactic {
|
||||
scoped_ptr<front_end_params> m_params;
|
||||
|
|
@ -146,159 +147,164 @@ public:
|
|||
model_converter_ref & mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
SASSERT(in->is_well_sorted());
|
||||
ast_manager & m = in->m();
|
||||
TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
|
||||
<< " PREPROCESS: " << fparams().m_preprocess << ", SOLVER:" << fparams().m_solver << "\n";
|
||||
tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n";
|
||||
tout << "params_ref: " << m_params_ref << "\n";);
|
||||
TRACE("smt_tactic_detail", in->display(tout););
|
||||
TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);
|
||||
scoped_init_ctx init(*this, m);
|
||||
SASSERT(m_ctx != 0);
|
||||
|
||||
scoped_ptr<expr2expr_map> dep2bool;
|
||||
scoped_ptr<expr2expr_map> bool2dep;
|
||||
ptr_vector<expr> assumptions;
|
||||
if (in->unsat_core_enabled()) {
|
||||
if (in->proofs_enabled())
|
||||
throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores");
|
||||
dep2bool = alloc(expr2expr_map);
|
||||
bool2dep = alloc(expr2expr_map);
|
||||
ptr_vector<expr> deps;
|
||||
ptr_vector<expr> clause;
|
||||
unsigned sz = in->size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * f = in->form(i);
|
||||
expr_dependency * d = in->dep(i);
|
||||
if (d == 0) {
|
||||
m_ctx->assert_expr(f);
|
||||
}
|
||||
else {
|
||||
// create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
|
||||
clause.reset();
|
||||
clause.push_back(f);
|
||||
deps.reset();
|
||||
m.linearize(d, deps);
|
||||
SASSERT(!deps.empty()); // d != 0, then deps must not be empty
|
||||
ptr_vector<expr>::iterator it = deps.begin();
|
||||
ptr_vector<expr>::iterator end = deps.end();
|
||||
for (; it != end; ++it) {
|
||||
expr * d = *it;
|
||||
if (is_uninterp_const(d) && m.is_bool(d)) {
|
||||
// no need to create a fresh boolean variable for d
|
||||
if (!bool2dep->contains(d)) {
|
||||
assumptions.push_back(d);
|
||||
bool2dep->insert(d, d);
|
||||
}
|
||||
clause.push_back(m.mk_not(d));
|
||||
}
|
||||
else {
|
||||
// must normalize assumption
|
||||
expr * b = 0;
|
||||
if (!dep2bool->find(d, b)) {
|
||||
b = m.mk_fresh_const(0, m.mk_bool_sort());
|
||||
dep2bool->insert(d, b);
|
||||
bool2dep->insert(b, d);
|
||||
assumptions.push_back(b);
|
||||
}
|
||||
clause.push_back(m.mk_not(b));
|
||||
}
|
||||
}
|
||||
SASSERT(clause.size() > 1);
|
||||
expr_ref cls(m);
|
||||
cls = m.mk_or(clause.size(), clause.c_ptr());
|
||||
m_ctx->assert_expr(cls);
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (in->proofs_enabled()) {
|
||||
unsigned sz = in->size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
m_ctx->assert_expr(in->form(i), in->pr(i));
|
||||
}
|
||||
}
|
||||
else {
|
||||
unsigned sz = in->size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
m_ctx->assert_expr(in->form(i));
|
||||
}
|
||||
}
|
||||
|
||||
lbool r;
|
||||
if (assumptions.empty())
|
||||
r = m_ctx->setup_and_check();
|
||||
else
|
||||
r = m_ctx->check(assumptions.size(), assumptions.c_ptr());
|
||||
m_ctx->collect_statistics(m_stats);
|
||||
|
||||
switch (r) {
|
||||
case l_true: {
|
||||
if (m_fail_if_inconclusive && !in->sat_preserved())
|
||||
throw tactic_exception("over-approximated goal found to be sat");
|
||||
// the empty assertion set is trivially satifiable.
|
||||
in->reset();
|
||||
result.push_back(in.get());
|
||||
// store the model in a do nothin model converter.
|
||||
if (in->models_enabled()) {
|
||||
model_ref md;
|
||||
m_ctx->get_model(md);
|
||||
mc = model2model_converter(md.get());
|
||||
}
|
||||
pc = 0;
|
||||
core = 0;
|
||||
return;
|
||||
}
|
||||
case l_false: {
|
||||
if (m_fail_if_inconclusive && !in->unsat_preserved()) {
|
||||
TRACE("smt_tactic", tout << "failed to show to be unsat...\n";);
|
||||
throw tactic_exception("under-approximated goal found to be unsat");
|
||||
}
|
||||
// formula is unsat, reset the goal, and store false there.
|
||||
in->reset();
|
||||
proof * pr = 0;
|
||||
expr_dependency * lcore = 0;
|
||||
if (in->proofs_enabled())
|
||||
pr = m_ctx->get_proof();
|
||||
try {
|
||||
SASSERT(in->is_well_sorted());
|
||||
ast_manager & m = in->m();
|
||||
TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
|
||||
<< " PREPROCESS: " << fparams().m_preprocess << ", SOLVER:" << fparams().m_solver << "\n";
|
||||
tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n";
|
||||
tout << "params_ref: " << m_params_ref << "\n";);
|
||||
TRACE("smt_tactic_detail", in->display(tout););
|
||||
TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);
|
||||
scoped_init_ctx init(*this, m);
|
||||
SASSERT(m_ctx != 0);
|
||||
|
||||
scoped_ptr<expr2expr_map> dep2bool;
|
||||
scoped_ptr<expr2expr_map> bool2dep;
|
||||
ptr_vector<expr> assumptions;
|
||||
if (in->unsat_core_enabled()) {
|
||||
unsigned sz = m_ctx->get_unsat_core_size();
|
||||
if (in->proofs_enabled())
|
||||
throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores");
|
||||
dep2bool = alloc(expr2expr_map);
|
||||
bool2dep = alloc(expr2expr_map);
|
||||
ptr_vector<expr> deps;
|
||||
ptr_vector<expr> clause;
|
||||
unsigned sz = in->size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * b = m_ctx->get_unsat_core_expr(i);
|
||||
SASSERT(is_uninterp_const(b) && m.is_bool(b));
|
||||
expr * d = bool2dep->find(b);
|
||||
lcore = m.mk_join(lcore, m.mk_leaf(d));
|
||||
}
|
||||
}
|
||||
in->assert_expr(m.mk_false(), pr, lcore);
|
||||
result.push_back(in.get());
|
||||
mc = 0;
|
||||
pc = 0;
|
||||
core = 0;
|
||||
return;
|
||||
}
|
||||
case l_undef:
|
||||
if (m_fail_if_inconclusive)
|
||||
throw tactic_exception("smt tactic failed to show goal to be sat/unsat");
|
||||
result.push_back(in.get());
|
||||
if (m_candidate_models) {
|
||||
switch (m_ctx->last_failure()) {
|
||||
case smt::NUM_CONFLICTS:
|
||||
case smt::THEORY:
|
||||
case smt::QUANTIFIERS:
|
||||
if (in->models_enabled()) {
|
||||
model_ref md;
|
||||
m_ctx->get_model(md);
|
||||
mc = model2model_converter(md.get());
|
||||
expr * f = in->form(i);
|
||||
expr_dependency * d = in->dep(i);
|
||||
if (d == 0) {
|
||||
m_ctx->assert_expr(f);
|
||||
}
|
||||
else {
|
||||
// create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
|
||||
clause.reset();
|
||||
clause.push_back(f);
|
||||
deps.reset();
|
||||
m.linearize(d, deps);
|
||||
SASSERT(!deps.empty()); // d != 0, then deps must not be empty
|
||||
ptr_vector<expr>::iterator it = deps.begin();
|
||||
ptr_vector<expr>::iterator end = deps.end();
|
||||
for (; it != end; ++it) {
|
||||
expr * d = *it;
|
||||
if (is_uninterp_const(d) && m.is_bool(d)) {
|
||||
// no need to create a fresh boolean variable for d
|
||||
if (!bool2dep->contains(d)) {
|
||||
assumptions.push_back(d);
|
||||
bool2dep->insert(d, d);
|
||||
}
|
||||
clause.push_back(m.mk_not(d));
|
||||
}
|
||||
else {
|
||||
// must normalize assumption
|
||||
expr * b = 0;
|
||||
if (!dep2bool->find(d, b)) {
|
||||
b = m.mk_fresh_const(0, m.mk_bool_sort());
|
||||
dep2bool->insert(d, b);
|
||||
bool2dep->insert(b, d);
|
||||
assumptions.push_back(b);
|
||||
}
|
||||
clause.push_back(m.mk_not(b));
|
||||
}
|
||||
}
|
||||
SASSERT(clause.size() > 1);
|
||||
expr_ref cls(m);
|
||||
cls = m.mk_or(clause.size(), clause.c_ptr());
|
||||
m_ctx->assert_expr(cls);
|
||||
}
|
||||
pc = 0;
|
||||
core = 0;
|
||||
return;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
m_failure = m_ctx->last_failure_as_string();
|
||||
throw tactic_exception(m_failure.c_str());
|
||||
else if (in->proofs_enabled()) {
|
||||
unsigned sz = in->size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
m_ctx->assert_expr(in->form(i), in->pr(i));
|
||||
}
|
||||
}
|
||||
else {
|
||||
unsigned sz = in->size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
m_ctx->assert_expr(in->form(i));
|
||||
}
|
||||
}
|
||||
|
||||
lbool r;
|
||||
if (assumptions.empty())
|
||||
r = m_ctx->setup_and_check();
|
||||
else
|
||||
r = m_ctx->check(assumptions.size(), assumptions.c_ptr());
|
||||
m_ctx->collect_statistics(m_stats);
|
||||
|
||||
switch (r) {
|
||||
case l_true: {
|
||||
if (m_fail_if_inconclusive && !in->sat_preserved())
|
||||
throw tactic_exception("over-approximated goal found to be sat");
|
||||
// the empty assertion set is trivially satifiable.
|
||||
in->reset();
|
||||
result.push_back(in.get());
|
||||
// store the model in a do nothin model converter.
|
||||
if (in->models_enabled()) {
|
||||
model_ref md;
|
||||
m_ctx->get_model(md);
|
||||
mc = model2model_converter(md.get());
|
||||
}
|
||||
pc = 0;
|
||||
core = 0;
|
||||
return;
|
||||
}
|
||||
case l_false: {
|
||||
if (m_fail_if_inconclusive && !in->unsat_preserved()) {
|
||||
TRACE("smt_tactic", tout << "failed to show to be unsat...\n";);
|
||||
throw tactic_exception("under-approximated goal found to be unsat");
|
||||
}
|
||||
// formula is unsat, reset the goal, and store false there.
|
||||
in->reset();
|
||||
proof * pr = 0;
|
||||
expr_dependency * lcore = 0;
|
||||
if (in->proofs_enabled())
|
||||
pr = m_ctx->get_proof();
|
||||
if (in->unsat_core_enabled()) {
|
||||
unsigned sz = m_ctx->get_unsat_core_size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * b = m_ctx->get_unsat_core_expr(i);
|
||||
SASSERT(is_uninterp_const(b) && m.is_bool(b));
|
||||
expr * d = bool2dep->find(b);
|
||||
lcore = m.mk_join(lcore, m.mk_leaf(d));
|
||||
}
|
||||
}
|
||||
in->assert_expr(m.mk_false(), pr, lcore);
|
||||
result.push_back(in.get());
|
||||
mc = 0;
|
||||
pc = 0;
|
||||
core = 0;
|
||||
return;
|
||||
}
|
||||
case l_undef:
|
||||
if (m_fail_if_inconclusive)
|
||||
throw tactic_exception("smt tactic failed to show goal to be sat/unsat");
|
||||
result.push_back(in.get());
|
||||
if (m_candidate_models) {
|
||||
switch (m_ctx->last_failure()) {
|
||||
case smt::NUM_CONFLICTS:
|
||||
case smt::THEORY:
|
||||
case smt::QUANTIFIERS:
|
||||
if (in->models_enabled()) {
|
||||
model_ref md;
|
||||
m_ctx->get_model(md);
|
||||
mc = model2model_converter(md.get());
|
||||
}
|
||||
pc = 0;
|
||||
core = 0;
|
||||
return;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
m_failure = m_ctx->last_failure_as_string();
|
||||
throw tactic_exception(m_failure.c_str());
|
||||
}
|
||||
}
|
||||
catch (rewriter_exception & ex) {
|
||||
throw tactic_exception(ex.msg());
|
||||
}
|
||||
}
|
||||
};
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue