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.

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;