mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

logging pre-processing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-09-03 15:19:28 -07:00
parent ff3268e636
commit c2e73a6aae
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/solver/simplifier_solver.cpp
View file

@ -110,12 +110,13 @@ class simplifier_solver : public solver {
expr_ref_vector orig_assumptions(assumptions); expr_ref_vector orig_assumptions(assumptions);
m_core_replace.reset(); m_core_replace.reset();
if (qhead < m_fmls.size() || !assumptions.empty()) { if (qhead < m_fmls.size() || !assumptions.empty()) {
TRACE("solver", tout << "qhead " << qhead << "\n");
m_preprocess_state.replay(qhead, assumptions); m_preprocess_state.replay(qhead, assumptions);
m_preprocess_state.freeze(assumptions); m_preprocess_state.freeze(assumptions);
m_preprocess.reduce(); m_preprocess.reduce();
if (!m.inc()) if (!m.inc())
return; return;
TRACE("solver", tout << "qhead " << qhead << "\n";
m_preprocess_state.display(tout));
m_preprocess_state.advance_qhead(); m_preprocess_state.advance_qhead();
for (unsigned i = 0; i < assumptions.size(); ++i) for (unsigned i = 0; i < assumptions.size(); ++i)
m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i)); m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i));