mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

address perf #2098

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-23 16:58:00 -08:00
parent 9c07167ff8
commit f7746e2284
2 changed files with 4 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/sat/sat_big.cpp
View file

@ -164,22 +164,22 @@ namespace sat {
DEBUG_CODE(for (unsigned i = 0; i < num_lits; ++i) { VERIFY(m_left[i] < m_right[i]);});
}
// svector<std::pair<literal, literal>> big::s_del_bin;
bool big::in_del(literal u, literal v) const {
if (u.index() > v.index()) std::swap(u, v);
return m_del_bin.contains(std::make_pair(u, v));
return m_del_bin[u.index()].contains(v);
}
void big::add_del(literal u, literal v) {
if (u.index() > v.index()) std::swap(u, v);
m_del_bin.push_back(std::make_pair(u, v));
m_del_bin[u.index()].push_back(v);
}
unsigned big::reduce_tr(solver& s) {
unsigned idx = 0;
unsigned elim = 0;
m_del_bin.reset();
m_del_bin.reserve(s.m_watches.size());
for (watch_list & wlist : s.m_watches) {
if (s.inconsistent()) break;
literal u = to_literal(idx++);
@ -211,22 +211,6 @@ namespace sat {
wlist.set_end(itprev);
}
#if 0
s_del_bin.append(m_del_bin);
IF_VERBOSE(1,
display(verbose_stream() << "Learned: " << learned() << ":");
verbose_stream() << "del-bin\n";
for (auto p : m_del_bin) {
verbose_stream() << p.first << " " << p.second << "\n";
if (safe_reach(~p.first, p.second)) {
display_path(verbose_stream(), ~p.first, p.second) << " " << "\n";
}
else {
display_path(verbose_stream(), ~p.second, p.first) << " " << "\n";
}
}
);
#endif
s.propagate(false);
return elim;
}

2
src/sat/sat_big.h
View file

@ -36,7 +36,7 @@ namespace sat {
bool m_learned;
bool m_include_cardinality;
svector<std::pair<literal, literal>> m_del_bin;
vector<svector<literal> > m_del_bin;
void init_dfs_num();