mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

Don't nest propgate() calls

Browse source
This commit is contained in:
Jakob Rath 2022-01-20 17:06:30 +01:00
parent c9b9b5f531
commit 64152c338d
3 changed files with 17 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -76,6 +76,7 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
#define LOG(x) LOG_(LogLevel::Default , x) #define LOG(x) LOG_(LogLevel::Default , x)
#define LOG_V(x) LOG_(LogLevel::Verbose , x) #define LOG_V(x) LOG_(LogLevel::Verbose , x)
#define COND_LOG(c, x) if (c) LOG(x) #define COND_LOG(c, x) if (c) LOG(x)
#define LOGE(x) LOG(#x << " = " << (x))
#define IF_LOGGING(x) \ #define IF_LOGGING(x) \
do { \ do { \
@ -96,6 +97,8 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
#define LOG_H3(x) LOG_(0, x) #define LOG_H3(x) LOG_(0, x)
#define LOG(x) LOG_(0, x) #define LOG(x) LOG_(0, x)
#define LOG_V(x) LOG_(0, x) #define LOG_V(x) LOG_(0, x)
#define COND_LOG(c, x) LOG_(c, x)
#define LOGE(x) LOG_(0, x)
#define IF_LOGGING(x) \ #define IF_LOGGING(x) \
do { \ do { \

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

@ -192,6 +192,10 @@ namespace polysat {
void solver::propagate() { void solver::propagate() {
if (!can_propagate()) if (!can_propagate())
return; return;
static bool propagating = false;
if (propagating)
return;
propagating = true;
push_qhead(); push_qhead();
while (can_propagate()) { while (can_propagate()) {
auto const& item = m_search[m_qhead++]; auto const& item = m_search[m_qhead++];
@ -230,14 +234,19 @@ namespace polysat {
*/ */
void solver::propagate(pvar v) { void solver::propagate(pvar v) {
LOG_H2("Propagate v" << v); LOG_H2("Propagate v" << v);
SASSERT(!m_locked_wlist);
DEBUG_CODE(m_locked_wlist = v;);
auto& wlist = m_pwatch[v]; auto& wlist = m_pwatch[v];
unsigned i = 0, j = 0, sz = wlist.size(); unsigned i = 0, j = 0, sz = wlist.size();
LOG("wlist old: " << wlist);
for (; i < sz && !is_conflict(); ++i) for (; i < sz && !is_conflict(); ++i)
if (!wlist[i].propagate(*this, v)) if (!wlist[i].propagate(*this, v))
wlist[j++] = wlist[i]; wlist[j++] = wlist[i];
for (; i < sz; ++i) for (; i < sz; ++i)
wlist[j++] = wlist[i]; wlist[j++] = wlist[i];
wlist.shrink(j); wlist.shrink(j);
LOG("wlist new: " << wlist);
DEBUG_CODE(m_locked_wlist = std::nullopt;);
} }
bool solver::propagate(sat::literal lit, clause& cl) { bool solver::propagate(sat::literal lit, clause& cl) {
@ -374,6 +383,7 @@ namespace polysat {
void solver::add_watch(signed_constraint c, pvar v) { void solver::add_watch(signed_constraint c, pvar v) {
SASSERT(c); SASSERT(c);
// SASSERT(m_locked_wlist != v); // appending doesn't interfere with propagation, so it should be fine
LOG("Watching v" << v << " in constraint " << c); LOG("Watching v" << v << " in constraint " << c);
m_pwatch[v].push_back(c); m_pwatch[v].push_back(c);
} }
@ -389,6 +399,7 @@ namespace polysat {
void solver::erase_watch(pvar v, signed_constraint c) { void solver::erase_watch(pvar v, signed_constraint c) {
if (v == null_var) if (v == null_var)
return; return;
SASSERT(m_locked_wlist != v);
auto& wlist = m_pwatch[v]; auto& wlist = m_pwatch[v];
unsigned sz = wlist.size(); unsigned sz = wlist.size();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {

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

@ -103,6 +103,9 @@ namespace polysat {
vector<rational> m_value; // assigned value vector<rational> m_value; // assigned value
vector<justification> m_justification; // justification for variable assignment vector<justification> m_justification; // justification for variable assignment
vector<signed_constraints> m_pwatch; // watch list datastructure into constraints. vector<signed_constraints> m_pwatch; // watch list datastructure into constraints.
#ifndef NDEBUG
std::optional<pvar> m_locked_wlist; // restrict watch list modification while it is begin propagated
#endif
unsigned_vector m_activity; unsigned_vector m_activity;
vector<pdd> m_vars; vector<pdd> m_vars;