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.h | |
| 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.h')
| -rw-r--r-- | src/smt/term_formula_removal.h | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index ac2644182..0c026a5fe 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -130,12 +130,10 @@ class RemoveTermFormulas { * Get the set of skolems introduced by this class that occur in node n, * add them to skolems. * - * This method uses an optimization that returns false immediately if n - * was unchanged by term formula removal, based on the initial context. - * - * Return true if any nodes were added to skolems. + * @param n The node to traverse + * @param skolems The set where the skolems are added */ - bool getSkolems(TNode n, + void getSkolems(TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const; /** |