mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

refactor watch_diseq, disable it completely

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-07 09:57:24 -08:00
parent 031e4cdb38
commit d21fc642b4
1 changed files with 25 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

54
src/smt/theory_bv.cpp
View file

@ -24,7 +24,7 @@ Revision History:
#include "smt/smt_model_generator.h" #include "smt/smt_model_generator.h"
#include "util/stats.h" #include "util/stats.h"
#define WATCH_DISEQ 1 #define WATCH_DISEQ 0
namespace smt { namespace smt {
@ -1160,9 +1160,6 @@ namespace smt {
literal_vector::const_iterator end1 = bits1.end(); literal_vector::const_iterator end1 = bits1.end();
literal_vector const & bits2 = m_bits[v2]; literal_vector const & bits2 = m_bits[v2];
literal_vector::const_iterator it2 = bits2.begin(); literal_vector::const_iterator it2 = bits2.begin();
#if WATCH_DISEQ
bool_var watch_var = null_bool_var;
#endif
for (; it1 != end1; ++it1, ++it2) { for (; it1 != end1; ++it1, ++it2) {
if (*it1 == ~(*it2)) if (*it1 == ~(*it2))
return; return;
@ -1171,35 +1168,34 @@ namespace smt {
if (val1 != l_undef && val2 != l_undef && val1 != val2) { if (val1 != l_undef && val2 != l_undef && val1 != val2) {
return; return;
} }
#if WATCH_DISEQ
if (watch_var != null_bool_var) {
// skip
}
else if (val1 == l_undef) {
watch_var = it1->var();
m_diseq_watch.reserve(watch_var+1);
m_diseq_watch[watch_var].push_back(std::make_pair(v1, v2));
m_diseq_watch_trail.push_back(watch_var);
}
else if (val2 == l_undef) {
watch_var = it2->var();
m_diseq_watch.reserve(watch_var+1);
m_diseq_watch[watch_var].push_back(std::make_pair(v1, v2));
m_diseq_watch_trail.push_back(watch_var);
}
#endif
} }
#if WATCH_DISEQ #if WATCH_DISEQ
if (watch_var != null_bool_var) { bool_var watch_var = null_bool_var;
unsigned h = hash_u_u(v1, v2); it1 = bits1.begin();
unsigned act = m_diseq_activity[hash_u_u(v1, v2) & 0xFF]++; it2 = bits2.begin();
if ((act & 0x1) == 0x1) { unsigned h = hash_u_u(v1, v2);
return; unsigned act = m_diseq_activity[hash_u_u(v1, v2) & 0xFF]++;
//m_replay_diseq.push_back(std::make_pair(v1, v2));
for (; it1 != end1 && ((act & 0x3) != 0x3); ++it1, ++it2) {
lbool val1 = ctx.get_assignment(*it1);
lbool val2 = ctx.get_assignment(*it2);
if (val1 == l_undef) {
watch_var = it1->var();
} }
m_diseq_watch[watch_var].pop_back(); else if (val2 == l_undef) {
m_diseq_watch_trail.pop_back(); watch_var = it2->var();
}
else {
continue;
}
m_diseq_watch.reserve(watch_var+1);
m_diseq_watch[watch_var].push_back(std::make_pair(v1, v2));
m_diseq_watch_trail.push_back(watch_var);
return;
//m_replay_diseq.push_back(std::make_pair(v1, v2));
} }
#endif #endif