mirror of
https://github.com/Z3Prover/z3
synced 2025-05-11 09:44:43 +00:00
synchronize fork
This commit is contained in:
nilsbecker
nilsbecker
commit
820c14ed06
430 changed files with 19930 additions and 13462 deletions
|
|
@ -15,12 +15,19 @@ Author:
|
|||
|
||||
Revision History:
|
||||
|
||||
- to support lambdas/array models:
|
||||
binding sk -> (as-array k!0)
|
||||
then include definition for k!0 as part of binding.
|
||||
Binding instance can be a pointer into m_pinned expressions.
|
||||
|
||||
--*/
|
||||
|
||||
#include "ast/normal_forms/pull_quant.h"
|
||||
#include "ast/for_each_expr.h"
|
||||
#include "ast/rewriter/var_subst.h"
|
||||
#include "ast/rewriter/rewriter_def.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/array_decl_plugin.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "smt/smt_model_checker.h"
|
||||
#include "smt/smt_context.h"
|
||||
|
|
@ -54,8 +61,8 @@ namespace smt {
|
|||
}
|
||||
|
||||
void model_checker::set_qm(quantifier_manager & qm) {
|
||||
SASSERT(m_qm == 0);
|
||||
SASSERT(m_context == 0);
|
||||
SASSERT(m_qm == nullptr);
|
||||
SASSERT(m_context == nullptr);
|
||||
m_qm = &qm;
|
||||
m_context = &(m_qm->get_context());
|
||||
}
|
||||
|
|
@ -64,6 +71,13 @@ namespace smt {
|
|||
\brief Return a term in the context that evaluates to val.
|
||||
*/
|
||||
expr * model_checker::get_term_from_ctx(expr * val) {
|
||||
init_value2expr();
|
||||
expr * t = nullptr;
|
||||
m_value2expr.find(val, t);
|
||||
return t;
|
||||
}
|
||||
|
||||
void model_checker::init_value2expr() {
|
||||
if (m_value2expr.empty()) {
|
||||
// populate m_value2expr
|
||||
for (auto const& kv : *m_root2value) {
|
||||
|
|
@ -73,9 +87,28 @@ namespace smt {
|
|||
m_value2expr.insert(val, n->get_owner());
|
||||
}
|
||||
}
|
||||
expr * t = nullptr;
|
||||
m_value2expr.find(val, t);
|
||||
return t;
|
||||
}
|
||||
|
||||
expr_ref model_checker::replace_value_from_ctx(expr * e) {
|
||||
init_value2expr();
|
||||
struct beta_reducer_cfg : default_rewriter_cfg {
|
||||
model_checker& mc;
|
||||
beta_reducer_cfg(model_checker& mc):mc(mc) {}
|
||||
bool get_subst(expr * e, expr* & t, proof *& pr) {
|
||||
t = nullptr; pr = nullptr;
|
||||
mc.m_value2expr.find(e, t);
|
||||
return t != nullptr;
|
||||
}
|
||||
};
|
||||
struct beta_reducer : public rewriter_tpl<beta_reducer_cfg> {
|
||||
beta_reducer_cfg m_cfg;
|
||||
beta_reducer(model_checker& m):
|
||||
rewriter_tpl<beta_reducer_cfg>(m.m, false, m_cfg), m_cfg(m) {}
|
||||
};
|
||||
beta_reducer br(*this);
|
||||
expr_ref result(m);
|
||||
br(e, result);
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -95,8 +128,6 @@ namespace smt {
|
|||
m_aux_context->assert_expr(fml);
|
||||
}
|
||||
|
||||
#define PP_DEPTH 8
|
||||
|
||||
/**
|
||||
\brief Assert the negation of q after applying the interpretation in m_curr_model to the uninterpreted symbols in q.
|
||||
|
||||
|
|
@ -123,9 +154,8 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
expr_ref sk_body(m);
|
||||
var_subst s(m);
|
||||
s(tmp, subst_args.size(), subst_args.c_ptr(), sk_body);
|
||||
expr_ref sk_body = s(tmp, subst_args.size(), subst_args.c_ptr());
|
||||
expr_ref r(m);
|
||||
r = m.mk_not(sk_body);
|
||||
TRACE("model_checker", tout << "mk_neg_q_m:\n" << mk_ismt2_pp(r, m) << "\n";);
|
||||
|
|
@ -133,37 +163,35 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) {
|
||||
if (cex == nullptr) {
|
||||
if (cex == nullptr || sks.empty()) {
|
||||
TRACE("model_checker", tout << "no model is available\n";);
|
||||
return false;
|
||||
}
|
||||
array_util autil(m);
|
||||
unsigned num_decls = q->get_num_decls();
|
||||
// Remark: sks were created for the flat version of q.
|
||||
SASSERT(sks.size() >= num_decls);
|
||||
expr_ref_vector bindings(m);
|
||||
expr_ref_vector bindings(m), defs(m);
|
||||
expr_ref def(m);
|
||||
bindings.resize(num_decls);
|
||||
unsigned max_generation = 0;
|
||||
for (unsigned i = 0; i < num_decls; i++) {
|
||||
expr * sk = sks.get(num_decls - i - 1);
|
||||
func_decl * sk_d = to_app(sk)->get_decl();
|
||||
expr_ref sk_value(m);
|
||||
sk_value = cex->get_const_interp(sk_d);
|
||||
if (sk_value == 0) {
|
||||
sk_value = cex->get_some_value(sk_d->get_range());
|
||||
if (sk_value == 0) {
|
||||
TRACE("model_checker", tout << "Could not get value for " << sk_d->get_name() << "\n";);
|
||||
return false; // get_some_value failed... giving up
|
||||
}
|
||||
TRACE("model_checker", tout << "Got some value " << sk_value << "\n";);
|
||||
expr_ref sk_value(cex->get_some_const_interp(sk_d), m);
|
||||
if (!sk_value) {
|
||||
TRACE("model_checker", tout << "Could not get value for " << sk_d->get_name() << "\n";);
|
||||
return false; // get_some_value failed... giving up
|
||||
}
|
||||
TRACE("model_checker", tout << "Got some value " << sk_value << "\n";);
|
||||
|
||||
if (use_inv) {
|
||||
unsigned sk_term_gen;
|
||||
expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen);
|
||||
if (sk_term != nullptr) {
|
||||
TRACE("model_checker", tout << "Found inverse " << mk_pp(sk_term, m) << "\n";);
|
||||
SASSERT(!m.is_model_value(sk_term));
|
||||
if (sk_term_gen > max_generation)
|
||||
max_generation = sk_term_gen;
|
||||
max_generation = std::max(sk_term_gen, max_generation);
|
||||
sk_value = sk_term;
|
||||
}
|
||||
else {
|
||||
|
|
@ -181,39 +209,48 @@ namespace smt {
|
|||
TRACE("model_checker", tout << "value is private to model: " << sk_value << "\n";);
|
||||
return false;
|
||||
}
|
||||
func_decl * f = nullptr;
|
||||
if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f)) {
|
||||
expr_ref body(cex->get_func_interp(f)->get_interp(), m);
|
||||
ptr_vector<sort> sorts(f->get_arity(), f->get_domain());
|
||||
svector<symbol> names;
|
||||
for (unsigned i = 0; i < f->get_arity(); ++i) {
|
||||
names.push_back(symbol(i));
|
||||
}
|
||||
defined_names dn(m);
|
||||
body = replace_value_from_ctx(body);
|
||||
body = m.mk_lambda(sorts.size(), sorts.c_ptr(), names.c_ptr(), body);
|
||||
// sk_value = m.mk_fresh_const(0, m.get_sort(sk_value)); // get rid of as-array
|
||||
body = dn.mk_definition(body, to_app(sk_value));
|
||||
defs.push_back(body);
|
||||
}
|
||||
bindings.set(num_decls - i - 1, sk_value);
|
||||
}
|
||||
|
||||
TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: ";
|
||||
for (unsigned i = 0; i < num_decls; i++) {
|
||||
tout << mk_ismt2_pp(bindings[i].get(), m) << " ";
|
||||
}
|
||||
tout << "\n";);
|
||||
|
||||
TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\n" << defs << "\n";);
|
||||
if (!defs.empty()) def = mk_and(defs);
|
||||
max_generation = std::max(m_qm->get_generation(q), max_generation);
|
||||
add_instance(q, bindings, max_generation);
|
||||
add_instance(q, bindings, max_generation, def.get());
|
||||
return true;
|
||||
}
|
||||
|
||||
void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) {
|
||||
void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation, expr* def) {
|
||||
SASSERT(q->get_num_decls() == bindings.size());
|
||||
for (expr* b : bindings)
|
||||
m_pinned_exprs.push_back(b);
|
||||
unsigned offset = m_pinned_exprs.size();
|
||||
m_pinned_exprs.append(bindings);
|
||||
m_pinned_exprs.push_back(q);
|
||||
|
||||
void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls()));
|
||||
instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation);
|
||||
m_new_instances.push_back(new_inst);
|
||||
m_pinned_exprs.push_back(def);
|
||||
m_new_instances.push_back(instance(q, offset, def, max_generation));
|
||||
}
|
||||
|
||||
void model_checker::operator()(expr *n) {
|
||||
if (m.is_model_value(n) || m_autil.is_as_array(n)) {
|
||||
if (m.is_model_value(n) /*|| m_autil.is_as_array(n)*/) {
|
||||
throw is_model_value();
|
||||
}
|
||||
}
|
||||
|
||||
bool model_checker::contains_model_value(expr* n) {
|
||||
if (m.is_model_value(n) || m_autil.is_as_array(n)) {
|
||||
if (m.is_model_value(n) /*|| m_autil.is_as_array(n)*/) {
|
||||
return true;
|
||||
}
|
||||
if (is_app(n) && to_app(n)->get_num_args() == 0) {
|
||||
|
|
@ -231,16 +268,13 @@ namespace smt {
|
|||
|
||||
|
||||
bool model_checker::add_blocking_clause(model * cex, expr_ref_vector & sks) {
|
||||
SASSERT(cex != 0);
|
||||
SASSERT(cex != nullptr);
|
||||
expr_ref_buffer diseqs(m);
|
||||
for (expr * sk : sks) {
|
||||
func_decl * sk_d = to_app(sk)->get_decl();
|
||||
expr_ref sk_value(m);
|
||||
sk_value = cex->get_const_interp(sk_d);
|
||||
if (sk_value == 0) {
|
||||
sk_value = cex->get_some_value(sk_d->get_range());
|
||||
if (sk_value == 0)
|
||||
return false; // get_some_value failed... aborting add_blocking_clause
|
||||
expr_ref sk_value(cex->get_some_const_interp(sk_d), m);
|
||||
if (!sk_value) {
|
||||
return false; // get_some_value failed... aborting add_blocking_clause
|
||||
}
|
||||
diseqs.push_back(m.mk_not(m.mk_eq(sk, sk_value)));
|
||||
}
|
||||
|
|
@ -251,40 +285,43 @@ namespace smt {
|
|||
return true;
|
||||
}
|
||||
|
||||
struct scoped_ctx_push {
|
||||
context* c;
|
||||
scoped_ctx_push(context* c): c(c) { c->push(); }
|
||||
~scoped_ctx_push() { c->pop(1); }
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Return true if q is satisfied by m_curr_model.
|
||||
*/
|
||||
bool model_checker::check(quantifier * q) {
|
||||
SASSERT(!m_aux_context->relevancy());
|
||||
m_aux_context->push();
|
||||
scoped_ctx_push _push(m_aux_context.get());
|
||||
|
||||
quantifier * flat_q = get_flat_quantifier(q);
|
||||
TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" <<
|
||||
mk_ismt2_pp(flat_q->get_expr(), m) << "\n";);
|
||||
TRACE("model_checker", tout << "model checking:\n" << expr_ref(q->get_expr(), m) << "\n" << expr_ref(flat_q->get_expr(), m) << "\n";);
|
||||
expr_ref_vector sks(m);
|
||||
|
||||
assert_neg_q_m(flat_q, sks);
|
||||
TRACE("model_checker", tout << "skolems:\n";
|
||||
for (expr* sk : sks) {
|
||||
tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n";
|
||||
});
|
||||
TRACE("model_checker", tout << "skolems:\n" << sks << "\n";);
|
||||
|
||||
flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true);
|
||||
lbool r = m_aux_context->check();
|
||||
TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";);
|
||||
if (r != l_true) {
|
||||
m_aux_context->pop(1);
|
||||
if (r != l_true) {
|
||||
return r == l_false; // quantifier is satisfied by m_curr_model
|
||||
}
|
||||
|
||||
model_ref complete_cex;
|
||||
m_aux_context->get_model(complete_cex);
|
||||
|
||||
|
||||
// try to find new instances using instantiation sets.
|
||||
m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks);
|
||||
|
||||
|
||||
unsigned num_new_instances = 0;
|
||||
|
||||
|
||||
while (true) {
|
||||
flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true);
|
||||
lbool r = m_aux_context->check();
|
||||
TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
|
||||
if (r != l_true)
|
||||
|
|
@ -308,7 +345,6 @@ namespace smt {
|
|||
add_instance(q, complete_cex.get(), sks, false);
|
||||
}
|
||||
|
||||
m_aux_context->pop(1);
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
@ -318,33 +354,29 @@ namespace smt {
|
|||
expr* fn = to_app(q->get_pattern(0))->get_arg(0);
|
||||
SASSERT(is_app(fn));
|
||||
func_decl* f = to_app(fn)->get_decl();
|
||||
enode_vector::const_iterator it = m_context->begin_enodes_of(f);
|
||||
enode_vector::const_iterator end = m_context->end_enodes_of(f);
|
||||
|
||||
bool is_undef = false;
|
||||
expr_ref_vector args(m);
|
||||
unsigned num_decls = q->get_num_decls();
|
||||
args.resize(num_decls, nullptr);
|
||||
var_subst sub(m);
|
||||
expr_ref tmp(m), result(m);
|
||||
for (; it != end; ++it) {
|
||||
if (m_context->is_relevant(*it)) {
|
||||
app* e = (*it)->get_owner();
|
||||
for (enode* n : m_context->enodes_of(f)) {
|
||||
if (m_context->is_relevant(n)) {
|
||||
app* e = n->get_owner();
|
||||
SASSERT(e->get_num_args() == num_decls);
|
||||
for (unsigned i = 0; i < num_decls; ++i) {
|
||||
args[i] = e->get_arg(i);
|
||||
}
|
||||
sub(q->get_expr(), num_decls, args.c_ptr(), tmp);
|
||||
tmp = sub(q->get_expr(), num_decls, args.c_ptr());
|
||||
m_curr_model->eval(tmp, result, true);
|
||||
if (strict_rec_fun ? !m.is_true(result) : m.is_false(result)) {
|
||||
add_instance(q, args, 0);
|
||||
add_instance(q, args, 0, nullptr);
|
||||
return false;
|
||||
}
|
||||
TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";);
|
||||
// if (!m.is_true(result)) is_undef = true;
|
||||
TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";);
|
||||
}
|
||||
}
|
||||
return !is_undef;
|
||||
return true;
|
||||
}
|
||||
|
||||
void model_checker::init_aux_context() {
|
||||
|
|
@ -360,7 +392,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool model_checker::check(proto_model * md, obj_map<enode, app *> const & root2value) {
|
||||
SASSERT(md != 0);
|
||||
SASSERT(md != nullptr);
|
||||
|
||||
m_root2value = &root2value;
|
||||
|
||||
|
|
@ -391,7 +423,6 @@ namespace smt {
|
|||
|
||||
check_quantifiers(false, found_relevant, num_failures);
|
||||
|
||||
|
||||
if (found_relevant)
|
||||
m_iteration_idx++;
|
||||
|
||||
|
|
@ -416,35 +447,47 @@ namespace smt {
|
|||
return num_failures == 0;
|
||||
}
|
||||
|
||||
//
|
||||
// (repeated from defined_names.cpp)
|
||||
// NB. The pattern for lambdas is incomplete.
|
||||
// consider store(a, i, v) == \lambda j . if i = j then v else a[j]
|
||||
// the instantiation rules for store(a, i, v) are:
|
||||
// sotre(a, i, v)[j] = if i = j then v else a[j] with patterns {a[j], store(a, i, v)} { store(a, i, v)[j] }
|
||||
// The first pattern is not included.
|
||||
// TBD use a model-based scheme for exracting instantiations instead of
|
||||
// using multi-patterns.
|
||||
//
|
||||
|
||||
void model_checker::check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures) {
|
||||
ptr_vector<quantifier>::const_iterator it = m_qm->begin_quantifiers();
|
||||
ptr_vector<quantifier>::const_iterator end = m_qm->end_quantifiers();
|
||||
for (; it != end; ++it) {
|
||||
quantifier * q = *it;
|
||||
if(!m_qm->mbqi_enabled(q)) continue;
|
||||
for (quantifier * q : *m_qm) {
|
||||
if (!(m_qm->mbqi_enabled(q) &&
|
||||
m_context->is_relevant(q) &&
|
||||
m_context->get_assignment(q) == l_true &&
|
||||
!m.is_lambda_def(q))) {
|
||||
continue;
|
||||
}
|
||||
|
||||
TRACE("model_checker",
|
||||
tout << "Check: " << mk_pp(q, m) << "\n";
|
||||
tout << m_context->get_assignment(q) << "\n";);
|
||||
|
||||
if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) {
|
||||
if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
|
||||
verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
|
||||
}
|
||||
found_relevant = true;
|
||||
if (m.is_rec_fun_def(q)) {
|
||||
if (!check_rec_fun(q, strict_rec_fun)) {
|
||||
TRACE("model_checker", tout << "checking recursive function failed\n";);
|
||||
num_failures++;
|
||||
}
|
||||
}
|
||||
else if (!check(q)) {
|
||||
if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
|
||||
IF_VERBOSE(0, verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n");
|
||||
}
|
||||
TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";);
|
||||
if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
|
||||
verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
|
||||
}
|
||||
found_relevant = true;
|
||||
if (m.is_rec_fun_def(q)) {
|
||||
if (!check_rec_fun(q, strict_rec_fun)) {
|
||||
TRACE("model_checker", tout << "checking recursive function failed\n";);
|
||||
num_failures++;
|
||||
}
|
||||
}
|
||||
else if (!check(q)) {
|
||||
if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
|
||||
IF_VERBOSE(0, verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n");
|
||||
}
|
||||
TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";);
|
||||
num_failures++;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -467,7 +510,6 @@ namespace smt {
|
|||
void model_checker::reset_new_instances() {
|
||||
m_pinned_exprs.reset();
|
||||
m_new_instances.reset();
|
||||
m_new_instances_region.reset();
|
||||
}
|
||||
|
||||
void model_checker::reset() {
|
||||
|
|
@ -478,32 +520,30 @@ namespace smt {
|
|||
TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";);
|
||||
ptr_buffer<enode> bindings;
|
||||
vector<std::tuple<enode *, enode *>> dummy;
|
||||
for (instance* inst : m_new_instances) {
|
||||
quantifier * q = inst->m_q;
|
||||
for (instance const& inst : m_new_instances) {
|
||||
quantifier * q = inst.m_q;
|
||||
if (m_context->b_internalized(q)) {
|
||||
bindings.reset();
|
||||
unsigned num_decls = q->get_num_decls();
|
||||
unsigned gen = inst->m_generation;
|
||||
unsigned gen = inst.m_generation;
|
||||
unsigned offset = inst.m_bindings_offset;
|
||||
for (unsigned i = 0; i < num_decls; i++) {
|
||||
expr * b = inst->m_bindings[i];
|
||||
expr * b = m_pinned_exprs.get(offset + i);
|
||||
if (!m_context->e_internalized(b)) {
|
||||
TRACE("model_checker_bug_detail", tout << "internalizing b:\n" << mk_pp(b, m) << "\n";);
|
||||
TRACE("model_checker", tout << "internalizing b:\n" << mk_pp(b, m) << "\n";);
|
||||
m_context->internalize(b, false, gen);
|
||||
}
|
||||
bindings.push_back(m_context->get_enode(b));
|
||||
}
|
||||
|
||||
if (inst.m_def) {
|
||||
m_context->internalize_assertion(inst.m_def, 0, gen);
|
||||
}
|
||||
|
||||
TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m) << "\n";
|
||||
tout << "inconsistent: " << m_context->inconsistent() << "\n";
|
||||
tout << "bindings:\n";
|
||||
for (unsigned i = 0; i < num_decls; i++) {
|
||||
expr * b = inst->m_bindings[i];
|
||||
tout << mk_pp(b, m) << "\n";
|
||||
});
|
||||
TRACE("model_checker_instance",
|
||||
expr_ref inst_expr(m);
|
||||
instantiate(m, q, inst->m_bindings, inst_expr);
|
||||
tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";);
|
||||
m_context->add_instance(q, nullptr, num_decls, bindings.c_ptr(), gen, gen, gen, dummy);
|
||||
tout << "bindings:\n" << expr_ref_vector(m, num_decls, m_pinned_exprs.c_ptr() + offset) << "\n";);
|
||||
m_context->add_instance(q, nullptr, num_decls, bindings.c_ptr(), inst.m_def, gen, gen, gen, dummy);
|
||||
TRACE("model_checker_bug_detail", tout << "after instantiating, inconsistent: " << m_context->inconsistent() << "\n";);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue