From bec60f763bbe8daf87413088f19a4b7c23ba7e5c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 30 Sep 2017 12:35:36 -0700
Subject: [PATCH] add diagnostics to DDNF and fix #1268
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/muz/ddnf/ddnf.cpp | 21 ++++++++++++++++-----
src/test/ddnf.cpp | 4 ++++
2 files changed, 20 insertions(+), 5 deletions(-)
diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp
index 0e2f6b35f..da1f5392b 100644
--- a/src/muz/ddnf/ddnf.cpp
+++ b/src/muz/ddnf/ddnf.cpp
@@ -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;
}
diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp
index 09f1a4cf9..c9eb6aa08 100644
--- a/src/test/ddnf.cpp
+++ b/src/test/ddnf.cpp
@@ -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);
}