diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-28 11:03:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-28 11:03:33 -0500 |
commit | c38f35164adc5ab255803765a568ef820fa8f3b2 (patch) | |
tree | 6cbd4b21e8e9ff364b5b2f14467cd986ea69acf2 /src/proof | |
parent | b90cfb462bde3e75c07bb14e2393ee8e4b4f4d42 (diff) |
Use lemma property enum for OutputChannel::lemma (#4755)
There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.
This makes them into a enum.
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/proof_output_channel.cpp | 6 | ||||
-rw-r--r-- | src/proof/proof_output_channel.h | 4 |
2 files changed, 7 insertions, 3 deletions
diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp index 1e6e759e3..88467aea6 100644 --- a/src/proof/proof_output_channel.cpp +++ b/src/proof/proof_output_channel.cpp @@ -48,8 +48,10 @@ bool ProofOutputChannel::propagate(TNode x) { return true; } -theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, - bool, bool) { +theory::LemmaStatus ProofOutputChannel::lemma(TNode n, + ProofRule rule, + theory::LemmaProperty p) +{ Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl; // TODO(#1231): We should transition to supporting multiple lemmas. The // following assertion cannot be enabled due to diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h index 6a91bad7c..b68abd44b 100644 --- a/src/proof/proof_output_channel.h +++ b/src/proof/proof_output_channel.h @@ -38,7 +38,9 @@ class ProofOutputChannel : public theory::OutputChannel { */ void conflict(TNode n, std::unique_ptr<Proof> pf) override; bool propagate(TNode x) override; - theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) override; + theory::LemmaStatus lemma(TNode n, + ProofRule rule, + theory::LemmaProperty p) override; theory::LemmaStatus splitLemma(TNode, bool) override; void requirePhase(TNode n, bool b) override; void setIncomplete() override; |