mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Fix for #343. Optimizations introduced on 8-10-2015 were too agressive

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-01 13:41:57 -08:00
parent f68c1d755f
commit 9fa4bf2f8f
1 changed files with 31 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/tactic/arith/lia2card_tactic.cpp
View file

@ -189,6 +189,8 @@ public:
TRACE("pb", tout << "add bound " << mk_pp(x, m) << "\n";);
}
}
expr_ref_vector fmls(m);
expr_mark subfmls;
for (unsigned i = 0; i < g->size(); i++) {
expr_ref new_curr(m);
proof_ref new_pr(m);
@ -198,6 +200,15 @@ public:
new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
}
g->update(i, new_curr, new_pr, g->dep(i));
mark_rec(subfmls, new_curr);
}
expr_set::iterator it = m_01s->begin(), end = m_01s->end();
for (; it != end; ++it) {
expr* v = *it;
if (subfmls.is_marked(v)) {
g->assert_expr(a.mk_le(v, a.mk_numeral(rational(1), true)));
g->assert_expr(a.mk_le(a.mk_numeral(rational(0), true), v));
}
}
g->inc_depth();
result.push_back(g.get());
@ -207,6 +218,26 @@ public:
// TBD: convert models for 0-1 variables.
// TBD: support proof conversion (or not..)
}
void mark_rec(expr_mark& mark, expr* e) {
ptr_vector<expr> todo;
todo.push_back(e);
while (!todo.empty()) {
e = todo.back();
todo.pop_back();
if (!mark.is_marked(e)) {
mark.mark(e);
if (is_app(e)) {
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
todo.push_back(to_app(e)->get_arg(i));
}
}
else if (is_quantifier(e)) {
todo.push_back(to_quantifier(e)->get_expr());
}
}
}
}
bool is_01var(expr* x) const {