mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

add diagnostics to DDNF and fix #1268

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-30 12:35:36 -07:00
parent 04b11d9721
commit bec60f763b
2 changed files with 20 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -192,10 +192,15 @@ namespace datalog {
for (unsigned i = 0; i < new_tbvs.size(); ++i) {
tbv const& nt = *new_tbvs[i];
IF_VERBOSE(10, m_tbv.display(verbose_stream() << "insert: ", nt); verbose_stream() << "\n";);
if (contains(nt)) continue;
ddnf_node* n = alloc(ddnf_node, *this, m_tbv, nt, m_noderefs.size());
m_noderefs.push_back(n);
m_nodes.insert(n);
ddnf_node* n;
if (contains(nt)) {
n = find(nt);
}
else {
n = alloc(ddnf_node, *this, m_tbv, nt, m_noderefs.size());
m_noderefs.push_back(n);
m_nodes.insert(n);
}
insert(*m_root, n, new_tbvs);
}
return find(t);
@ -275,13 +280,17 @@ namespace datalog {
void insert(ddnf_node& root, ddnf_node* new_n, ptr_vector<tbv const>& new_intersections) {
tbv const& new_tbv = new_n->get_tbv();
IF_VERBOSE(10, m_tbv.display(verbose_stream() << "root: ", root.get_tbv());
m_tbv.display(verbose_stream() << " new node ", new_tbv); verbose_stream() << "\n";);
SASSERT(m_tbv.contains(root.get_tbv(), new_tbv));
if (&root == new_n) return;
if (m_eq(&root, new_n)) return;
++m_stats.m_num_inserts;
bool inserted = false;
for (unsigned i = 0; i < root.num_children(); ++i) {
ddnf_node& child = *(root[i]);
++m_stats.m_num_comparisons;
IF_VERBOSE(10, m_tbv.display(verbose_stream() << "child ", child.get_tbv());
verbose_stream() << " contains: " << m_tbv.contains(child.get_tbv(), new_tbv) << "\n";);
if (m_tbv.contains(child.get_tbv(), new_tbv)) {
inserted = true;
insert(child, new_n, new_intersections);
@ -299,11 +308,13 @@ namespace datalog {
// checking for subset
if (m_tbv.contains(new_tbv, child.get_tbv())) {
subset_children.push_back(&child);
IF_VERBOSE(10, m_tbv.display(verbose_stream() << "contains child", child.get_tbv()); verbose_stream() << "\n";);
++m_stats.m_num_comparisons;
}
else if (m_tbv.intersect(child.get_tbv(), new_tbv, *intr)) {
// this means there is a non-full intersection
new_intersections.push_back(intr);
IF_VERBOSE(10, m_tbv.display(verbose_stream() << "intersect child ", child.get_tbv()); verbose_stream() << "\n";);
intr = m_tbv.allocate();
m_stats.m_num_comparisons += 2;
}

4
src/test/ddnf.cpp
View file

@ -214,6 +214,10 @@ void tst_ddnf1() {
ddnf.insert(*tX1);
ddnf.insert(*t1X);
ddnf.display(std::cout);
tbvm.deallocate(tXX);
tbvm.deallocate(t1X);
tbvm.deallocate(tX1);
tbvm.deallocate(t11);
}