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

update for equivalences

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-07-28 10:30:23 -07:00
parent 6dbfdf3e9c
commit b2b2c636f8
5 changed files with 68 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_scc.cpp
View file

@ -33,10 +33,11 @@ namespace sat {
struct frame {
unsigned m_lidx;
unsigned m_succ_idx;
bool m_first;
watched * m_it;
watched * m_end;
frame(unsigned lidx, watched * it, watched * end):m_lidx(lidx), m_first(true), m_it(it), m_end(end) {}
frame(unsigned lidx, watched * it, watched * end, unsigned sidx = 0):m_lidx(lidx), m_succ_idx(sidx), m_first(true), m_it(it), m_end(end) {}
};
typedef svector<frame> frames;
@ -75,7 +76,7 @@ namespace sat {
index.resize(num_lits, UINT_MAX);
lowlink.resize(num_lits, UINT_MAX);
in_s.resize(num_lits, false);
literal_vector roots;
literal_vector roots, lits;
roots.resize(m_solver.num_vars(), null_literal);
unsigned next_index = 0;
svector<frame> frames;
@ -106,6 +107,7 @@ namespace sat {
frame & fr = frames.back();
unsigned l_idx = fr.m_lidx;
if (!fr.m_first) {
SASSERT(fr.m_it->is_binary_clause());
// after visiting child
literal l2 = fr.m_it->get_literal();
unsigned l2_idx = l2.index();