mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

ddnf

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-22 14:19:31 -07:00
parent cc642d2693
commit c3f2eb773a
1 changed files with 0 additions and 99 deletions
Download patch file Download diff file Expand all files Collapse all files

99
src/muz/ddnf/ddnf.cpp
View file

@ -945,37 +945,6 @@ namespace datalog {
//
-------------------------------
void add_pos(ddnf_node& n, vector<dot>& active) {
for (unsigned i = 0; i < n.pos().size(); ++i) {
active.push_back(n.pos()[i]);
// TBD: Garvit; prove (or disprove): there are no repetitions.
// the argument may be that the sub-expressions are
// traversed in DFS order, and that repeated dots
// cannot occur below each-other.
}
for (unsigned i = 0; i < active.size(); ++i) {
m_dots.find(active[i])->insert(&n);
}
for (unsigned i = 0; i < n.num_children(); ++i) {
vector<dot> active1(active);
add_pos(*n[i], active1);
}
}
void del_neg(ddnf_node& n, vector<dot>& active) {
for (unsigned i = 0; i < n.neg().size(); ++i) {
active.push_back(n.neg()[i]);
}
for (unsigned i = 0; i < active.size(); ++i) {
m_dots.find(active[i])->remove(&n);
}
for (unsigned i = 0; i < n.num_children(); ++i) {
vector<dot> active1(active);
del_neg(*n[i], active1);
}
}
class trie {
public:
class node {
@ -1026,71 +995,3 @@ namespace datalog {
};
#endif
#if 0
class dot {
tbv m_pos;
vector<tbv> m_negs;
public:
dot() {}
dot(tbv const& pos): m_pos(pos) {}
dot(tbv const& pos, vector<tbv> const& negs):
m_pos(pos), m_negs(negs) {
DEBUG_CODE(
for (unsigned i = 0; i < negs.size(); ++i) {
SASSERT(pos.size() == negs[i].size());
}
);
}
tbv const& pos() const { return m_pos; }
tbv neg(unsigned i) const { return m_negs[i]; }
unsigned size() const { return m_negs.size(); }
unsigned num_bits() const { return m_pos.size(); }
bool operator==(dot const& other) const {
if (m_pos != other.m_pos) return false;
if (m_negs.size() != other.m_negs.size()) return false;
for (unsigned i = 0; i < m_negs.size(); ++i) {
if (m_negs[i] != other.m_negs[i]) return false;
}
return true;
}
void display(std::ostream& out) {
out << "<";
m_pos.display(out);
out << "\\";
for (unsigned i = 0; i < m_negs.size(); ++i) {
m_negs[i].display(out);
if (i + 1 < m_negs.size()) out << " u ";
}
out << ">";
}
struct eq {
bool operator()(dot const& d1, dot const& d2) const {
return d1 == d2;
}
};
struct hash {
unsigned operator()(dot const& d) const {
unsigned h = d.pos().get_hash();
for (unsigned i = 0; i < d.size(); ++i) {
h ^= d.neg(i).get_hash();
}
return h;
}
};
};
vector<dot> m_pos;
vector<dot> m_neg;
vector<dot> const& pos() const { return m_pos; }
vector<dot> const& neg() const { return m_neg; }
ddnf_node* add_pos(dot const& d) { m_pos.push_back(d); return this; }
ddnf_node* add_neg(dot const& d) { m_neg.push_back(d); return this; }
#endif