**/
+#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);
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);
}
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);
}
#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;
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;
//
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;
#define __CVC4__THEORY__OUTPUT_CHANNEL_H
#include "base/cvc4_assert.h"
+#include "proof/proof_manager.h"
#include "smt/logic_exception.h"
#include "theory/interrupted.h"
-#include "proof/proof_manager.h"
+#include "util/proof.h"
#include "util/resource_manager.h"
namespace CVC4 {
* for inspection and the user-level at which the lemma will reside.
*/
class LemmaStatus {
- Node d_rewrittenLemma;
- unsigned d_level;
-
-public:
- LemmaStatus(TNode rewrittenLemma, unsigned level) :
- d_rewrittenLemma(rewrittenLemma),
- d_level(level) {
- }
+ public:
+ LemmaStatus(TNode rewrittenLemma, unsigned level)
+ : d_rewrittenLemma(rewrittenLemma), d_level(level) {}
/** Get the T-rewritten form of the lemma. */
TNode getRewrittenLemma() const throw() { return d_rewrittenLemma; }
*/
unsigned getLevel() const throw() { return d_level; }
-};/* class LemmaStatus */
+ private:
+ Node d_rewrittenLemma;
+ unsigned d_level;
+}; /* class LemmaStatus */
/**
* Generic "theory output channel" interface.
+ *
+ * All methods can throw unrecoverable CVC4::Exception's unless otherwise
+ * documented.
*/
class OutputChannel {
- /** Disallow copying: private constructor */
- OutputChannel(const OutputChannel&) CVC4_UNDEFINED;
-
- /** Disallow assignment: private operator=() */
- OutputChannel& operator=(const OutputChannel&) CVC4_UNDEFINED;
-
-public:
-
- /**
- * Construct an OutputChannel.
- */
- OutputChannel() {
- }
+ public:
+ /** Construct an OutputChannel. */
+ OutputChannel() {}
/**
* Destructs an OutputChannel. This implementation does nothing,
* but we need a virtual destructor for safety in case subclasses
* have a destructor.
*/
- virtual ~OutputChannel() {
- }
+ virtual ~OutputChannel() {}
+
+ OutputChannel(const OutputChannel&) = delete;
+ OutputChannel& operator=(const OutputChannel&) = delete;
/**
* With safePoint(), the theory signals that it is at a safe point
* and can be interrupted.
+ *
+ * @throws Interrupted if the theory can be safely interrupted.
*/
- virtual void safePoint(uint64_t amount)
- throw(Interrupted, UnsafeInterruptException, AssertionException)
- {}
+ virtual void safePoint(uint64_t amount) {}
/**
* Indicate a theory conflict has arisen.
* @param pf - a proof of the conflict. This is only non-null if proofs
* are enabled.
*/
- virtual void conflict(TNode n, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) = 0;
+ virtual void conflict(TNode n, Proof* pf = nullptr) = 0;
/**
* Propagate a theory literal.
* @param n - a theory consequence at the current decision level
* @return false if an immediate conflict was encountered
*/
- virtual bool propagate(TNode n) throw(AssertionException, UnsafeInterruptException) = 0;
+ virtual bool propagate(TNode n) = 0;
/**
* Tell the core that a valid theory lemma at decision level 0 has
* @return the "status" of the lemma, including user level at which
* the lemma resides; the lemma will be removed when this user level pops
*/
- virtual LemmaStatus lemma(TNode n, ProofRule rule,
- bool removable = false,
+ virtual LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false,
bool preprocess = false,
bool sendAtoms = false) = 0;
/**
* Variant of the lemma function that does not require providing a proof rule.
*/
- virtual LemmaStatus lemma(TNode n,
- bool removable = false,
- bool preprocess = false,
- bool sendAtoms = false) {
+ virtual LemmaStatus lemma(TNode n, bool removable = false,
+ bool preprocess = false, bool sendAtoms = false) {
return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms);
}
*
* @param n - a theory atom; must be of Boolean type
*/
- LemmaStatus split(TNode n)
- throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
- return splitLemma(n.orNode(n.notNode()));
- }
+ LemmaStatus split(TNode n) { return splitLemma(n.orNode(n.notNode())); }
virtual LemmaStatus splitLemma(TNode n, bool removable = false) = 0;
* been pre-registered
* @param phase - the phase to decide on n
*/
- virtual void requirePhase(TNode n, bool phase)
- throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
+ virtual void requirePhase(TNode n, bool phase) = 0;
/**
* Flips the most recent unflipped decision to the other phase and
* @return true if a decision was flipped; false if no decision
* could be flipped, or if the root decision was re-flipped
*/
- virtual bool flipDecision()
- throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
+ virtual bool flipDecision() = 0;
/**
* Notification from a theory that it realizes it is incomplete at
* this context level. If SAT is later determined by the
* TheoryEngine, it should actually return an UNKNOWN result.
*/
- virtual void setIncomplete() throw(AssertionException, UnsafeInterruptException) = 0;
+ virtual void setIncomplete() = 0;
/**
* "Spend" a "resource." The meaning is specific to the context in
* long-running operations, they cannot rely on resource() to break
* out of infinite or intractable computations.
*/
- virtual void spendResource(unsigned ammount) throw(UnsafeInterruptException) {}
+ virtual void spendResource(unsigned amount) {}
/**
* Handle user attribute.
*/
virtual void handleUserAttribute(const char* attr, Theory* t) {}
-
/** Demands that the search restart from sat search level 0.
* Using this leads to non-termination issues.
* It is appropriate for prototyping for theories.
*/
- virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {}
+ virtual void demandRestart() {}
-};/* class OutputChannel */
+}; /* class OutputChannel */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace theory
+} // namespace CVC4
#endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */
return result;
}
-bool TheoryEngine::EngineOutputChannel::propagate(TNode literal)
- throw(AssertionException, UnsafeInterruptException) {
- Debug("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
- ++ d_statistics.propagations;
+bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) {
+ Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
+ << ">::propagate(" << literal << ")" << std::endl;
+ ++d_statistics.propagations;
d_engine->d_outputChannelUsed = true;
return d_engine->propagate(literal, d_theory);
}
-void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf)
- throw(AssertionException, UnsafeInterruptException) {
- Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
- Assert (pf == NULL); // Theory shouldn't be producing proofs yet
- ++ d_statistics.conflicts;
+void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode,
+ Proof* proof) {
+ Trace("theory::conflict")
+ << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode
+ << ")" << std::endl;
+ Assert(!proof); // Theory shouldn't be producing proofs yet
+ ++d_statistics.conflicts;
d_engine->d_outputChannelUsed = true;
d_engine->conflict(conflictNode, d_theory);
}
~Statistics();
};/* class TheoryEngine::Statistics */
-
/**
* An output channel for Theory that passes messages
* back to a TheoryEngine.
*/
class EngineOutputChannel : public theory::OutputChannel {
-
friend class TheoryEngine;
/**
*/
Statistics d_statistics;
- /**
- * The theory owning this chanell.
- */
+ /** The theory owning this channel. */
theory::TheoryId d_theory;
- public:
+ public:
+ EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory)
+ : d_engine(engine), d_statistics(theory), d_theory(theory) {}
- EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory) :
- d_engine(engine),
- d_statistics(theory),
- d_theory(theory)
- {
- }
-
- void safePoint(uint64_t ammount) throw(theory::Interrupted, UnsafeInterruptException, AssertionException) {
- spendResource(ammount);
+ void safePoint(uint64_t amount) override {
+ spendResource(amount);
if (d_engine->d_interrupted) {
throw theory::Interrupted();
}
}
- void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException);
+ void conflict(TNode conflictNode, Proof* pf = nullptr) override;
+ bool propagate(TNode literal) override;
- bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException);
+ theory::LemmaStatus lemma(TNode lemma, ProofRule rule,
+ bool removable = false, bool preprocess = false,
+ bool sendAtoms = false) override;
- theory::LemmaStatus lemma(TNode lemma,
- ProofRule rule,
- bool removable = false,
- bool preprocess = false,
- bool sendAtoms = false);
+ theory::LemmaStatus splitLemma(TNode lemma,
+ bool removable = false) override;
- theory::LemmaStatus splitLemma(TNode lemma, bool removable = false);
-
- void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+ void demandRestart() override {
NodeManager* curr = NodeManager::currentNM();
- Node restartVar = curr->mkSkolem("restartVar",
- curr->booleanType(),
- "A boolean variable asserted to be true to force a restart");
- Trace("theory::restart") << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar << ")" << std::endl;
- ++ d_statistics.restartDemands;
+ Node restartVar = curr->mkSkolem(
+ "restartVar", curr->booleanType(),
+ "A boolean variable asserted to be true to force a restart");
+ Trace("theory::restart")
+ << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar
+ << ")" << std::endl;
+ ++d_statistics.restartDemands;
lemma(restartVar, RULE_INVALID, true);
}
- void requirePhase(TNode n, bool phase)
- throw(theory::Interrupted, AssertionException, UnsafeInterruptException) {
- Debug("theory") << "EngineOutputChannel::requirePhase("
- << n << ", " << phase << ")" << std::endl;
- ++ d_statistics.requirePhase;
+ void requirePhase(TNode n, bool phase) override {
+ Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", "
+ << phase << ")" << std::endl;
+ ++d_statistics.requirePhase;
d_engine->d_propEngine->requirePhase(n, phase);
}
- bool flipDecision()
- throw(theory::Interrupted, AssertionException, UnsafeInterruptException) {
+ bool flipDecision() override {
Debug("theory") << "EngineOutputChannel::flipDecision()" << std::endl;
- ++ d_statistics.flipDecision;
+ ++d_statistics.flipDecision;
return d_engine->d_propEngine->flipDecision();
}
- void setIncomplete() throw(AssertionException, UnsafeInterruptException) {
+ void setIncomplete() override {
Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl;
d_engine->setIncomplete(d_theory);
}
- void spendResource(unsigned ammount) throw(UnsafeInterruptException) {
- d_engine->spendResource(ammount);
+ void spendResource(unsigned amount) override {
+ d_engine->spendResource(amount);
}
- void handleUserAttribute( const char* attr, theory::Theory* t ){
- d_engine->handleUserAttribute( attr, t );
+ void handleUserAttribute(const char* attr, theory::Theory* t) override {
+ d_engine->handleUserAttribute(attr, t);
}
- private:
-
+ private:
/**
* A helper function for registering lemma recipes with the proof engine
*/
- void registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, theory::TheoryId theoryId);
- };/* class TheoryEngine::EngineOutputChannel */
+ void registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess,
+ theory::TheoryId theoryId);
+ }; /* class TheoryEngine::EngineOutputChannel */
/**
* Output channels for individual theories.
/**
* "Spend" a resource during a search or preprocessing.
*/
- void spendResource(unsigned ammount);
+ void spendResource(unsigned amount);
/**
* Adds a theory. Only one theory per TheoryId can be present, so if
class TestOutputChannel : public theory::OutputChannel {
public:
- std::vector< std::pair<enum OutputChannelCallType, Node> > d_callHistory;
-
TestOutputChannel() {}
+ ~TestOutputChannel() override {}
- ~TestOutputChannel() {}
-
- void safePoint(uint64_t ammount) throw(Interrupted, AssertionException) {}
+ void safePoint(uint64_t amount) override {}
- void conflict(TNode n, Proof* pf = NULL)
- throw(AssertionException, UnsafeInterruptException) {
+ void conflict(TNode n, Proof* pf = nullptr) override {
push(CONFLICT, n);
}
- bool propagate(TNode n)
- throw(AssertionException, UnsafeInterruptException) {
+ bool propagate(TNode n) override {
push(PROPAGATE, n);
return true;
}
- void propagateAsDecision(TNode n)
- throw(AssertionException, UnsafeInterruptException) {
- push(PROPAGATE_AS_DECISION, n);
- }
-
- LemmaStatus lemma(TNode n, ProofRule rule,
- bool removable = false,
- bool preprocess = false,
- bool sendAtoms = false) throw(AssertionException, UnsafeInterruptException) {
+ LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false,
+ bool preprocess = false, bool sendAtoms = false) override {
push(LEMMA, n);
return LemmaStatus(Node::null(), 0);
}
- void requirePhase(TNode, bool) throw(Interrupted, AssertionException, UnsafeInterruptException) {
- }
+ void requirePhase(TNode, bool) override {}
+ bool flipDecision() override { return true; }
+ void setIncomplete() override {}
+ void handleUserAttribute(const char* attr, theory::Theory* t) override {}
- bool flipDecision() throw(Interrupted, AssertionException, UnsafeInterruptException) {
- return true;
- }
-
- void setIncomplete() throw(AssertionException, UnsafeInterruptException) {
- }
-
- void handleUserAttribute( const char* attr, theory::Theory* t ) {
- }
-
- void clear() {
- d_callHistory.clear();
- }
-
- LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+ LemmaStatus splitLemma(TNode n, bool removable = false) override {
push(LEMMA, n);
return LemmaStatus(Node::null(), 0);
}
- Node getIthNode(int i) {
+ void clear() { d_callHistory.clear(); }
+
+ Node getIthNode(int i) const {
Node tmp = (d_callHistory[i]).second;
return tmp;
}
- OutputChannelCallType getIthCallType(int i) {
+ OutputChannelCallType getIthCallType(int i) const {
return (d_callHistory[i]).first;
}
- unsigned getNumCalls() {
- return d_callHistory.size();
- }
+ unsigned getNumCalls() const { return d_callHistory.size(); }
- void printIth(std::ostream& os, int i) {
+ void printIth(std::ostream& os, int i) const {
os << "[TestOutputChannel " << i;
os << " " << getIthCallType(i);
os << " " << getIthNode(i) << "]";
}
-private:
-
+ private:
void push(OutputChannelCallType call, TNode n) {
d_callHistory.push_back(std::make_pair(call, n));
}
+ std::vector< std::pair<enum OutputChannelCallType, Node> > d_callHistory;
};/* class TestOutputChannel */
}/* CVC4::theory namespace */
using namespace std;
class FakeOutputChannel : public OutputChannel {
- void conflict(TNode n, Proof* pf = NULL) throw(AssertionException) {
+ void conflict(TNode n, Proof* pf) override { Unimplemented(); }
+ bool propagate(TNode n) override { Unimplemented(); }
+ LemmaStatus lemma(TNode n, ProofRule rule, bool removable, bool preprocess,
+ bool sendAtoms) override {
Unimplemented();
}
- bool propagate(TNode n) throw(AssertionException) {
+ void requirePhase(TNode, bool) override { Unimplemented(); }
+ bool flipDecision() override { Unimplemented(); }
+ void setIncomplete() override { Unimplemented(); }
+ void handleUserAttribute(const char* attr, Theory* t) override {
Unimplemented();
}
- void propagateAsDecision(TNode n) throw(AssertionException) {
- Unimplemented();
- }
- LemmaStatus lemma(TNode n, ProofRule rule,
- bool removable,
- bool preprocess,
- bool sendAtoms) throw(AssertionException) {
- Unimplemented();
- }
- void requirePhase(TNode, bool) throw(AssertionException) {
- Unimplemented();
- }
- bool flipDecision() throw(AssertionException) {
- Unimplemented();
- }
- void explanation(TNode n) throw(AssertionException) {
- Unimplemented();
- }
- void setIncomplete() throw(AssertionException) {
- Unimplemented();
- }
- void handleUserAttribute( const char* attr, Theory* t ){
- Unimplemented();
- }
- LemmaStatus splitLemma(TNode n, bool removable) throw(TypeCheckingExceptionPrivate, AssertionException){
- Unimplemented();
- }
-};/* class FakeOutputChannel */
+ LemmaStatus splitLemma(TNode n, bool removable) override { Unimplemented(); }
+}; /* class FakeOutputChannel */
template<TheoryId theory>
class FakeTheory;
*/
enum OutputChannelCallType{CONFLICT, PROPAGATE, LEMMA, EXPLANATION};
class TestOutputChannel : public OutputChannel {
-private:
- void push(OutputChannelCallType call, TNode n) {
- d_callHistory.push_back(make_pair(call, n));
- }
-
-public:
- vector< pair<OutputChannelCallType, Node> > d_callHistory;
-
+ public:
TestOutputChannel() {}
+ ~TestOutputChannel() override {}
- ~TestOutputChannel() {}
-
- void safePoint(uint64_t amount)
- throw(Interrupted, UnsafeInterruptException, AssertionException)
- {}
+ void safePoint(uint64_t amount) override {}
- void conflict(TNode n, Proof* pf = NULL)
- throw(AssertionException) {
+ void conflict(TNode n, Proof* pf = nullptr) override {
push(CONFLICT, n);
}
- bool propagate(TNode n)
- throw(AssertionException) {
+ bool propagate(TNode n) override {
push(PROPAGATE, n);
return true;
}
- void propagateAsDecision(TNode n)
- throw(AssertionException) {
- // ignore
- }
-
- LemmaStatus lemma(TNode n, ProofRule rule,
- bool removable = false,
- bool preprocess = false,
- bool sendAtoms = false)
- throw(AssertionException) {
+ LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false,
+ bool preprocess = false, bool sendAtoms = false) override {
push(LEMMA, n);
return LemmaStatus(Node::null(), 0);
}
- LemmaStatus splitLemma(TNode n, bool removable) throw (TypeCheckingExceptionPrivate, AssertionException){
+ LemmaStatus splitLemma(TNode n, bool removable) override {
push(LEMMA, n);
return LemmaStatus(Node::null(), 0);
}
- void requirePhase(TNode, bool)
- throw(Interrupted, AssertionException) {
- Unreachable();
- }
+ void requirePhase(TNode, bool) override { Unreachable(); }
+ bool flipDecision() override { Unreachable(); }
+ void setIncomplete() override { Unreachable(); }
- bool flipDecision()
- throw(Interrupted, AssertionException) {
- Unreachable();
- }
+ void clear() { d_callHistory.clear(); }
- void setIncomplete()
- throw(AssertionException) {
- Unreachable();
- }
-
- void clear() {
- d_callHistory.clear();
- }
-
- Node getIthNode(int i) {
+ Node getIthNode(int i) const {
Node tmp = (d_callHistory[i]).second;
return tmp;
}
- OutputChannelCallType getIthCallType(int i) {
+ OutputChannelCallType getIthCallType(int i) const {
return (d_callHistory[i]).first;
}
- unsigned getNumCalls() {
- return d_callHistory.size();
+ unsigned getNumCalls() const { return d_callHistory.size(); }
+
+ private:
+ void push(OutputChannelCallType call, TNode n) {
+ d_callHistory.push_back(make_pair(call, n));
}
+ vector<pair<OutputChannelCallType, Node> > d_callHistory;
};
class DummyTheory : public Theory {
projects / cvc5.git / commitdiff