mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-02 19:08:47 +00:00
Code Activity

cc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-30 11:45:41 -07:00
parent 7cff3d4236
commit d1118cb178
2 changed files with 12 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -221,9 +221,9 @@ namespace polysat {
LOG_H3("Propagate " << s.m_vars[v] << " in " << *this); LOG_H3("Propagate " << s.m_vars[v] << " in " << *this);
SASSERT(!vars().empty()); SASSERT(!vars().empty());
unsigned idx = 0; unsigned idx = 0;
if (vars()[idx] != v) if (var(idx) != v)
idx = 1; idx = 1;
SASSERT(v == vars()[idx]); SASSERT(v == var(idx));
// find other watch variable. // find other watch variable.
for (unsigned i = vars().size(); i-- > 2; ) { for (unsigned i = vars().size(); i-- > 2; ) {
unsigned other_v = vars()[i]; unsigned other_v = vars()[i];
@ -234,7 +234,7 @@ namespace polysat {
} }
} }
// at most one variable remains unassigned. // at most one variable remains unassigned.
unsigned other_v = vars()[idx]; unsigned other_v = var(idx);
propagate_core(s, is_positive, v, other_v); propagate_core(s, is_positive, v, other_v);
return false; return false;
} }
@ -271,6 +271,12 @@ namespace polysat {
}); });
} }
#if 0
// NB code review:
// resolve is done elsewhere or should be done elsewhere.
// by not having it as a method on clauses we can work with fixed literal arrays
// instead of dynamically expandable vectors.
bool clause::resolve(sat::bool_var var, clause const& other) { bool clause::resolve(sat::bool_var var, clause const& other) {
DEBUG_CODE({ DEBUG_CODE({
bool this_has_pos = std::count(begin(), end(), sat::literal(var)) > 0; bool this_has_pos = std::count(begin(), end(), sat::literal(var)) > 0;
@ -292,6 +298,7 @@ namespace polysat {
m_literals.push_back(lit); m_literals.push_back(lit);
return true; return true;
} }
#endif
std::ostream& clause::display(std::ostream& out) const { std::ostream& clause::display(std::ostream& out) const {
bool first = true; bool first = true;

3
src/math/polysat/constraint.h
View file

@ -161,6 +161,7 @@ namespace polysat {
ule_constraint const& to_ule() const; ule_constraint const& to_ule() const;
unsigned_vector& vars() { return m_vars; } unsigned_vector& vars() { return m_vars; }
unsigned_vector const& vars() const { return m_vars; } unsigned_vector const& vars() const { return m_vars; }
unsigned var(unsigned idx) const { return m_vars[idx]; }
unsigned level() const { return m_storage_level; } unsigned level() const { return m_storage_level; }
bool has_bvar() const { return m_bvar != sat::null_bool_var; } bool has_bvar() const { return m_bvar != sat::null_bool_var; }
sat::bool_var bvar() const { return m_bvar; } sat::bool_var bvar() const { return m_bvar; }
@ -347,7 +348,7 @@ namespace polysat {
static clause_ref from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals); static clause_ref from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals);
// Resolve with 'other' upon 'var'. // Resolve with 'other' upon 'var'.
bool resolve(sat::bool_var var, clause const& other); // bool resolve(sat::bool_var var, clause const& other);
p_dependency* dep() const { return m_dep; } p_dependency* dep() const { return m_dep; }
unsigned level() const { return m_level; } unsigned level() const { return m_level; }