Add algorithm for finding pairs of paths in a node trie (#8286)

This is in preparation for cleaning our implementation of care graph computations.

Right now, UF, datatypes, sets, and strings all have copy/pasted versions of an algorithm that creates an index of operators and run the algorithm in the PR for computing care graphs.

Followup PRs will extend the theory interface and add an instance of this class for computing care graphs. Then, we will add optimized care graph computation for bags (which is missing right now), and then perhaps revisit arrays, which appears to have issues in its computeCareGraph method.

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 67e67ca44f13ace45ecd6f565631f5a2c2f7676d..8db3ba4ed8c51a6cb4f754b17a9d31a42444ee93 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -52,6 +52,8 @@ libcvc5_add_sources(
   node_self_iterator.h
   node_trie.cpp
   node_trie.h
+  node_trie_algorithm.cpp
+  node_trie_algorithm.h
   node_traversal.cpp
   node_traversal.h
   node_value.cpp

diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp
index ae33ae92f347373924475cfda4d8c761a9c8cc18..4e6e27e9e68ce90791318223aeeb24bf0335a89b 100644 (file)
--- a/src/expr/node_trie.cpp
+++ b/src/expr/node_trie.cpp
@@ -16,7 +16,6 @@
 #include "expr/node_trie.h"
 
 namespace cvc5 {
-namespace theory {
 
 template <bool ref_count>
 NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::existsTerm(
@@ -92,5 +91,4 @@ template void NodeTemplateTrie<false>::debugPrint(const char* c,
 template void NodeTemplateTrie<true>::debugPrint(const char* c,
                                                  unsigned depth) const;
 
-}  // namespace theory
 }  // namespace cvc5

diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h
index 8617d19f598197e957f141bb54b7ac4fc32d95e4..f6c3312a9049211c257b0374f706c994fc25e4eb 100644 (file)
--- a/src/expr/node_trie.h
+++ b/src/expr/node_trie.h
@@ -22,7 +22,6 @@
 #include "expr/node.h"
 
 namespace cvc5 {
-namespace theory {
 
 /** NodeTemplate trie class
  *
@@ -107,7 +106,6 @@ typedef NodeTemplateTrie<true> NodeTrie;
 /** Non-reference-counted version of the above data structure */
 typedef NodeTemplateTrie<false> TNodeTrie;
 
-}  // namespace theory
 }  // namespace cvc5
 
 #endif /* CVC5__EXPR__NODE_TRIE_H */

diff --git a/src/expr/node_trie_algorithm.cpp b/src/expr/node_trie_algorithm.cpp
new file mode 100644 (file)
index 0000000..3bd9016
--- /dev/null
+++ b/src/expr/node_trie_algorithm.cpp
@@ -0,0 +1,90 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Algorithms for node tries
+ */
+
+#include "expr/node_trie_algorithm.h"
+
+namespace cvc5 {
+
+void nodeTriePathPairProcess(const TNodeTrie* t,
+                             size_t arity,
+                             NodeTriePathPairProcessCallback& ntpc)
+{
+  std::vector<std::tuple<const TNodeTrie*, const TNodeTrie*, size_t>> visit;
+  std::tuple<const TNodeTrie*, const TNodeTrie*, size_t> cur;
+  const TNodeTrie* t1;
+  const TNodeTrie* t2;
+  size_t depth;
+  visit.emplace_back(t, nullptr, 0);
+  do
+  {
+    cur = visit.back();
+    t1 = std::get<0>(cur);
+    t2 = std::get<1>(cur);
+    depth = std::get<2>(cur);
+    visit.pop_back();
+    if (depth == arity)
+    {
+      // We are at the leaves. If we split the path, process the data.
+      if (t2 != nullptr)
+      {
+        ntpc.processData(t1->getData(), t2->getData());
+      }
+    }
+    else if (t2 == nullptr)
+    {
+      // we are exploring paths with a common prefix
+      if (depth < (arity - 1))
+      {
+        // continue exploring paths with common prefix, internal to each child
+        for (const std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
+        {
+          visit.emplace_back(&tt.second, nullptr, depth + 1);
+        }
+      }
+      // consider splitting the path at this node
+      for (std::map<TNode, TNodeTrie>::const_iterator it = t1->d_data.begin();
+           it != t1->d_data.end();
+           ++it)
+      {
+        std::map<TNode, TNodeTrie>::const_iterator it2 = it;
+        ++it2;
+        for (; it2 != t1->d_data.end(); ++it2)
+        {
+          if (ntpc.considerPath(it->first, it2->first))
+          {
+            visit.emplace_back(&it->second, &it2->second, depth + 1);
+          }
+        }
+      }
+    }
+    else
+    {
+      Assert(t1 != t2);
+      // considering two different paths, take the product of their children
+      for (const std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+      {
+        for (const std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+        {
+          if (ntpc.considerPath(tt1.first, tt2.first))
+          {
+            visit.emplace_back(&tt1.second, &tt2.second, depth + 1);
+          }
+        }
+      }
+    }
+  } while (!visit.empty());
+}
+
+}  // namespace cvc5

diff --git a/src/expr/node_trie_algorithm.h b/src/expr/node_trie_algorithm.h
new file mode 100644 (file)
index 0000000..caadecf
--- /dev/null
+++ b/src/expr/node_trie_algorithm.h
@@ -0,0 +1,52 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Algorithms for node tries
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__EXPR__NODE_TRIE_ALGORITHM_H
+#define CVC5__EXPR__NODE_TRIE_ALGORITHM_H
+
+#include "expr/node_trie.h"
+
+namespace cvc5 {
+
+/** A virtual base class for the algorithm below. */
+class NodeTriePathPairProcessCallback
+{
+ public:
+  NodeTriePathPairProcessCallback() {}
+  virtual ~NodeTriePathPairProcessCallback() {}
+  /** Whether to consider a pair in paths in a trie */
+  virtual bool considerPath(TNode a, TNode b) = 0;
+  /** Process leaves */
+  virtual void processData(TNode fa, TNode fb) = 0;
+};
+
+/**
+ * Given a TNode trie of arity n, this calls ntpc.processData(fa, fb) on all
+ * pairs of distinct leaves fa and fb in t at paths [fa1, ..., fan] and
+ * [fb1, ..., fbn] in t such that ntpc.considerPath(fai, fbi) returns true for
+ * all i = 1, ..., n.
+ *
+ * A common use case for this algorithm is computing the care graph for theory
+ * combination.
+ */
+void nodeTriePathPairProcess(const TNodeTrie* t,
+                             size_t n,
+                             NodeTriePathPairProcessCallback& ntpc);
+
+}  // namespace cvc5
+
+#endif /* CVC5__EXPR__NODE_TRIE_ALGORITHM_H */