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

add stubs for reinit_clauses

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

5
src/math/polysat/boolean.cpp
View file

@ -17,13 +17,14 @@ Author:
namespace polysat {
sat::bool_var bool_var_manager::new_var() {
sat::bool_var bool_var_manager::new_var(unsigned scope) {
sat::bool_var var;
if (m_unused.empty()) {
var = size();
m_value.push_back(l_undef);
m_value.push_back(l_undef);
m_level.push_back(UINT_MAX);
m_scope.push_back(scope);
m_deps.push_back(null_dependency);
m_kind.push_back(kind_t::unassigned);
m_reason.push_back(nullptr);
@ -34,6 +35,7 @@ namespace polysat {
var = m_unused.back();
m_unused.pop_back();
auto lit = sat::literal(var);
m_scope[var] = scope;
SASSERT_EQ(m_value[lit.index()], l_undef);
SASSERT_EQ(m_value[(~lit).index()], l_undef);
SASSERT_EQ(m_level[var], UINT_MAX);
@ -52,6 +54,7 @@ namespace polysat {
m_value[lit.index()] = l_undef;
m_value[(~lit).index()] = l_undef;
m_level[var] = UINT_MAX;
m_scope[var] = UINT_MAX;
m_kind[var] = kind_t::unassigned;
m_reason[var] = nullptr;
m_deps[var] = null_dependency;

6
src/math/polysat/boolean.h
View file

@ -34,6 +34,7 @@ namespace polysat {
svector<sat::bool_var> m_unused; // previously deleted variables that can be reused by new_var();
svector<lbool> m_value; // current value (indexed by literal)
unsigned_vector m_level; // level of assignment (indexed by variable)
unsigned_vector m_scope; // scope where variable is active
dependency_vector m_deps; // dependencies of external asserts
svector<kind_t> m_kind; // decision or propagation?
ptr_vector<clause> m_reason; // reasons for bool-propagated literals
@ -49,7 +50,7 @@ namespace polysat {
// allocated size (not the number of active variables)
unsigned size() const { return m_level.size(); }
sat::bool_var new_var();
sat::bool_var new_var(unsigned scope);
void del_var(sat::bool_var var);
bool is_assigned(sat::bool_var var) const { SASSERT(invariant(var)); return value(var) != l_undef; }
@ -69,6 +70,9 @@ namespace polysat {
bool is_undef(sat::literal lit) const { return value(lit) == l_undef; }
unsigned level(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_level[var]; }
unsigned level(sat::literal lit) const { return level(lit.var()); }
unsigned scope(sat::literal lit) const { return scope(lit.var()); }
unsigned scope(sat::bool_var var) const { return m_scope[var]; }
void set_scope(sat::bool_var var, unsigned scope) { m_scope[var] = scope; }
clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); SASSERT(is_bool_propagation(var) == !!m_reason[var]); return m_reason[var]; }
clause* reason(sat::literal lit) const { return reason(lit.var()); }
dependency dep(sat::bool_var var) const { return var == sat::null_bool_var ? null_dependency : m_deps[var]; }

4
src/math/polysat/clause.h
View file

@ -36,6 +36,7 @@ namespace polysat {
unsigned m_ref_count = 0; // TODO: remove refcount once we confirm it's not needed anymore
bool m_redundant = redundant_default;
bool m_active = false; // clause is active iff it has been added to the solver and boolean watchlists
bool m_on_reinit_stack = false;
sat::literal_vector m_literals;
char const* m_name = "";
@ -84,6 +85,9 @@ namespace polysat {
void set_name(char const* name) { m_name = name; }
char const* name() const { return m_name; }
void set_on_reinit_stack(bool f) { m_on_reinit_stack = f; }
bool on_reinit_stack() const { return m_on_reinit_stack; }
};
inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); }

13
src/math/polysat/constraint_manager.cpp
View file

@ -46,7 +46,7 @@ namespace polysat {
void constraint_manager::ensure_bvar(constraint* c) {
if (!c->has_bvar())
assign_bv2c(s.m_bvars.new_var(), c);
assign_bv2c(s.m_bvars.new_var(s.m_level), c);
}
void constraint_manager::erase_bvar(constraint* c) {
@ -130,16 +130,16 @@ namespace polysat {
SASSERT(std::all_of(cl.begin() + 1, cl.end(), [&](auto lit) { return get_watch_level(lit) <= get_watch_level(cl[1]); }));
}
void constraint_manager::watch(clause& cl) {
bool constraint_manager::watch(clause& cl) {
if (cl.empty())
return;
return false;
if (cl.size() == 1) {
if (s.m_bvars.is_false(cl[0]))
s.set_conflict(cl);
else if (!s.m_bvars.is_assigned(cl[0]))
s.assign_propagate(cl[0], cl);
return;
return true;
}
normalize_watch(cl);
@ -148,16 +148,17 @@ namespace polysat {
s.m_bvars.watch(cl[1]).push_back(&cl);
if (s.m_bvars.is_true(cl[0]))
return;
return false;
SASSERT(!s.m_bvars.is_true(cl[1]));
if (!s.m_bvars.is_false(cl[1])) {
SASSERT(!s.m_bvars.is_assigned(cl[0]) && !s.m_bvars.is_assigned(cl[1]));
return;
return false;
}
if (s.m_bvars.is_false(cl[0]))
s.set_conflict(cl);
else
s.assign_propagate(cl[0], cl);
return true;
}
void constraint_manager::unwatch(clause& cl) {

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

@ -77,7 +77,7 @@ namespace polysat {
void gc_clauses();
void normalize_watch(clause& cl);
void watch(clause& cl);
bool watch(clause& cl);
void unwatch(clause& cl);
void register_clause(clause* cl);

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

@ -318,6 +318,58 @@ namespace polysat {
}
}
bool solver::has_variables_to_reinit(clause const& c) const {
return any_of(c, [&](sat::literal lit) { return m_bvars.scope(lit) > 0; });
}
// TODO
// pop_levels is called from pop and backjump
// backjump invoked a few places.
// the logic for propagating clauses after a pop or backjump
// is different. pop_levels inserts into repropagate
// pop_levels should end with a call to reinit_clauses where
// old_sz is the current trail head for clauses created within the scope.
//
// pop-levels can also update the scope of variables created below the pop level.
// the scope of variables would be set to the new level for clauses surviving a pop.
void solver::reinit_clauses(unsigned old_sz) {
unsigned sz = m_clauses_to_reinit.size();
SASSERT(old_sz <= sz);
unsigned j = old_sz;
for (unsigned i = old_sz; i < sz; i++) {
clause& c = *m_clauses_to_reinit[i];
bool reinit = false;
#if 0
// todo, private methods to constraint_manager
m_constraints.unwatch(c);
reinit = m_constraints.watch(c);
#endif
// reinit <- true if clause is used for propagation
// has_variables_to_reinit:
// = clause contains literal that was created above base level.
// Each Boolean has a "scope". The scope is initialized to the scope where
// the Boolean is created.
// TODO
// The scope is updated on pop to be the new level where the clause resides.
// the reinit-stack is also
if (reinit && !at_base_level())
// clause propagated literal, must keep it in the reinit stack.
m_clauses_to_reinit[j++] = &c;
else if (has_variables_to_reinit(c) && !at_base_level())
m_clauses_to_reinit[j++] = &c;
else
c.set_on_reinit_stack(false);
}
m_clauses_to_reinit.shrink(j);
}
bool solver::can_repropagate() {
return !m_repropagate_lits.empty() && !is_conflict();
}
@ -742,6 +794,7 @@ namespace polysat {
m_trail.pop_back();
}
m_constraints.release_level(m_level + 1);
SASSERT(m_level == target_level);
}

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

@ -200,6 +200,7 @@ namespace polysat {
sat::literal_set m_ptrue_lits;
sat::literal_vector m_ptrue_lits_trail;
unsigned_vector m_ptrue_lits_size_trail;
void push_qhead() {
m_trail.push_back(trail_instr_t::qhead_i);
@ -344,6 +345,13 @@ namespace polysat {
signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); }
// clause reinitialization
ptr_vector<clause> m_clauses_to_reinit;
void push_reinit_stack(clause& c);
void reinit_clauses(unsigned old_sz);
bool has_variables_to_reinit(clause const& c) const;
bool inc() { return m_lim.inc(); }
void log_lemma_smt2(clause& clause);