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/theory/output_channel.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/theory/output_channel.cpp')
-rw-r--r-- | src/theory/output_channel.cpp | 16 |
1 files changed, 2 insertions, 14 deletions
diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp index 91f30514c..e63b78486 100644 --- a/src/theory/output_channel.cpp +++ b/src/theory/output_channel.cpp @@ -84,19 +84,7 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p) return out; } -LemmaStatus::LemmaStatus(TNode rewrittenLemma, unsigned level) - : d_rewrittenLemma(rewrittenLemma), d_level(level) -{ -} - -TNode LemmaStatus::getRewrittenLemma() const { return d_rewrittenLemma; } - -unsigned LemmaStatus::getLevel() const { return d_level; } - -LemmaStatus OutputChannel::split(TNode n) -{ - return splitLemma(n.orNode(n.notNode())); -} +void OutputChannel::split(TNode n) { splitLemma(n.orNode(n.notNode())); } void OutputChannel::trustedConflict(TrustNode pconf) { @@ -104,7 +92,7 @@ void OutputChannel::trustedConflict(TrustNode pconf) << std::endl; } -LemmaStatus OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p) +void OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p) { Unreachable() << "OutputChannel::trustedLemma: no implementation" << std::endl; |