From 665aeb203c4be6822ee61bed6c25107cba45083c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Mar 2022 22:18:12 -0600 Subject: [PATCH] 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. --- src/expr/CMakeLists.txt | 2 + src/expr/node_trie.cpp | 2 - src/expr/node_trie.h | 2 - src/expr/node_trie_algorithm.cpp | 90 ++++++++++++++++++++++++++++++++ src/expr/node_trie_algorithm.h | 52 ++++++++++++++++++ 5 files changed, 144 insertions(+), 4 deletions(-) create mode 100644 src/expr/node_trie_algorithm.cpp create mode 100644 src/expr/node_trie_algorithm.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 67e67ca44..8db3ba4ed 100644 --- 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 ae33ae92f..4e6e27e9e 100644 --- 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 NodeTemplate NodeTemplateTrie::existsTerm( @@ -92,5 +91,4 @@ template void NodeTemplateTrie::debugPrint(const char* c, template void NodeTemplateTrie::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 8617d19f5..f6c3312a9 100644 --- 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 NodeTrie; /** Non-reference-counted version of the above data structure */ typedef NodeTemplateTrie 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 index 000000000..3bd9016e0 --- /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> visit; + std::tuple 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& tt : t1->d_data) + { + visit.emplace_back(&tt.second, nullptr, depth + 1); + } + } + // consider splitting the path at this node + for (std::map::const_iterator it = t1->d_data.begin(); + it != t1->d_data.end(); + ++it) + { + std::map::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& tt1 : t1->d_data) + { + for (const std::pair& 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 index 000000000..caadecfc7 --- /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 */ -- 2.30.2