Removing throw specifiers from OutputChannel and subclasses. (#1209)

3 files changed, 75 insertions, 42 deletions

diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp
index 819cc0102..85a742dfa 100644
--- a/src/proof/proof_output_channel.cpp
+++ b/src/proof/proof_output_channel.cpp
@@ -15,25 +15,32 @@
 
 **/
 
+#include "proof/proof_output_channel.h"
+
 #include "base/cvc4_assert.h"
-#include "proof_output_channel.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/valuation.h"
 
 namespace CVC4 {
 
-ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(NULL) {}
+ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(nullptr) {}
+
+Proof* ProofOutputChannel::getConflictProof() {
+  Assert(hasConflict());
+  return d_proof;
+}
 
-void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() {
+void ProofOutputChannel::conflict(TNode n, Proof* pf) {
   Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl;
-  Assert(d_conflict.isNull());
-  Assert(!n.isNull());
+  Assert(!hasConflict());
+  Assert(!d_proof);
   d_conflict = n;
-  Assert(pf != NULL);
   d_proof = pf;
+  Assert(hasConflict());
+  Assert(d_proof);
 }
 
-bool ProofOutputChannel::propagate(TNode x) throw() {
+bool ProofOutputChannel::propagate(TNode x) {
   Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x
                   << std::endl;
   d_propagations.insert(x);
@@ -43,6 +50,12 @@ bool ProofOutputChannel::propagate(TNode x) throw() {
 theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool,
                                               bool, bool) {
   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
+  // "test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt".
+  // Assert(
+  //     d_lemma.isNull(),
+  //     "Multiple calls to ProofOutputChannel::lemma() are not supported.");
   d_lemma = n;
   return theory::LemmaStatus(TNode::null(), 0);
 }
@@ -52,18 +65,18 @@ theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) {
   return theory::LemmaStatus(TNode::null(), 0);
 }
 
-void ProofOutputChannel::requirePhase(TNode n, bool b) throw() {
+void ProofOutputChannel::requirePhase(TNode n, bool b) {
   Debug("pf::tp") << "ProofOutputChannel::requirePhase called" << std::endl;
   Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl;
 }
 
-bool ProofOutputChannel::flipDecision() throw() {
+bool ProofOutputChannel::flipDecision() {
   Debug("pf::tp") << "ProofOutputChannel::flipDecision called" << std::endl;
   AlwaysAssert(false);
   return false;
 }
 
-void ProofOutputChannel::setIncomplete() throw() {
+void ProofOutputChannel::setIncomplete() {
   Debug("pf::tp") << "ProofOutputChannel::setIncomplete called" << std::endl;
   AlwaysAssert(false);
 }
diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h
index b114ec25f..9516eb71b 100644
--- a/src/proof/proof_output_channel.h
+++ b/src/proof/proof_output_channel.h
@@ -16,31 +16,49 @@
 #ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
 #define __CVC4__PROOF_OUTPUT_CHANNEL_H
 
+#include <set>
 #include <unordered_set>
 
+#include "expr/node.h"
+#include "util/proof.h"
 #include "theory/output_channel.h"
+#include "theory/theory.h"
 
 namespace CVC4 {
 
 class ProofOutputChannel : public theory::OutputChannel {
-public:
+ public:
+  ProofOutputChannel();
+  ~ProofOutputChannel() override {}
+
+  /**
+   * This may be called at most once per ProofOutputChannel.
+   * Requires that `n` and `pf` are non-null.
+   */
+  void conflict(TNode n, Proof* pf) override;
+  bool propagate(TNode x) override;
+  theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) override;
+  theory::LemmaStatus splitLemma(TNode, bool) override;
+  void requirePhase(TNode n, bool b) override;
+  bool flipDecision() override;
+  void setIncomplete() override;
+
+  /** Has conflict() has been called? */
+  bool hasConflict() const { return !d_conflict.isNull(); }
+
+  /**
+   * Returns the proof passed into the conflict() call.
+   * Requires hasConflict() to hold.
+   */
+  Proof* getConflictProof();
+  Node getLastLemma() const { return d_lemma; }
+
+ private:
   Node d_conflict;
   Proof* d_proof;
   Node d_lemma;
   std::set<Node> d_propagations;
-
-  ProofOutputChannel();
-
-  virtual ~ProofOutputChannel() throw() {}
-
-  virtual void conflict(TNode n, Proof* pf) throw();
-  virtual bool propagate(TNode x) throw();
-  virtual theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool);
-  virtual theory::LemmaStatus splitLemma(TNode, bool);
-  virtual void requirePhase(TNode n, bool b) throw();
-  virtual bool flipDecision() throw();
-  virtual void setIncomplete() throw();
-};/* class ProofOutputChannel */
+}; /* class ProofOutputChannel */
 
 class MyPreRegisterVisitor {
   theory::Theory* d_theory;
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 7dee924be..62dcd0006 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -1021,31 +1021,32 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
   th->check(theory::Theory::EFFORT_FULL);
   Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - th->check() DONE" << std::endl;
 
-  if(oc.d_conflict.isNull()) {
+  if(!oc.hasConflict()) {
     Trace("pf::tp") << "; conflict is null" << std::endl;
-    Assert(!oc.d_lemma.isNull());
-    Trace("pf::tp") << "; ++ but got lemma: " << oc.d_lemma << std::endl;
+    Node lastLemma  = oc.getLastLemma();
+    Assert(!lastLemma.isNull());
+    Trace("pf::tp") << "; ++ but got lemma: " << lastLemma << std::endl;
 
-    if (oc.d_lemma.getKind() == kind::OR) {
+    if (lastLemma.getKind() == kind::OR) {
       Debug("pf::tp") << "OR lemma. Negating each child separately" << std::endl;
-      for (unsigned i = 0; i < oc.d_lemma.getNumChildren(); ++i) {
-        if (oc.d_lemma[i].getKind() == kind::NOT) {
-          Trace("pf::tp") << ";     asserting fact: " << oc.d_lemma[i][0] << std::endl;
-          th->assertFact(oc.d_lemma[i][0], false);
+      for (unsigned i = 0; i < lastLemma.getNumChildren(); ++i) {
+        if (lastLemma[i].getKind() == kind::NOT) {
+          Trace("pf::tp") << ";     asserting fact: " << lastLemma[i][0] << std::endl;
+          th->assertFact(lastLemma[i][0], false);
         }
         else {
-          Trace("pf::tp") << ";     asserting fact: " << oc.d_lemma[i].notNode() << std::endl;
-          th->assertFact(oc.d_lemma[i].notNode(), false);
+          Trace("pf::tp") << ";     asserting fact: " << lastLemma[i].notNode() << std::endl;
+          th->assertFact(lastLemma[i].notNode(), false);
         }
       }
-    }
-    else {
+    } else {
       Unreachable();
 
-      Assert(oc.d_lemma.getKind() == kind::NOT);
+      Assert(oc.getLastLemma().getKind() == kind::NOT);
       Debug("pf::tp") << "NOT lemma" << std::endl;
-      Trace("pf::tp") << ";     asserting fact: " << oc.d_lemma[0] << std::endl;
-      th->assertFact(oc.d_lemma[0], false);
+      Trace("pf::tp") << ";     asserting fact: " << oc.getLastLemma()[0]
+                      << std::endl;
+      th->assertFact(oc.getLastLemma()[0], false);
     }
 
     // Trace("pf::tp") << "; ++ but got lemma: " << oc.d_lemma << std::endl;
@@ -1054,10 +1055,11 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
 
     //
     th->check(theory::Theory::EFFORT_FULL);
+  } else {
+    Debug("pf::tp") << "Calling   oc.d_proof->toStream(os)" << std::endl;
+    oc.getConflictProof()->toStream(os, map);
+    Debug("pf::tp") << "Calling   oc.d_proof->toStream(os) -- DONE!" << std::endl;
   }
-  Debug("pf::tp") << "Calling   oc.d_proof->toStream(os)" << std::endl;
-  oc.d_proof->toStream(os, map);
-  Debug("pf::tp") << "Calling   oc.d_proof->toStream(os) -- DONE!" << std::endl;
 
   Debug("pf::tp") << "About to delete the theory solver used for proving the lemma... " << std::endl;
   delete th;