mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

quantifiers and a heuristic for disequalities

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-27 15:34:02 -08:00
parent e2198f6541
commit 1d9b090196
2 changed files with 37 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

61
src/muz_qe/pdr_quantifiers.cpp
View file

@ -106,11 +106,19 @@ namespace pdr {
} }
void quantifier_model_checker::apply_binding(quantifier* q, expr_ref_vector& binding) { void quantifier_model_checker::apply_binding(quantifier* q, expr_ref_vector& binding) {
datalog::scoped_no_proof _scp(m); datalog::scoped_no_proof _scp(m);
app_ref_vector& var_inst = m_current_pt->get_inst(m_current_rule); app_ref_vector& var_inst = m_current_pt->get_inst(m_current_rule);
expr_ref e(m);
var_subst vs(m, false);
inv_var_shifter invsh(m);
vs(q->get_expr(), binding.size(), binding.c_ptr(), e);
invsh(e, q->get_num_decls(), e);
expr_ref_vector inst(m);
inst.append(var_inst.size(), (expr*const*)var_inst.c_ptr());
inst.reverse();
expr_abstract(m, 0, inst.size(), inst.c_ptr(), e, e);
m_instantiated_rules.push_back(m_current_rule);
m_instantiations.push_back(to_app(e));
TRACE("pdr", tout << mk_pp(q, m) << "\n"; TRACE("pdr", tout << mk_pp(q, m) << "\n";
tout << "binding\n"; tout << "binding\n";
for (unsigned i = 0; i < binding.size(); ++i) { for (unsigned i = 0; i < binding.size(); ++i) {
@ -122,21 +130,8 @@ namespace pdr {
tout << mk_pp(var_inst[i].get(), m) << " "; tout << mk_pp(var_inst[i].get(), m) << " ";
} }
tout << "\n"; tout << "\n";
tout << mk_pp(e, m) << "\n";
); );
expr_ref e(m);
var_subst vs(m, false);
inv_var_shifter invsh(m);
vs(q->get_expr(), binding.size(), binding.c_ptr(), e);
invsh(e, q->get_num_decls(), e);
expr_ref_vector inst(m);
inst.append(var_inst.size(), (expr*const*)var_inst.c_ptr());
inst.reverse();
expr_abstract(m, 0, inst.size(), inst.c_ptr(), e, e);
TRACE("pdr", tout << mk_pp(e, m) << "\n";);
m_instantiated_rules.push_back(m_current_rule);
m_instantiations.push_back(to_app(e));
} }
@ -206,7 +201,6 @@ namespace pdr {
front_end_params fparams; front_end_params fparams;
fparams.m_proof_mode = PGM_COARSE; fparams.m_proof_mode = PGM_COARSE;
fparams.m_mbqi = true; fparams.m_mbqi = true;
// TBD: does not work on integers: fparams.m_mbqi = true;
fmls.push_back(m_A.get()); fmls.push_back(m_A.get());
fmls.append(m_Bs); fmls.append(m_Bs);
@ -259,18 +253,6 @@ namespace pdr {
add_binding(q, new_binding); add_binding(q, new_binding);
found_instance = true; found_instance = true;
} }
if (collector.size() == 0) {
// Try to create dummy instances.
for (unsigned i = 0; i < m_Bs.size(); ++i) {
q = qs[i];
expr_ref_vector binding(m);
for (unsigned j = 0; j < q->get_num_decls(); ++j) {
binding.push_back(m.mk_fresh_const("B", q->get_decl_sort(j)));
}
add_binding(q, binding);
}
found_instance = true;
}
return found_instance; return found_instance;
} }
@ -300,7 +282,7 @@ namespace pdr {
pred_transformer& pt = node.pt(); pred_transformer& pt = node.pt();
manager& pm = pt.get_pdr_manager(); manager& pm = pt.get_pdr_manager();
expr_ref A(m), B(m), C(m), v(m); expr_ref A(m), B(m), C(m), v(m);
expr_ref_vector As(m); expr_ref_vector As(m), Bs(m);
m_Bs.reset(); m_Bs.reset();
// //
// nodes from leaves that are repeated // nodes from leaves that are repeated
@ -342,7 +324,6 @@ namespace pdr {
for (unsigned j = 0; j < qis->size(); ++j) { for (unsigned j = 0; j < qis->size(); ++j) {
q = (*qis)[j].get(); q = (*qis)[j].get();
app_ref_vector& inst = pt.get_inst(m_current_rule); app_ref_vector& inst = pt.get_inst(m_current_rule);
ptr_vector<app>& aux_vars = pt.get_aux_vars(*m_current_rule);
TRACE("pdr", TRACE("pdr",
tout << "q:\n" << mk_pp(q, m) << "\n"; tout << "q:\n" << mk_pp(q, m) << "\n";
tout << "level: " << level << "\n"; tout << "level: " << level << "\n";
@ -359,7 +340,7 @@ namespace pdr {
app* a = to_app(q->get_expr()); app* a = to_app(q->get_expr());
func_decl* f = a->get_decl(); func_decl* f = a->get_decl();
pred_transformer& pt2 = m_ctx.get_pred_transformer(f); pred_transformer& pt2 = m_ctx.get_pred_transformer(f);
B = pt2.get_formulas(previous_level, true); B = pt2.get_formulas(previous_level, false);
TRACE("pdr", tout << "B:\n" << mk_pp(B, m) << "\n";); TRACE("pdr", tout << "B:\n" << mk_pp(B, m) << "\n";);
@ -371,17 +352,23 @@ namespace pdr {
rep->set_substitution(&sub); rep->set_substitution(&sub);
(*rep)(B); (*rep)(B);
TRACE("pdr", tout << "B substituted:\n" << mk_pp(B, m) << "\n";); TRACE("pdr", tout << "B substituted:\n" << mk_pp(B, m) << "\n";);
datalog::flatten_and(B, Bs);
B = m.update_quantifier(q, B); for (unsigned i = 0; i < Bs.size(); ++i) {
m_Bs.push_back(B); m_Bs.push_back(m.update_quantifier(q, Bs[i].get()));
}
} }
} }
TRACE("pdr", TRACE("pdr",
tout << "A:\n" << mk_pp(m_A, m) << "\n"; tout << "A:\n" << mk_pp(m_A, m) << "\n";
tout << "quantifier:\n";
for (unsigned i = 0; i < qis->size(); ++i) {
tout << mk_pp((*qis)[i].get(), m) << " ";
}
tout << "\n";
tout << "B:\n"; tout << "B:\n";
for (unsigned i = 0; i < m_Bs.size(); ++i) { for (unsigned i = 0; i < m_Bs.size(); ++i) {
tout << mk_pp((*qis)[i].get(), m) << "\n" << mk_pp(m_Bs[i].get(), m) << "\n"; tout << mk_pp(m_Bs[i].get(), m) << "\n";
} }
ast_smt_pp pp(m); ast_smt_pp pp(m);
pp.add_assumption(m_A); pp.add_assumption(m_A);

16
src/muz_qe/pdr_util.cpp
View file

@ -219,11 +219,21 @@ namespace pdr {
collect(formulas, tocollect); collect(formulas, tocollect);
for (unsigned i = 0; i < tocollect.size(); ++i) { for (unsigned i = 0; i < tocollect.size(); ++i) {
expr* e = tocollect[i]; expr* e = tocollect[i];
expr* e1, *e2;
SASSERT(m.is_bool(e)); SASSERT(m.is_bool(e));
SASSERT(is_true(e) || is_false(e)); SASSERT(is_true(e) || is_false(e));
if (is_true(e)) { if (is_true(e)) {
result.push_back(e); result.push_back(e);
} }
// hack to break disequalities for arithmetic variables.
else if (m.is_eq(e, e1, e2) && m_arith.is_int_real(e1)) {
if (get_number(e1) < get_number(e2)) {
result.push_back(m_arith.mk_lt(e1,e2));
}
else {
result.push_back(m_arith.mk_lt(e2,e1));
}
}
else { else {
result.push_back(m.mk_not(e)); result.push_back(m.mk_not(e));
} }
@ -260,11 +270,11 @@ namespace pdr {
SASSERT(v); SASSERT(v);
// no-op // no-op
} }
else if (!m.is_bool(args[0])) { else if (m.is_bool(args[0])) {
tocollect.push_back(e); todo.append(sz, args);
} }
else { else {
todo.append(sz, args); tocollect.push_back(e);
} }
break; break;
case OP_DISTINCT: case OP_DISTINCT: