Unrecursified and merged bv::utils::is(Core|Equality)Term. (#1605)

This unrecursifies and merges bv::utils::isCoreTerm and bv::utils::isEqualityTerm to avoid
code duplication.

In the best case, the recursive implementation visits less nodes. This can be achieved with
the non-recursive implementation, however, at the cost of increased code complexity.
In practice, on QF_BV the new implementation slightly improves performance.

Tested against the recursive implementation with a temporary assertion on regression
tests (bv::utils::isCoreTerm was tested with --bv-eq-slicer=auto).
Further tested on QF_BV with a TO of 300s (slight performance improvement).

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index d458bc3a6866f19a477565b4c58edc8178b7292a..5e9133932b69967ba312517f78687cff2253353a 100644 (file)
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -126,75 +126,76 @@ bool isBVPredicate(TNode node)
          || k == kind::BITVECTOR_REDAND;
 }
 
-bool isCoreTerm(TNode term, TNodeBoolMap& cache)
+static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache)
 {
-  term = term.getKind() == kind::NOT ? term[0] : term;
-  TNodeBoolMap::const_iterator it = cache.find(term);
-  if (it != cache.end())
-  {
-    return it->second;
-  }
+  TNode t = term.getKind() == kind::NOT ? term[0] : term;
 
-  if (term.getNumChildren() == 0) return true;
+  std::vector<TNode> stack;
+  std::unordered_map<TNode, bool, TNodeHashFunction> visited;
+  stack.push_back(t);
 
-  if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV)
+  while (!stack.empty())
   {
-    Kind k = term.getKind();
-    if (k != kind::CONST_BITVECTOR && k != kind::BITVECTOR_CONCAT
-        && k != kind::BITVECTOR_EXTRACT && k != kind::EQUAL
-        && term.getMetaKind() != kind::metakind::VARIABLE)
+    TNode n = stack.back();
+    stack.pop_back();
+
+    if (cache.find(n) != cache.end()) continue;
+
+    if (n.getNumChildren() == 0)
     {
-      cache[term] = false;
-      return false;
+      cache[n] = true;
+      visited[n] = true;
+      continue;
     }
-  }
 
-  for (unsigned i = 0; i < term.getNumChildren(); ++i)
-  {
-    if (!isCoreTerm(term[i], cache))
+    if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, n)
+        == theory::THEORY_BV)
     {
-      cache[term] = false;
-      return false;
+      Kind k = n.getKind();
+      Assert(k != kind::CONST_BITVECTOR);
+      if (k != kind::EQUAL
+          && (iseq || k != kind::BITVECTOR_CONCAT)
+          && (iseq || k != kind::BITVECTOR_EXTRACT)
+          && n.getMetaKind() != kind::metakind::VARIABLE)
+      {
+        cache[n] = false;
+        continue;
+      }
     }
-  }
-
-  cache[term] = true;
-  return true;
-}
-
-bool isEqualityTerm(TNode term, TNodeBoolMap& cache)
-{
-  term = term.getKind() == kind::NOT ? term[0] : term;
-  TNodeBoolMap::const_iterator it = cache.find(term);
-  if (it != cache.end())
-  {
-    return it->second;
-  }
 
-  if (term.getNumChildren() == 0) return true;
-
-  if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV)
-  {
-    Kind k = term.getKind();
-    if (k != kind::CONST_BITVECTOR && k != kind::EQUAL
-        && term.getMetaKind() != kind::metakind::VARIABLE)
+    if (!visited[n])
     {
-      cache[term] = false;
-      return false;
+      visited[n] = true;
+      stack.push_back(n);
+      stack.insert(stack.end(), n.begin(), n.end());
     }
-  }
-
-  for (unsigned i = 0; i < term.getNumChildren(); ++i)
-  {
-    if (!isEqualityTerm(term[i], cache))
+    else
     {
-      cache[term] = false;
-      return false;
+      bool iseqt = true;
+      for (const Node& c : n)
+      {
+        Assert(cache.find(c) != cache.end());
+        if (!cache[c])
+        {
+          iseqt = false;
+          break;
+        }
+      }
+      cache[n] = iseqt;
     }
   }
+  Assert(cache.find(t) != cache.end());
+  return cache[t];
+}
 
-  cache[term] = true;
-  return true;
+bool isCoreTerm(TNode term, TNodeBoolMap& cache)
+{
+  return isCoreEqTerm(false, term, cache);
+}
+
+bool isEqualityTerm(TNode term, TNodeBoolMap& cache)
+{
+  return isCoreEqTerm(true, term, cache);
 }
 
 bool isBitblastAtom(Node lit)

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 7b08ef83f0e85b4b228ce145ca4bf598e17c4511..4bf84525d9ba350f3528799ce27612565f77764e 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -62,9 +62,11 @@ unsigned isPow2Const(TNode node, bool& isNeg);
 bool isBvConstTerm(TNode node);
 /* Returns true if node is a predicate over bit-vector nodes. */
 bool isBVPredicate(TNode node);
-/* Returns true if given term is a THEORY_BV term.  */
+/* Returns true if given term is a THEORY_BV \Sigma_core term.
+ * \Sigma_core = { concat, extract, =, bv constants, bv variables } */
 bool isCoreTerm(TNode term, TNodeBoolMap& cache);
-/* Returns true if given term is a bv constant, variable or equality term.  */
+/* Returns true if given term is a THEORY_BV \Sigma_equality term.
+ * \Sigma_equality = { =, bv constants, bv variables }  */
 bool isEqualityTerm(TNode term, TNodeBoolMap& cache);
 /* Returns true if given node is an atom that is bit-blasted.  */
 bool isBitblastAtom(Node lit);