trail.shrink(trail.size() - trail_lim[level]);
trail_lim.shrink(trail_lim.size() - level);
}
- // Now, clear the TheoryEngine queue
- proxy->clearAssertionQueues();
}
*/
CVC4_PUBLIC ~PropEngine();
+ /**
+ * This is called by SmtEngine, at shutdown time, just before
+ * destruction. It is important because there are destruction
+ * ordering issues between some parts of the system (notably between
+ * PropEngine and Theory). For now, there's nothing to do here in
+ * the PropEngine.
+ */
+ void shutdown() {
+ }
+
/**
* Converts the given formula to CNF and assert the CNF to the sat solver.
* The formula is asserted permanently for the current context.
inline size_t operator()(const SatLiteral& literal) const;
};
- inline SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, context::Context* context,
- const Options* options);
+ inline SatSolver(PropEngine* propEngine,
+ TheoryEngine* theoryEngine,
+ context::Context* context,
+ const Options* options);
inline ~SatSolver();
inline void enqueueTheoryLiteral(const SatLiteral& l);
inline void setCnfStream(CnfStream* cnfStream);
-
- inline void clearAssertionQueues();
};
}/* CVC4::prop namespace */
return out;
}
-size_t SatSolver::SatLiteralHashFcn::operator()(const SatLiteral& literal) const {
+inline size_t
+SatSolver::SatLiteralHashFcn::operator()(const SatLiteral& literal) const {
return (size_t) minisat::toInt(literal);
}
d_cnfStream = cnfStream;
}
-
-void SatSolver::clearAssertionQueues() {
- d_theoryEngine->clearAssertionQueues();
-}
-
}/* CVC4::prop namespace */
}/* CVC4 namespace */
d_options(opts) {
NodeManagerScope nms(d_nodeManager);
+
d_decisionEngine = new DecisionEngine;
d_theoryEngine = new TheoryEngine(this, d_ctxt);
d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt);
}
+void SmtEngine::shutdown() {
+ d_propEngine->shutdown();
+ d_theoryEngine->shutdown();
+ d_decisionEngine->shutdown();
+}
+
SmtEngine::~SmtEngine() {
NodeManagerScope nms(d_nodeManager);
+
+ shutdown();
+
delete d_propEngine;
delete d_theoryEngine;
delete d_decisionEngine;
// now in an SmtEnginePrivate class. See the comment in
// smt_engine.cpp.
+ /**
+ * This is called by the destructor, just before destroying the
+ * PropEngine, TheoryEngine, and DecisionEngine (in that order). It
+ * is important because there are destruction ordering issues
+ * between PropEngine and Theory.
+ */
+ void shutdown();
+
/**
* Full check of consistency in current context. Returns true iff
* consistent.
#include "theory/output_channel.h"
#include "context/context.h"
-#include <queue>
+#include <deque>
#include <list>
#include <typeinfo>
namespace CVC4 {
+
+class TheoryEngine;
+
namespace theory {
// rewrite cache support
private:
template <class T>
- friend class TheoryImpl;
+ friend class ::CVC4::theory::TheoryImpl;
+
+ friend class ::CVC4::TheoryEngine;
/**
* Construct a Theory.
*/
Theory(context::Context* ctxt, OutputChannel& out) throw() :
d_context(ctxt),
+ d_facts(),
+ d_factsResetter(*this),
d_out(&out) {
}
*/
Theory();
+ /**
+ * The context for the Theory.
+ */
+ context::Context* d_context;
+
+ /**
+ * The assertFact() queue.
+ *
+ * This queue MUST be emptied by ANY call to check() at ANY effort
+ * level. In debug builds, this is checked. On backjump we clear
+ * the fact queue (see FactsResetter, below).
+ *
+ * These can safely be TNodes because the literal map maintained in
+ * the SAT solver keeps them live. As an added benefit, if we have
+ * them as TNodes, dtors are cheap (optimized away?).
+ */
+ std::deque<TNode> d_facts;
+
+ /** Helper class to reset the fact queue on pop(). */
+ class FactsResetter : public context::ContextNotifyObj {
+ Theory& d_thy;
+
+ public:
+ FactsResetter(Theory& thy) :
+ context::ContextNotifyObj(thy.d_context),
+ d_thy(thy) {
+ }
+
+ void notify() {
+ d_thy.d_facts.clear();
+ }
+ } d_factsResetter;
+
+ friend class FactsResetter;
+
protected:
/**
- * The output channel for the Theory.
+ * This is called at shutdown time by the TheoryEngine, just before
+ * destruction. It is important because there are destruction
+ * ordering issues between PropEngine and Theory (based on what
+ * hard-links to Nodes are outstanding). As the fact queue might be
+ * nonempty, we ensure here that it's clear. If you overload this,
+ * you must make an explicit call here to the Theory implementation
+ * of this function too.
*/
- context::Context* d_context;
+ virtual void shutdown() {
+ d_facts.clear();
+ }
+
+ context::Context* getContext() const {
+ return d_context;
+ }
/**
* The output channel for the Theory.
OutputChannel* d_out;
/**
- * The assertFact() queue.
+ * Returns true if the assertFact queue is empty
*/
- // FIXME CD: on backjump we clear the facts IFF the queue gets
- // emptied on every DL. In general I guess we need a CDQueue<>?
- // Perhaps one that asserts it's empty at each push?
- std::queue<Node> d_facts;
+ bool done() throw() {
+ return d_facts.empty();
+ }
/**
* Return whether a node is shared or not. Used by setup().
bool isShared(TNode n) throw();
/**
- * Returns true if the assertFact queue is empty
+ * Check whether a node is in the rewrite cache or not.
*/
- bool done() throw() {
- return d_facts.empty();
+ static bool inRewriteCache(TNode n) throw() {
+ return n.hasAttribute(RewriteCache());
+ }
+
+ /**
+ * Get the value of the rewrite cache (or Node::null()) if there is
+ * none).
+ */
+ static Node getRewriteCache(TNode n) throw() {
+ return n.getAttribute(RewriteCache());
}
public:
*/
virtual void preRegisterTerm(TNode) = 0;
+ /**
+ * Rewrite a term. Done one time for a Node, ever.
+ */
+ virtual Node rewrite(TNode n) {
+ return n;
+ }
+
/**
* Register a term.
*
*/
void assertFact(TNode n) {
Debug("theory") << "Theory::assertFact(" << n << ")" << std::endl;
- d_facts.push(n);
+ d_facts.push_back(n);
}
- /**
- * Clear the assertion queue.
- */
- void clearAssertionQueue() {
- while (d_facts.size() > 0) {
- d_facts.pop();
- }
- }
-
-
/**
* Check the current assignment's consistency.
*/
"Theory::get() called with assertion queue empty!" );
Node fact = d_facts.front();
- d_facts.pop();
+ d_facts.pop_front();
Debug("theory") << "Theory::get() => " << fact << "(" << d_facts.size() << " left)" << std::endl;
return top;
}
+Node TheoryEngine::rewrite(TNode in) {
+ if(inRewriteCache(in)) {
+ return getRewriteCache(in);
+ }
+
+ if(in.getKind() == kind::VARIABLE ||
+ in.getKind() == kind::SKOLEM) {
+ return in;
+ }
+
+ /*
+ theory::Theory* thy = theoryOf(in);
+ if(thy == NULL) {
+ Node out = rewriteBuiltins(in);
+ setRewriteCache(in, out);
+ return in;
+ } else {
+ Node out = thy->rewrite(in);
+ setRewriteCache(in, out);
+ return out;
+ }
+ */
+
+ if(in.getKind() == kind::EQUAL) {
+ Assert(in.getNumChildren() == 2);
+ if(in[0] == in[1]) {
+ Node out = NodeManager::currentNM()->mkNode(kind::TRUE);
+ //setRewriteCache(in, out);
+ return out;
+ }
+ } else {
+ Node out = rewriteChildren(in);
+ //setRewriteCache(in, out);
+ return out;
+ }
+
+ //setRewriteCache(in, in);
+ return in;
+}
+
}/* CVC4 namespace */
/**
* Check whether a node is in the rewrite cache or not.
*/
- bool inRewriteCache(TNode n) throw() {
+ static bool inRewriteCache(TNode n) throw() {
return n.hasAttribute(theory::RewriteCache());
}
* Get the value of the rewrite cache (or Node::null()) if there is
* none).
*/
- Node getRewriteCache(TNode n) throw() {
+ static Node getRewriteCache(TNode n) throw() {
return n.getAttribute(theory::RewriteCache());
}
- Node rewrite(TNode in) {
- /*
- Node out = theoryOf(in)->rewrite(in);
- in.setAttribute(theory::RewriteCache(), out);
- return out;
- */
- if(inRewriteCache(in)) {
- return getRewriteCache(in);
- } else if(in.getKind() == kind::VARIABLE) {
- return in;
- } else if(in.getKind() == kind::EQUAL) {
- Assert(in.getNumChildren() == 2);
- if(in[0] == in[1]) {
- Node out = NodeManager::currentNM()->mkNode(kind::TRUE);
- //in.setAttribute(theory::RewriteCache(), out);
- return out;
- }
- } else {
- NodeBuilder<> b(in.getKind());
- for(TNode::iterator c = in.begin(); c != in.end(); ++c) {
- b << rewrite(*c);
- }
- Node out = b;
- //in.setAttribute(theory::RewriteCache(), out);
- return out;
+ /**
+ * Get the value of the rewrite cache (or Node::null()) if there is
+ * none).
+ */
+ static void setRewriteCache(TNode n, TNode v) throw() {
+ return n.setAttribute(theory::RewriteCache(), v);
+ }
+
+ /**
+ * This is the top rewrite entry point, called during preprocessing.
+ * It dispatches to the proper theories to rewrite the given Node.
+ */
+ Node rewrite(TNode in);
+
+ /**
+ * Convenience function to recurse through the children, rewriting,
+ * while leaving the Node's kind alone.
+ */
+ Node rewriteChildren(TNode in) {
+ NodeBuilder<> b(in.getKind());
+ for(TNode::iterator c = in.begin(); c != in.end(); ++c) {
+ b << rewrite(*c);
}
+ return Node(b);
+ }
- //in.setAttribute(theory::RewriteCache(), in);
- return in;
+ /**
+ * Rewrite Nodes with builtin kind (that is, those Nodes n for which
+ * theoryOf(n) == NULL). The master list is in expr/builtin_kinds.
+ */
+ Node rewriteBuiltins(TNode in) {
+ switch(Kind k = in.getKind()) {
+ case kind::EQUAL:
+ return rewriteChildren(in);
+
+ case kind::ITE:
+ Unhandled(k);
+
+ case kind::SKOLEM:
+ case kind::VARIABLE:
+ return in;
+
+ case kind::TUPLE:
+ return rewriteChildren(in);
+
+ default:
+ Unhandled(k);
+ }
}
public:
d_theoryOfTable.registerTheory(&d_bv);
}
+ /**
+ * This is called at shutdown time by the SmtEngine, just before
+ * destruction. It is important because there are destruction
+ * ordering issues between PropEngine and Theory.
+ */
+ void shutdown() {
+ d_bool.shutdown();
+ d_uf.shutdown();
+ d_arith.shutdown();
+ d_arrays.shutdown();
+ d_bv.shutdown();
+ }
+
/**
* Get the theory associated to a given Node.
*
return d_theoryOut.d_conflictNode;
}
- /**
- * Clears the queues of the theories.
- */
- void clearAssertionQueues() {
- d_uf.clearAssertionQueue();
- }
-
};/* class TheoryEngine */
}/* CVC4 namespace */
"during backtracking");
}else{
//The attribute does not exist, so it is created and set
- ecN = new (true) ECData(d_context, n);
+ ecN = new (true) ECData(getContext(), n);
n.setAttribute(ECAttr(), ecN);
}
}
}
- ecChild->addPredecessor(n, d_context);
+ ecChild->addPredecessor(n, getContext());
}
}
Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl;
* virtual in the final design (?)
*/
Node DecisionEngine::nextDecision() {
- Unreachable();
+ Unimplemented();
}
}/* CVC4 namespace */
*/
virtual Node nextDecision();// = 0
+ /**
+ * This is called by SmtEngine, at shutdown time, just before
+ * destruction. It is important because there are destruction
+ * ordering issues between some parts of the system. For now,
+ * there's nothing to do here in the DecisionEngine.
+ */
+ virtual void shutdown() {
+ }
+
// TODO: design decision: decision engine should be notified of
// propagated lits, and also why(?) (so that it can make decisions
// based on the utility of various theories and various theory
projects / cvc5.git / commitdiff