mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-11 23:51:40 -08:00
parent fc3a642876
commit d1dab327cd
3 changed files with 119 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

192
src/sat/smt/q_mbi.cpp
View file

@ -75,32 +75,32 @@ namespace q {
return result;
}
/**
*
*/
void mbqi::restrict_to_universe(expr* sk, ptr_vector<expr> const& universe) {
SASSERT(!universe.empty());
expr_ref_vector eqs(m);
euf::enode* n = nullptr;
unsigned generation_min = UINT_MAX;
for (expr* e : universe) {
euf::enode* n = nullptr;
if (ctx.values2root().find(e, n)) {
unsigned g = n->class_generation();
generation_min = std::min(generation_min, g);
m_generation_max = std::max(m_generation_max, g);
if (g > m_generation_bound) {
std::cout << "SKIP\n";
continue;
}
#if 1
if (g < generation_min) {
std::cout << "RESET\n";
eqs.reset();
}
#endif
m_generation_max = std::max(m_generation_max, g);
generation_min = std::min(generation_min, g);
eqs.push_back(m.mk_eq(sk, e));
std::cout << mk_pp(e, m) << ": " << ctx.bpp(n) << " gen: " << n->generation() << " " << n->class_generation() << " class-size: " << n->get_root()->class_size() << "\n";
}
else
eqs.push_back(m.mk_eq(sk, e));
eqs.push_back(m.mk_eq(sk, e));
}
if (eqs.empty()) {
for (expr* e : universe)
if (ctx.values2root().find(e, n) && n->class_generation() <= generation_min)
eqs.push_back(m.mk_eq(sk, e));
}
m_solver->assert_expr(mk_or(eqs));
}
@ -134,12 +134,16 @@ namespace q {
if (count > m_max_choose_candidates)
break;
}
std::cout << "choose " << r->class_size() << " " << expr_ref(r->get_expr(), m) << "\n";
return expr_ref(r->get_expr(), m);
}
lbool mbqi::check_forall(quantifier* q) {
quantifier* q_flat = m_qs.flatten(q);
init_solver();
m_generation_bound = 1;
m_generation_max = 0;
::solver::scoped_push _sp(*m_solver);
std::cout << mk_pp(q, m, 4) << "\n";
auto* qb = specialize(q_flat);
@ -147,6 +151,12 @@ namespace q {
return l_undef;
if (m.is_false(qb->mbody))
return l_true;
if (!qb->free_vars.empty())
quick_check(q, *qb);
add_universe_restriction(q, *qb);
std::cout << "gen-max: " << m_generation_max << "\n";
#if 0
if (quick_check(q, *qb)) {
@ -159,38 +169,48 @@ namespace q {
return r;
if (r == l_false)
return l_true;
model_ref mdl0, mdl1;
model_ref mdl;
expr_ref proj(m);
m_solver->get_model(mdl0);
unsigned i = 0;
m_solver->get_model(mdl);
if (check_forall_subst(q, *qb, *mdl))
return l_false;
else
return check_forall_default(q, *qb, *mdl);
}
lbool mbqi::check_forall_default(quantifier* q, q_body& qb, model& mdl) {
expr_ref_vector eqs(m);
if (!qb->var_args.empty()) {
::solver::scoped_push _sp(*m_solver);
add_domain_eqs(*mdl0, *qb);
for (; i < m_max_cex && l_true == m_solver->check_sat(0, nullptr); ++i) {
m_solver->get_model(mdl1);
proj = solver_project(*mdl1, *qb, eqs, true);
if (!proj)
break;
std::cout << "project\n" << proj << "\n";
std::cout << "eqs: " << eqs << "\n";
add_instantiation(q, proj);
m_solver->assert_expr(m.mk_not(mk_and(eqs)));
std::cout << "solve again " << i << "\n";
}
}
if (i == 0) {
add_domain_bounds(*mdl0, *qb);
proj = solver_project(*mdl0, *qb, eqs, false);
if (!proj)
return l_undef;
std::cout << "project-base\n" << proj << "\n";
add_instantiation(q, proj);
}
// TODO: add as top-level clause for relevancy
add_domain_bounds(mdl, qb);
auto proj = solver_project(mdl, qb, eqs, false);
if (!proj)
return l_undef;
std::cout << "project-base\n" << proj << "\n";
add_instantiation(q, proj);
return l_false;
}
bool mbqi::check_forall_subst(quantifier* q, q_body& qb, model& mdl0) {
if (qb.var_args.empty())
return false;
model_ref mdl1;
expr_ref_vector eqs(m);
unsigned i = 0;
::solver::scoped_push _sp(*m_solver);
add_domain_eqs(mdl0, qb);
for (; i < m_max_cex && l_true == m_solver->check_sat(0, nullptr); ++i) {
m_solver->get_model(mdl1);
auto proj = solver_project(*mdl1, qb, eqs, true);
if (!proj)
break;
std::cout << "project\n" << proj << "\n";
std::cout << "eqs: " << eqs << "\n";
add_instantiation(q, proj);
m_solver->assert_expr(m.mk_not(mk_and(eqs)));
std::cout << "solve again " << i << "\n";
}
return i > 0;
}
void mbqi::add_instantiation(quantifier* q, expr_ref& proj) {
sat::literal qlit = ctx.expr2literal(q);
if (is_exists(q))
@ -201,6 +221,15 @@ namespace q {
m_instantiations.push_back(instantiation_t(qlit, proj, generation));
}
void mbqi::add_universe_restriction(quantifier* q, q_body& qb) {
unsigned sz = q->get_num_decls();
for (unsigned i = 0; i < sz; ++i) {
sort* s = q->get_decl_sort(i);
if (m_model->has_uninterpreted_sort(s))
restrict_to_universe(qb.vars.get(i), m_model->get_universe(s));
}
}
mbqi::q_body* mbqi::specialize(quantifier* q) {
var_subst subst(m);
q_body* result = q2body(q);
@ -208,12 +237,6 @@ namespace q {
if (!m_model->eval_expr(q->get_expr(), mbody, true))
return nullptr;
unsigned sz = q->get_num_decls();
for (unsigned i = 0; i < sz; ++i) {
sort* s = q->get_decl_sort(i);
if (m_model->has_uninterpreted_sort(s))
restrict_to_universe(result->vars.get(i), m_model->get_universe(s));
}
mbody = subst(mbody, result->vars);
if (is_forall(q))
@ -452,7 +475,8 @@ namespace q {
}
bool mbqi::quick_check(quantifier* q, q_body& qb) {
unsigned max_rounds = 10;
std::cout << "QUICK-CHECK\n";
unsigned max_rounds = 100;
unsigned_vector offsets;
if (!first_offset(offsets, qb.vars))
return false;
@ -460,70 +484,78 @@ namespace q {
unsigned bindings = 0;
expr_ref_vector binding(m);
for (unsigned i = 0; i < max_rounds && bindings < m_max_cex; ++i) {
if (!next_binding(offsets, qb.vars, binding))
break;
set_binding(offsets, qb.vars, binding);
std::cout << "binding " << binding << "\n";
if (m_model->is_true(qb.vbody)) {
expr_ref body(q->get_expr(), m);
body = subst(q->get_expr(), binding);
if (is_forall(q))
body = ::mk_not(m, body);
sat::literal qlit = ctx.expr2literal(q);
std::cout << "instantiate " << mk_pp(q, m) << "\n";
std::cout << "binding:\n" << binding << "\n";
std::cout << "body:\n" << body << "\n";
add_instantiation(q, body);
++bindings;
}
if (!next_offset(offsets, qb.vars))
break;
}
return bindings > 0;
}
bool mbqi::first_offset(unsigned_vector& offsets, app_ref_vector const& vars) {
offsets.reset();
unsigned index = 0;
bool mbqi::next_offset(unsigned_vector& offsets, app_ref_vector const& vars, unsigned index, unsigned start) {
auto* v = vars[index];
sort* srt = m.get_sort(v);
auto const& nodes = ctx.get_egraph().nodes();
unsigned sz = nodes.size();
for (unsigned i = start; i < sz; ++i) {
expr* e = nodes[i]->get_expr();
if (m.get_sort(e) == srt && !m.is_value(e)) {
offsets[index] = i;
return true;
}
}
return false;
}
bool mbqi::first_offset(unsigned_vector& offsets, app_ref_vector const& vars) {
offsets.reset();
for (app* v : vars)
offsets.push_back(0);
for (auto* v : vars) {
sort* srt = m.get_sort(v);
bool found = false;
unsigned i = offsets[index];
for (; i < sz; ++i) {
expr* e = nodes[i]->get_expr();
if (m.get_sort(e) == srt && !m.is_value(e)) {
offsets[index] = i;
break;
}
}
++index;
if (i == sz)
for (unsigned i = 0; i < vars.size(); ++i)
if (!next_offset(offsets, vars, i, 0))
return false;
}
return true;
}
bool mbqi::next_binding(unsigned_vector& offsets, app_ref_vector const& vars, expr_ref_vector& binding) {
auto const& nodes = ctx.get_egraph().nodes();
unsigned index = m_qs.random() % offsets.size();
unsigned i = offsets[index] + 1;
sort* srt = m.get_sort(vars[index]);
unsigned sz = nodes.size();
while (i < sz && m.get_sort(nodes[i]->get_expr()) != srt)
++i;
if (i == sz)
return false;
if (nodes[i]->generation() > 0)
return false;
void mbqi::set_binding(unsigned_vector const& offsets, app_ref_vector const& vars, expr_ref_vector& binding) {
binding.reset();
auto const& nodes = ctx.get_egraph().nodes();
m_model->reset_eval_cache();
for (unsigned j = 0; j < offsets.size(); ++j) {
unsigned offset = offsets[j];
binding.push_back(nodes[offset]->get_expr());
m_model->register_decl(vars[j]->get_decl(), (*m_model)(binding.get(j)));
}
offsets[index] = i;
}
bool mbqi::next_offset(unsigned_vector& offsets, app_ref_vector const& vars) {
for (unsigned i = 0; i < vars.size(); ++i) {
if (next_offset(offsets, vars, i, offsets[i] + 1))
return true;
if (!next_offset(offsets, vars, i, 0))
return false;
}
return false;
#if 0
auto const& nodes = ctx.get_egraph().nodes();
unsigned index = m_qs.random() % offsets.size();
if (!next_offset(offsets, vars, index, offsets[index] + 1))
return false;
if (nodes[offsets[index]]->generation() > 1)
return false;
return true;
#endif
}
void mbqi::init_model() {

8
src/sat/smt/q_mbi.h
View file

@ -78,6 +78,7 @@ namespace q {
q_body* specialize(quantifier* q);
q_body* q2body(quantifier* q);
expr_ref solver_project(model& mdl, q_body& qb, expr_ref_vector& eqs, bool use_inst);
void add_universe_restriction(quantifier* q, q_body& qb);
void add_domain_eqs(model& mdl, q_body& qb);
void add_domain_bounds(model& mdl, q_body& qb);
void eliminate_nested_vars(expr_ref_vector& fmls, q_body& qb);
@ -89,9 +90,14 @@ namespace q {
void add_plugin(mbp::project_plugin* p);
void add_instantiation(quantifier* q, expr_ref& proj);
lbool check_forall_default(quantifier* q, q_body& qb, model& mdl);
bool check_forall_subst(quantifier* q, q_body& qb, model& mdl);
bool quick_check(quantifier* q, q_body& qb);
bool next_binding(unsigned_vector& offsets, app_ref_vector const& vars, expr_ref_vector& binding);
bool next_offset(unsigned_vector& offsets, app_ref_vector const& vars);
bool first_offset(unsigned_vector& offsets, app_ref_vector const& vars);
bool next_offset(unsigned_vector& offsets, app_ref_vector const& vars, unsigned i, unsigned start);
void set_binding(unsigned_vector const& offsets, app_ref_vector const& vars, expr_ref_vector& binding);
public:

1
src/smt/theory_lra.cpp
View file

@ -3487,7 +3487,6 @@ public:
return inf_eps(rational::zero(), val);
}
default:
std::cout << st << "\n";
SASSERT(st == lp::lp_status::UNBOUNDED);
TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
has_shared = false;