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

keep track of qhead

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-25 11:42:16 +07:00
parent 5af6e1a046
commit 8184e7fe0a
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/simplifiers/card2bv.cpp
View file

@ -29,7 +29,7 @@ void card2bv::reduce() {
expr_ref new_f1(m), new_f2(m);
proof_ref new_pr(m);
for (unsigned idx = 0; !m_fmls.inconsistent() && idx < m_fmls.size(); idx++) {
for (unsigned idx = m_qhead; !m_fmls.inconsistent() && idx < m_fmls.size(); idx++) {
auto [f, d] = m_fmls[idx]();
rw1(f, new_f1);
rw2(false, new_f1, new_f2, new_pr);
@ -48,6 +48,8 @@ void card2bv::reduce() {
func_decl_ref_vector const& fns = rw2.fresh_constants();
for (func_decl* f : fns)
m_fmls.model_trail().hide(f);
advance_qhead(m_fmls.size());
}
void card2bv::collect_statistics(statistics& st) const {

3
src/ast/simplifiers/max_bv_sharing.cpp
View file

@ -253,7 +253,7 @@ public:
void reduce() override {
expr_ref new_curr(m);
proof_ref new_pr(m);
for (unsigned idx = 0; idx < m_fmls.size() && !m_fmls.inconsistent(); idx++) {
for (unsigned idx = m_qhead; idx < m_fmls.size() && !m_fmls.inconsistent(); idx++) {
auto [curr, d] = m_fmls[idx]();
m_rw(curr, new_curr, new_pr);
// Proof reconstruction: new_pr = m.mk_modus_ponens(old_pr, new_pr);
@ -261,6 +261,7 @@ public:
m_fmls.update(idx, dependent_expr(m, new_curr, d));
}
m_rw.cfg().cleanup();
advance_qhead(m_fmls.size());
}
};