diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-28 14:01:26 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-28 14:01:26 -0600 |
commit | e234ff58f561ac97642df15c698962faa9d1e5e4 (patch) | |
tree | cfac18adaeb0fccc348b81e84c854400d38a01fe /src/smt/term_formula_removal.cpp | |
parent | 3234db430074e278258e6d687c07146a59769a92 (diff) |
Simplify lemma interface (#5819)
This makes it so that TheoryEngine::lemma returns void not LemmaStatus.
Currently, there was only one use of LemmaStatus by theory solvers, which was CEGQI using it as a way of getting the preprocessed form of a lemma. This makes it so that there is an explicit method in Valuation for getting the preprocessed form of a term + its skolems and their definition assertions.
It also simplifies a few things, e.g. Valuation calls are forwarded to PropEngine instead of going through TheoryEngine. It fixes a few issues in TermFormulaRemoval related to getSkolems.
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) |