mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

#6340 again - reduce new assertions in fresh iteration

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-09-13 19:58:32 -07:00
parent a6a5985f8e
commit 34969b71ee
1 changed files with 25 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/smt/smt_context.cpp
View file

@ -3202,26 +3202,34 @@ namespace smt {
flet<bool> _internalizing(m_internalizing_assertions, true);
TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
reduce_assertions();
if (get_cancel_flag()) return;
if (!m_asserted_formulas.inconsistent()) {
unsigned qhead = m_asserted_formulas.get_qhead();
while (qhead < m_asserted_formulas.get_num_formulas()) {
if (get_cancel_flag()) {
m_asserted_formulas.commit(qhead);
return;
unsigned qhead = 0;
do {
reduce_assertions();
if (get_cancel_flag())
return;
qhead = m_asserted_formulas.get_qhead();
if (!m_asserted_formulas.inconsistent()) {
unsigned sz = m_asserted_formulas.get_num_formulas();
while (qhead < sz) {
if (get_cancel_flag()) {
m_asserted_formulas.commit(qhead);
return;
}
expr * f = m_asserted_formulas.get_formula(qhead);
proof * pr = m_asserted_formulas.get_formula_proof(qhead);
SASSERT(!pr || f == m.get_fact(pr));
internalize_assertion(f, pr, 0);
qhead++;
}
expr * f = m_asserted_formulas.get_formula(qhead);
proof * pr = m_asserted_formulas.get_formula_proof(qhead);
SASSERT(!pr || f == m.get_fact(pr));
internalize_assertion(f, pr, 0);
qhead++;
m_asserted_formulas.commit();
}
if (m_asserted_formulas.inconsistent() && !inconsistent()) {
asserted_inconsistent();
break;
}
m_asserted_formulas.commit();
}
if (m_asserted_formulas.inconsistent() && !inconsistent()) {
asserted_inconsistent();
}
while (qhead < m_asserted_formulas.get_num_formulas());
TRACE("internalize_assertions", tout << "after internalize_assertions()...\n";
tout << "inconsistent: " << inconsistent() << "\n";);
TRACE("after_internalize_assertions", display(tout););