mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

tuning relevancy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-07 08:05:40 -08:00
parent e22f713b19
commit 6f9082598c
3 changed files with 67 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/smt_relevancy.cpp
View file

@ -129,7 +129,7 @@ namespace smt {
struct relevancy_propagator_imp : public relevancy_propagator {
unsigned m_qhead;
expr_ref_vector m_relevant_exprs;
obj_hashtable<expr> m_is_relevant;
uint_set m_is_relevant;
typedef list<relevancy_eh *> relevancy_ehs;
obj_map<expr, relevancy_ehs *> m_relevant_ehs;
obj_map<expr, relevancy_ehs *> m_watches[2];
@ -242,7 +242,7 @@ namespace smt {
}
}
bool is_relevant_core(expr * n) const { return m_is_relevant.contains(n); }
bool is_relevant_core(expr * n) const { return m_is_relevant.contains(n->get_id()); }
bool is_relevant(expr * n) const override {
return !enabled() || is_relevant_core(n);
@ -275,7 +275,7 @@ namespace smt {
while (i != old_lim) {
--i;
expr * n = m_relevant_exprs.get(i);
m_is_relevant.erase(n);
m_is_relevant.remove(n->get_id());
TRACE("propagate_relevancy", tout << "unmarking:\n" << mk_ismt2_pp(n, get_manager()) << "\n";);
}
m_relevant_exprs.shrink(old_lim);
@ -303,7 +303,7 @@ namespace smt {
}
void set_relevant(expr * n) {
m_is_relevant.insert(n);
m_is_relevant.insert(n->get_id());
m_relevant_exprs.push_back(n);
m_context.relevant_eh(n);
}

68
src/smt/theory_bv.cpp
View file

@ -24,6 +24,7 @@ Revision History:
#include "smt/smt_model_generator.h"
#include "util/stats.h"
#define WATCH_DISEQ 1
namespace smt {
@ -629,7 +630,7 @@ namespace smt {
num *= numeral(2);
}
expr_ref sum(m_autil.mk_add(sz, args.c_ptr()), m);
th_rewriter rw(m);
th_rewriter rw(m);
rw(sum);
literal l(mk_eq(n, sum, false));
TRACE("bv",
@ -1159,21 +1160,48 @@ namespace smt {
literal_vector::const_iterator end1 = bits1.end();
literal_vector const & bits2 = m_bits[v2];
literal_vector::const_iterator it2 = bits2.begin();
#if WATCH_DISEQ
bool_var watch_var = null_bool_var;
#endif
for (; it1 != end1; ++it1, ++it2) {
if (*it1 == ~(*it2))
return;
lbool v1 = ctx.get_assignment(*it1);
lbool v2 = ctx.get_assignment(*it2);
if (v1 != l_undef && v2 != l_undef && v1 != v2) {
lbool val1 = ctx.get_assignment(*it1);
lbool val2 = ctx.get_assignment(*it2);
if (val1 != l_undef && val2 != l_undef && val1 != val2) {
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
}
unsigned h = hash_u_u(v1, v2);
unsigned act = m_diseq_activity[hash_u_u(v1, v2) & 0xFF]++;
if ((act & 0xFF) == 0xFF) {
//m_replay_diseq.push_back(std::make_pair(v1, v2));
#if WATCH_DISEQ
if (watch_var != null_bool_var) {
unsigned h = hash_u_u(v1, v2);
unsigned act = m_diseq_activity[hash_u_u(v1, v2) & 0xFF]++;
if ((act & 0x1) == 0x1) {
return;
//m_replay_diseq.push_back(std::make_pair(v1, v2));
}
m_diseq_watch[watch_var].pop_back();
m_diseq_watch_trail.pop_back();
}
#endif
literal_vector & lits = m_tmp_literals;
lits.reset();
@ -1214,6 +1242,17 @@ namespace smt {
}
TRACE("bv", tout << "prop queue size: " << m_prop_queue.size() << "\n";);
propagate_bits();
#if WATCH_DISEQ
if (!get_context().inconsistent() && m_diseq_watch.size() > static_cast<unsigned>(v)) {
unsigned sz = m_diseq_watch[v].size();
for (unsigned i = 0; i < sz; ++i) {
auto const & p = m_diseq_watch[v][i];
expand_diseq(p.first, p.second);
}
m_diseq_watch[v].reset();
}
#endif
}
}
@ -1353,6 +1392,9 @@ namespace smt {
void theory_bv::push_scope_eh() {
theory::push_scope_eh();
m_trail_stack.push_scope();
#if WATCH_DISEQ
m_diseq_watch_lim.push_back(m_diseq_watch_trail.size());
#endif
}
void theory_bv::pop_scope_eh(unsigned num_scopes) {
@ -1362,6 +1404,16 @@ namespace smt {
m_bits.shrink(num_old_vars);
m_wpos.shrink(num_old_vars);
m_zero_one_bits.shrink(num_old_vars);
#if WATCH_DISEQ
unsigned old_trail_sz = m_diseq_watch_lim[m_diseq_watch_lim.size()-num_scopes];
for (unsigned i = m_diseq_watch_trail.size(); i-- > old_trail_sz;) {
if (!m_diseq_watch[m_diseq_watch_trail[i]].empty()) {
m_diseq_watch[m_diseq_watch_trail[i]].pop_back();
}
}
m_diseq_watch_trail.shrink(old_trail_sz);
m_diseq_watch_lim.shrink(m_diseq_watch_lim.size()-num_scopes);
#endif
theory::pop_scope_eh(num_scopes);
}

3
src/smt/theory_bv.h
View file

@ -127,6 +127,9 @@ namespace smt {
unsigned char m_eq_activity[256];
unsigned char m_diseq_activity[256];
svector<std::pair<theory_var, theory_var>> m_replay_diseq;
vector<vector<std::pair<theory_var, theory_var>>> m_diseq_watch;
svector<bool_var> m_diseq_watch_trail;
unsigned_vector m_diseq_watch_lim;
literal_vector m_tmp_literals;
svector<var_pos> m_prop_queue;