diff options
Diffstat (limited to 'src/smt/term_formula_removal.cpp')
| -rw-r--r-- | src/smt/term_formula_removal.cpp | 23 |
1 files changed, 5 insertions, 18 deletions
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index f77ae7b49..9a856fc14 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -517,21 +517,9 @@ Node RemoveTermFormulas::getSkolemForNode(Node k) const return Node::null(); } -bool RemoveTermFormulas::getSkolems( +void RemoveTermFormulas::getSkolems( TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const { - // if n was unchanged by term formula removal, just return immediately - std::pair<Node, uint32_t> initial(n, d_rtfc.initialValue()); - TermFormulaCache::const_iterator itc = d_tfCache.find(initial); - if (itc != d_tfCache.end()) - { - if (itc->second == n) - { - return false; - } - } - // otherwise, traverse it - bool ret = false; std::unordered_set<TNode, TNodeHashFunction> visited; std::unordered_set<TNode, TNodeHashFunction>::iterator it; std::vector<TNode> visit; @@ -549,16 +537,15 @@ bool RemoveTermFormulas::getSkolems( { if (d_lemmaCache.find(cur) != d_lemmaCache.end()) { - // technically could already be in skolems if skolems was non-empty, - // regardless set return value to true. skolems.insert(cur); - ret = true; } } - visit.insert(visit.end(), cur.begin(), cur.end()); + else + { + visit.insert(visit.end(), cur.begin(), cur.end()); + } } } while (!visit.empty()); - return ret; } Node RemoveTermFormulas::getAxiomFor(Node n) |