diff options
author | Tim King <taking@cs.nyu.edu> | 2017-10-25 17:07:01 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-10-25 17:07:01 -0700 |
commit | 13c8e4a7b8575142ce9b70747969b71039389dfa (patch) | |
tree | b132e1b95223b2e9aa525388788912037037799a /src/proof | |
parent | 0e3f99d90a5fcafd04b04adf0d3e7e71ccfa65b0 (diff) |
Removing throw specifiers from OutputChannel and subclasses. (#1209)
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/proof_output_channel.cpp | 33 | ||||
-rw-r--r-- | src/proof/proof_output_channel.h | 46 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 38 |
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; |