diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2a16069f5..5c9e91d32 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -86,7 +86,7 @@ Node TermDb::getOperator(size_t i) const } /** ground terms */ -size_t TermDb::getNumGroundTerms(Node f) const +size_t TermDb::getNumGroundTerms(TNode f) const { NodeDbListMap::const_iterator it = d_opMap.find(f); if (it != d_opMap.end()) @@ -96,7 +96,7 @@ size_t TermDb::getNumGroundTerms(Node f) const return 0; } -Node TermDb::getGroundTerm(Node f, size_t i) const +Node TermDb::getGroundTerm(TNode f, size_t i) const { NodeDbListMap::const_iterator it = d_opMap.find(f); if (it != d_opMap.end()) @@ -108,6 +108,16 @@ Node TermDb::getGroundTerm(Node f, size_t i) const return Node::null(); } +DbList* TermDb::getGroundTermList(TNode f) const +{ + NodeDbListMap::const_iterator it = d_opMap.find(f); + if (it != d_opMap.end()) + { + return it->second.get(); + } + return nullptr; +} + size_t TermDb::getNumTypeGroundTerms(TypeNode tn) const { TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn); @@ -286,7 +296,8 @@ void TermDb::computeUfEqcTerms( TNode f ) { { return; } - d_func_map_eqc_trie[f].clear(); + TNodeTrie& tnt = d_func_map_eqc_trie[f]; + tnt.clear(); // get the matchable operators in the equivalence class of f std::vector<TNode> ops; getOperatorsFor(f, ops); @@ -300,7 +311,7 @@ void TermDb::computeUfEqcTerms( TNode f ) { { computeArgReps(n); TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n); - d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]); + tnt.d_data[r].addTerm(n, d_arg_reps[n]); } } } |