mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

elaborate on clause reinitialization code path

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-03-28 12:57:34 -07:00
parent 67efd6531b
commit d0e016c35d
2 changed files with 17 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/polysat/solver.cpp
View file

@ -322,6 +322,14 @@ namespace polysat {
return any_of(c, [&](sat::literal lit) { return m_bvars.scope(lit) > 0; });
}
void solver::push_reinit_stack(clause& c) {
if (c.on_reinit_stack())
return;
c.set_on_reinit_stack(true);
m_clauses_to_reinit.push_back(&c);
}
// TODO
// pop_levels is called from pop and backjump
// backjump invoked a few places.
@ -339,6 +347,7 @@ namespace polysat {
unsigned j = old_sz;
for (unsigned i = old_sz; i < sz; i++) {
clause& c = *m_clauses_to_reinit[i];
SASSERT(c.on_reinit_stack());
bool reinit = false;
#if 0
// todo, private methods to constraint_manager
@ -702,6 +711,7 @@ namespace polysat {
void solver::push_level() {
++m_level;
m_reinit_heads.push_back(m_clauses_to_reinit.size());
m_trail.push_back(trail_instr_t::inc_level_i);
}
@ -746,6 +756,8 @@ namespace polysat {
case trail_instr_t::inc_level_i: {
--m_level;
--num_levels;
m_reinit_head = m_reinit_heads.back();
m_reinit_heads.pop_back();
break;
}
case trail_instr_t::viable_add_i: {
@ -795,6 +807,9 @@ namespace polysat {
}
m_constraints.release_level(m_level + 1);
// todo:
// reinit_clauses(m_reinit_head);
SASSERT(m_level == target_level);
}

2
src/math/polysat/solver.h
View file

@ -348,6 +348,8 @@ namespace polysat {
// clause reinitialization
ptr_vector<clause> m_clauses_to_reinit;
unsigned_vector m_reinit_heads;
unsigned m_reinit_head = 0;
void push_reinit_stack(clause& c);
void reinit_clauses(unsigned old_sz);
bool has_variables_to_reinit(clause const& c) const;