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

refactor closure code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-01 13:50:18 -07:00
parent 929d9f430b
commit fcc351eba6
2 changed files with 10 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz/pdr/pdr_closure.cpp
View file

@ -135,8 +135,8 @@ namespace pdr {
result = e; result = e;
} }
else { else {
result = e;
IF_VERBOSE(1, verbose_stream() << "Cannot close: " << mk_pp(e, m) << "\n";); IF_VERBOSE(1, verbose_stream() << "Cannot close: " << mk_pp(e, m) << "\n";);
result = m.mk_true();
} }
return result; return result;
} }
@ -145,9 +145,9 @@ namespace pdr {
expr_ref_vector fmls(m); expr_ref_vector fmls(m);
qe::flatten_and(fml, fmls); qe::flatten_and(fml, fmls);
for (unsigned i = 0; i < fmls.size(); ++i) { for (unsigned i = 0; i < fmls.size(); ++i) {
fmls[i] = close_fml(fmls[i].get()); fmls[i] = close_fml(fmls[i].get());
} }
return expr_ref(m.mk_and(fmls.size(), fmls.c_ptr()), m); return qe::mk_and(fmls);
} }
expr_ref closure::relax(unsigned i, expr* fml) { expr_ref closure::relax(unsigned i, expr* fml) {

15
src/muz/pdr/pdr_generalizers.cpp
View file

@ -116,11 +116,10 @@ namespace pdr {
void core_farkas_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { void core_farkas_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
ast_manager& m = n.pt().get_manager(); ast_manager& m = n.pt().get_manager();
manager& pm = n.pt().get_pdr_manager();
if (core.empty()) return; if (core.empty()) return;
expr_ref A(m), B(pm.mk_and(core)), C(m); expr_ref A(m), B(qe::mk_and(core)), C(m);
expr_ref_vector Bs(m); expr_ref_vector Bs(m);
pm.get_or(B, Bs); qe::flatten_or(B, Bs);
A = n.pt().get_propagation_formula(m_ctx.get_pred_transformers(), n.level()); A = n.pt().get_propagation_formula(m_ctx.get_pred_transformers(), n.level());
bool change = false; bool change = false;
@ -130,13 +129,13 @@ namespace pdr {
if (m_farkas_learner.get_lemma_guesses(A, B, lemmas)) { if (m_farkas_learner.get_lemma_guesses(A, B, lemmas)) {
TRACE("pdr", TRACE("pdr",
tout << "Old core:\n" << mk_pp(B, m) << "\n"; tout << "Old core:\n" << mk_pp(B, m) << "\n";
tout << "New core:\n" << mk_pp(pm.mk_and(lemmas), m) << "\n";); tout << "New core:\n" << mk_pp(qe::mk_and(lemmas), m) << "\n";);
Bs[i] = pm.mk_and(lemmas); Bs[i] = qe::mk_and(lemmas);
change = true; change = true;
} }
} }
if (change) { if (change) {
C = pm.mk_or(Bs); C = qe::mk_or(Bs);
TRACE("pdr", tout << "prop:\n" << mk_pp(A,m) << "\ngen:" << mk_pp(B, m) << "\nto: " << mk_pp(C, m) << "\n";); TRACE("pdr", tout << "prop:\n" << mk_pp(A,m) << "\ngen:" << mk_pp(B, m) << "\nto: " << mk_pp(C, m) << "\n";);
core.reset(); core.reset();
qe::flatten_and(C, core); qe::flatten_and(C, core);
@ -688,7 +687,7 @@ namespace pdr {
for (unsigned i = 0; i < rules.size(); ++i) { for (unsigned i = 0; i < rules.size(); ++i) {
fmls.push_back(m.mk_not(mk_transition_rule(reps, level, *rules[i]))); fmls.push_back(m.mk_not(mk_transition_rule(reps, level, *rules[i])));
} }
fml = pm.mk_and(fmls); fml = qe::mk_and(fmls);
TRACE("pdr", tout << mk_pp(fml, m) << "\n";); TRACE("pdr", tout << mk_pp(fml, m) << "\n";);
return fml; return fml;
} }
@ -744,7 +743,7 @@ namespace pdr {
} }
} }
expr_ref result = pm.mk_and(conjs); expr_ref result = qe::mk_and(conjs);
TRACE("pdr", tout << mk_pp(result, m) << "\n";); TRACE("pdr", tout << mk_pp(result, m) << "\n";);
return result; return result;
} }