mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

remove unused class fields in BV theory

Browse source
This commit is contained in:
Nuno Lopes 2020-06-02 16:36:38 +01:00
parent b9ecf2512f
commit 023b630b5a
2 changed files with 9 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_bv.cpp
View file

@ -192,7 +192,7 @@ namespace smt {
for (literal lit : bits) { for (literal lit : bits) {
expr_ref l(get_manager()); expr_ref l(get_manager());
ctx.literal2expr(lit, l); ctx.literal2expr(lit, l);
r.push_back(l); r.push_back(std::move(l));
} }
} }
@ -315,11 +315,8 @@ namespace smt {
unsigned sz = bits.size(); unsigned sz = bits.size();
SASSERT(get_bv_size(n) == sz); SASSERT(get_bv_size(n) == sz);
m_bits[v].reset(); m_bits[v].reset();
m_bits_expr.reset();
for (unsigned i = 0; i < sz; ++i) ctx.internalize(bits.c_ptr(), sz, true);
m_bits_expr.push_back(bits.get(i));
ctx.internalize(m_bits_expr.c_ptr(), sz, true);
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
expr * bit = bits.get(i); expr * bit = bits.get(i);
@ -1163,7 +1160,7 @@ namespace smt {
ctx.internalize(diff, true); ctx.internalize(diff, true);
literal arg = ctx.get_literal(diff); literal arg = ctx.get_literal(diff);
lits.push_back(arg); lits.push_back(arg);
exprs.push_back(diff); exprs.push_back(std::move(diff));
} }
m_stats.m_num_diseq_dynamic++; m_stats.m_num_diseq_dynamic++;
if (m.has_trace_stream()) { if (m.has_trace_stream()) {
@ -1427,7 +1424,9 @@ namespace smt {
m_find(*this), m_find(*this),
m_approximates_large_bvs(false) { m_approximates_large_bvs(false) {
memset(m_eq_activity, 0, sizeof(m_eq_activity)); memset(m_eq_activity, 0, sizeof(m_eq_activity));
#if WATCH_DISEQ
memset(m_diseq_activity, 0, sizeof(m_diseq_activity)); memset(m_diseq_activity, 0, sizeof(m_diseq_activity));
#endif
} }
theory_bv::~theory_bv() { theory_bv::~theory_bv() {

8
src/smt/theory_bv.h
View file

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