mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

simplify with caching, but without expanding number of asserted formulas. Bug reported by Heizmann, codeplex issue 197

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-04-02 10:28:30 -07:00
parent 70d765df5c
commit d01c3491a6
1 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/asserted_formulas.cpp
View file

@ -603,11 +603,11 @@ void asserted_formulas::propagate_values() {
proof_ref_vector new_prs1(m_manager); proof_ref_vector new_prs1(m_manager);
expr_ref_vector new_exprs2(m_manager); expr_ref_vector new_exprs2(m_manager);
proof_ref_vector new_prs2(m_manager); proof_ref_vector new_prs2(m_manager);
unsigned i = 0;
unsigned sz = m_asserted_formulas.size(); unsigned sz = m_asserted_formulas.size();
for (; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
expr * n = m_asserted_formulas.get(i); expr * n = m_asserted_formulas.get(i);
proof * pr = m_asserted_formula_prs.get(i, 0); proof * pr = m_asserted_formula_prs.get(i, 0);
TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";);
if (m_manager.is_eq(n)) { if (m_manager.is_eq(n)) {
expr * lhs = to_app(n)->get_arg(0); expr * lhs = to_app(n)->get_arg(0);
expr * rhs = to_app(n)->get_arg(1); expr * rhs = to_app(n)->get_arg(1);
@ -615,9 +615,11 @@ void asserted_formulas::propagate_values() {
if (m_manager.is_value(lhs)) if (m_manager.is_value(lhs))
std::swap(lhs, rhs); std::swap(lhs, rhs);
if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) { if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
if (i >= m_asserted_qhead) {
new_exprs1.push_back(n); new_exprs1.push_back(n);
if (m_manager.proofs_enabled()) if (m_manager.proofs_enabled())
new_prs1.push_back(pr); new_prs1.push_back(pr);
}
TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";); TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";);
m_simplifier.cache_result(lhs, rhs, pr); m_simplifier.cache_result(lhs, rhs, pr);
found = true; found = true;
@ -625,10 +627,12 @@ void asserted_formulas::propagate_values() {
} }
} }
} }
if (i >= m_asserted_qhead) {
new_exprs2.push_back(n); new_exprs2.push_back(n);
if (m_manager.proofs_enabled()) if (m_manager.proofs_enabled())
new_prs2.push_back(pr); new_prs2.push_back(pr);
} }
}
TRACE("propagate_values", tout << "found: " << found << "\n";); TRACE("propagate_values", tout << "found: " << found << "\n";);
// If C is not empty, then reduce R using the updated simplifier cache with entries // If C is not empty, then reduce R using the updated simplifier cache with entries
// x -> n for each constraint 'x = n' in C. // x -> n for each constraint 'x = n' in C.