summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp534
1 files changed, 94 insertions, 440 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e2c42bccd..25fe29c67 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -26,14 +26,8 @@
#include "theory/theory.h"
#include "theory/theory_engine.h"
-#include "theory/builtin/theory_builtin.h"
-#include "theory/booleans/theory_bool.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/morgan/theory_uf_morgan.h"
-#include "theory/uf/tim/theory_uf_tim.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/rewriter.h"
+#include "theory/theory_traits.h"
using namespace std;
@@ -41,6 +35,12 @@ using namespace CVC4;
using namespace CVC4::theory;
namespace CVC4 {
+
+/** Tag for the "registerTerm()-has-been-called" flag on Nodes */
+struct Registered {};
+/** The "registerTerm()-has-been-called" flag on Nodes */
+typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
+
namespace theory {
struct PreRegisteredTag {};
@@ -129,150 +129,101 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
d_propEngine(NULL),
+ d_context(ctxt),
d_theoryOut(this, ctxt),
d_theoryRegistration(opts.theoryRegistration),
d_hasShutDown(false),
d_incomplete(ctxt, false),
d_statistics() {
- d_sharedTermManager = new SharedTermManager(this, ctxt);
+ Rewriter::init();
- d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut);
- d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut);
- switch(opts.uf_implementation) {
- case Options::TIM:
- d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut);
- break;
- case Options::MORGAN:
- d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut);
- break;
- default:
- Unhandled(opts.uf_implementation);
- }
- d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut);
- d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut);
- d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut);
-
- d_sharedTermManager->registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin));
- d_sharedTermManager->registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool));
- d_sharedTermManager->registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf));
- d_sharedTermManager->registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith));
- d_sharedTermManager->registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays));
- d_sharedTermManager->registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv));
-
- d_theoryOfTable.registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin));
- d_theoryOfTable.registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool));
- d_theoryOfTable.registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf));
- d_theoryOfTable.registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith));
- d_theoryOfTable.registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays));
- d_theoryOfTable.registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv));
+ d_sharedTermManager = new SharedTermManager(this, ctxt);
}
TheoryEngine::~TheoryEngine() {
Assert(d_hasShutDown);
- delete d_bv;
- delete d_arrays;
- delete d_arith;
- delete d_uf;
- delete d_bool;
- delete d_builtin;
-
- delete d_sharedTermManager;
-}
-
-Theory* TheoryEngine::theoryOf(TypeNode t) {
- // FIXME: we don't yet have a Type-to-Theory map. When we do,
- // look up the type of the var and return that Theory (?)
-
- // The following JUST hacks around this lack of a table
- Kind k = t.getKind();
- if(k == kind::TYPE_CONSTANT) {
- switch(TypeConstant tc = t.getConst<TypeConstant>()) {
- case BOOLEAN_TYPE:
- return d_theoryOfTable[kind::CONST_BOOLEAN];
- case INTEGER_TYPE:
- return d_theoryOfTable[kind::CONST_INTEGER];
- case REAL_TYPE:
- return d_theoryOfTable[kind::CONST_RATIONAL];
- case KIND_TYPE:
- default:
- Unhandled(tc);
+ for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++ theoryId) {
+ if (d_theoryTable[theoryId]) {
+ delete d_theoryTable[theoryId];
}
}
- return d_theoryOfTable[k];
+ delete d_sharedTermManager;
}
+struct preprocess_stack_element {
+ TNode node;
+ bool children_added;
+ preprocess_stack_element(TNode node)
+ : node(node), children_added(false) {}
+};
-Theory* TheoryEngine::theoryOf(TNode n) {
- Kind k = n.getKind();
+Node TheoryEngine::preprocess(TNode node) {
- Assert(k >= 0 && k < kind::LAST_KIND);
+ // Remove ITEs and rewrite the node
+ Node preprocessed = Rewriter::rewrite(removeITEs(node));
- if(n.getMetaKind() == kind::metakind::VARIABLE) {
- return theoryOf(n.getType());
- } else if(k == kind::EQUAL) {
- // equality is special: use LHS
- return theoryOf(n[0]);
- } else {
- // use our Kind-to-Theory mapping
- return d_theoryOfTable[k];
+ // If we are pre-registered already we are done
+ if (preprocessed.getAttribute(PreRegistered())) {
+ return preprocessed;
}
-}
-
-Node TheoryEngine::preprocess(TNode t) {
- Node top = rewrite(t);
- Debug("rewrite") << "rewrote: " << t << endl << "to : " << top << endl;
-
- list<TNode> toReg;
- toReg.push_back(top);
-
- /* Essentially this is doing a breadth-first numbering of
- * non-registered subterms with children. Any non-registered
- * leaves are immediately registered. */
- for(list<TNode>::iterator workp = toReg.begin();
- workp != toReg.end();
- ++workp) {
-
- TNode n = *workp;
- for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
- TNode c = *i;
-
- if(!c.getAttribute(theory::PreRegistered())) {// c not yet registered
- if(c.getNumChildren() == 0) {
- c.setAttribute(theory::PreRegistered(), true);
- theoryOf(c)->preRegisterTerm(c);
+ // Do a topological sort of the subexpressions and preregister them
+ vector<preprocess_stack_element> toVisit;
+ toVisit.push_back((TNode) preprocessed);
+ while (!toVisit.empty()) {
+ preprocess_stack_element& stackHead = toVisit.back();
+ // The current node we are processing
+ TNode current = stackHead.node;
+ // If we already added all the children its time to register or just pop from the stack
+ if (stackHead.children_added || current.getAttribute(PreRegistered())) {
+ if (!current.getAttribute(PreRegistered())) {
+ // Mark it as registered
+ current.setAttribute(PreRegistered(), true);
+ // Register this node
+ if (current.getKind() == kind::EQUAL) {
+ TheoryId theoryLHS = Theory::theoryOf(current[0]);
+ Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl;
+ d_theoryTable[theoryLHS]->preRegisterTerm(current);
+// TheoryId theoryRHS = Theory::theoryOf(current[1]);
+// if (theoryLHS != theoryRHS) {
+// d_theoryTable[theoryRHS]->preRegisterTerm(current);
+// Debug("register") << "preregistering " << current << " with " << theoryRHS << std::endl;
+// }
+// TheoryId typeTheory = Theory::theoryOf(current[0].getType());
+// if (typeTheory != theoryLHS && typeTheory != theoryRHS) {
+// d_theoryTable[typeTheory]->preRegisterTerm(current);
+// Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl;
+// }
} else {
- toReg.push_back(c);
+ TheoryId theory = Theory::theoryOf(current);
+ Debug("register") << "preregistering " << current << " with " << theory << std::endl;
+ d_theoryTable[theory]->preRegisterTerm(current);
+ TheoryId typeTheory = Theory::theoryOf(current.getType());
+ if (theory != typeTheory) {
+ Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl;
+ d_theoryTable[typeTheory]->preRegisterTerm(current);
+ }
+ }
+ }
+ // Done with this node, remove from the stack
+ toVisit.pop_back();
+ } else {
+ // Mark that we have added the children
+ stackHead.children_added = true;
+ // We need to add the children
+ for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
+ TNode childNode = *child_it;
+ if (!childNode.getAttribute(PreRegistered())) {
+ toVisit.push_back(childNode);
}
}
}
}
- /* Now register the list of terms in reverse order. Between this
- * and the above registration of leaves, this should ensure that
- * all subterms in the entire tree were registered in
- * reverse-topological order. */
- for(list<TNode>::reverse_iterator i = toReg.rbegin();
- i != toReg.rend();
- ++i) {
-
- TNode n = *i;
-
- /* Note that a shared TNode in the DAG rooted at "fact" could
- * appear twice on the list, so we have to avoid hitting it
- * twice. */
- // FIXME when ExprSets are online, use one of those to avoid
- // duplicates in the above?
- if(!n.getAttribute(theory::PreRegistered())) {
- n.setAttribute(theory::PreRegistered(), true);
- theoryOf(n)->preRegisterTerm(n);
- }
- }
-
- return top;
+ return preprocessed;
}
/* Our goal is to tease out any ITE's sitting under a theory operator. */
@@ -289,9 +240,9 @@ Node TheoryEngine::removeITEs(TNode node) {
if(node.getKind() == kind::ITE){
Assert( node.getNumChildren() == 3 );
- TypeNode nodeType = node[1].getType();
+ TypeNode nodeType = node.getType();
if(!nodeType.isBoolean()){
- Node skolem = nodeManager->mkVar(node.getType());
+ Node skolem = nodeManager->mkVar(nodeType);
Node newAssertion =
nodeManager->mkNode(kind::ITE,
node[0],
@@ -299,7 +250,7 @@ Node TheoryEngine::removeITEs(TNode node) {
nodeManager->mkNode(kind::EQUAL, skolem, node[2]));
nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem);
- Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])"
+ Debug("ite") << "removeITEs([" << node.getId() << "," << node << "," << nodeType << "])"
<< "->"
<< "["<<newAssertion.getId() << "," << newAssertion << "]"
<< endl;
@@ -330,277 +281,6 @@ Node TheoryEngine::removeITEs(TNode node) {
}
}
-namespace theory {
-namespace rewrite {
-
-/**
- * TheoryEngine::rewrite() keeps a stack of things that are being pre-
- * and post-rewritten. Each element of the stack is a
- * RewriteStackElement.
- */
-struct RewriteStackElement {
- /**
- * The node at this rewrite level. For example (AND (OR x y) z)
- * will have, as it's rewriting x, the stack:
- * x
- * (OR x y)
- * (AND (OR x y) z)
- */
- Node d_node;
-
- /**
- * The theory associated to d_node. Cached here to avoid having to
- * look it up again.
- */
- Theory* d_theory;
-
- /**
- * Whether or not this was a top-level rewrite. Note that at theory
- * boundaries, topLevel is forced to true, so it's not the case that
- * this is true only at the lowest stack level.
- */
- bool d_topLevel;
-
- /**
- * A saved index to the "next child" to pre- and post-rewrite. In
- * the case when (AND (OR x y) z) is being rewritten, the AND, OR,
- * and x are pre-rewritten, then (assuming they don't change), x is
- * post-rewritten, then y is pre- and post-rewritten, then the OR is
- * post-rewritten, then z is pre-rewritten, then the AND is
- * post-rewritten. At each stack level, we need to remember the
- * child index we're currently processing.
- */
- int d_nextChild;
-
- /**
- * A (re)builder for this node. As this node's children are
- * post-rewritten, in order, they append to this builder. When this
- * node is post-rewritten, it is reformed from d_builder since the
- * children may have changed. Note Nodes aren't rebuilt if they
- * have metakinds CONSTANT (which is illegal) or VARIABLE (which
- * would create a fresh variable, not what we want)---which is fine,
- * since those types don't have children anyway.
- */
- NodeBuilder<> d_builder;
-
- /**
- * Construct a fresh stack element.
- */
- RewriteStackElement(Node n, Theory* thy, bool topLevel) :
- d_node(n),
- d_theory(thy),
- d_topLevel(topLevel),
- d_nextChild(0) {
- }
-};
-
-}/* CVC4::theory::rewrite namespace */
-}/* CVC4::theory namespace */
-
-Node TheoryEngine::rewrite(TNode in, bool topLevel) {
- using theory::rewrite::RewriteStackElement;
-
- Node noItes = removeITEs(in);
- Node out;
-
- Debug("theory-rewrite") << "removeITEs of: " << in << endl
- << " is: " << noItes << endl;
-
- // descend top-down into the theory rewriters
- vector<RewriteStackElement> stack;
- stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), topLevel));
- Debug("theory-rewrite") << "TheoryEngine::rewrite() starting at" << endl
- << " " << noItes << " " << theoryOf(noItes)
- << " " << (topLevel ? "TOP-LEVEL " : "")
- << "0" << endl;
- // This whole thing is essentially recursive, but we avoid actually
- // doing any recursion.
- do {// do until the stack is empty..
- RewriteStackElement& rse = stack.back();
- bool done;
-
- Debug("theory-rewrite") << "rewriter looking at level " << stack.size()
- << endl
- << " " << rse.d_node << " " << rse.d_theory
- << "[" << *rse.d_theory << "]"
- << " " << (rse.d_topLevel ? "TOP-LEVEL " : "")
- << rse.d_nextChild << endl;
-
- if(rse.d_nextChild == 0) {
- Node original = rse.d_node;
- bool wasTopLevel = rse.d_topLevel;
- Node cached = getPreRewriteCache(original, wasTopLevel);
- if(cached.isNull()) {
- do {
- Debug("theory-rewrite") << "doing pre-rewrite in " << *rse.d_theory
- << " topLevel==" << rse.d_topLevel << endl;
- RewriteResponse response =
- rse.d_theory->preRewrite(rse.d_node, rse.d_topLevel);
- rse.d_node = response.getNode();
- Assert(!rse.d_node.isNull(), "node illegally rewritten to null");
- Theory* thy2 = theoryOf(rse.d_node);
- Assert(thy2 != NULL, "node illegally rewritten to null theory");
- Debug("theory-rewrite") << "got back " << rse.d_node << " "
- << thy2 << "[" << *thy2 << "]"
- << (response.needsMoreRewriting() ?
- (response.needsFullRewriting() ?
- " FULL-REWRITING" : " MORE-REWRITING")
- : " DONE")
- << endl;
- if(rse.d_theory != thy2) {
- Debug("theory-rewrite") << "pre-rewritten from " << *rse.d_theory
- << " into " << *thy2
- << ", marking top-level and !done" << endl;
- rse.d_theory = thy2;
- done = false;
- // FIXME how to handle the "top-levelness" of a node that's
- // rewritten from theory T1 into T2, then back to T1 ?
- rse.d_topLevel = true;
- } else {
- done = response.isDone();
- }
- } while(!done);
- setPreRewriteCache(original, wasTopLevel, rse.d_node);
- } else {// is in pre-rewrite cache
- Debug("theory-rewrite") << "in pre-cache: " << cached << endl;
- rse.d_node = cached;
- Theory* thy2 = theoryOf(cached);
- if(rse.d_theory != thy2) {
- Debug("theory-rewrite") << "[cache-]pre-rewritten from "
- << *rse.d_theory << " into " << *thy2
- << ", marking top-level" << endl;
- rse.d_theory = thy2;
- rse.d_topLevel = true;
- }
- }
- }
-
- // children
- Node original = rse.d_node;
- bool wasTopLevel = rse.d_topLevel;
- Node cached = getPostRewriteCache(original, wasTopLevel);
-
- if(cached.isNull()) {
- unsigned nch = rse.d_nextChild++;
-
- if(nch == 0 &&
- rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- // this is an apply, so we have to push the operator
- TNode op = rse.d_node.getOperator();
- Debug("theory-rewrite") << "pushing operator " << op
- << " of " << rse.d_node << endl;
- rse.d_builder << op;
- }
-
- if(nch < rse.d_node.getNumChildren()) {
- Debug("theory-rewrite") << "pushing child " << nch
- << " of " << rse.d_node << endl;
- Node c = rse.d_node[nch];
- Theory* t = theoryOf(c);
- stack.push_back(RewriteStackElement(c, t, t != rse.d_theory));
- continue;// break out of this node, do its child
- }
-
- // incorporate the children's rewrites
- if(rse.d_node.getMetaKind() != kind::metakind::VARIABLE &&
- rse.d_node.getMetaKind() != kind::metakind::CONSTANT) {
- Debug("theory-rewrite") << "builder here is " << &rse.d_builder
- << " and it gets " << rse.d_node.getKind()
- << endl;
- rse.d_builder << rse.d_node.getKind();
- rse.d_node = Node(rse.d_builder);
- }
-
- // post-rewriting
- do {
- Debug("theory-rewrite") << "doing post-rewrite of "
- << rse.d_node << endl
- << " in " << *rse.d_theory
- << " topLevel==" << rse.d_topLevel << endl;
- RewriteResponse response =
- rse.d_theory->postRewrite(rse.d_node, rse.d_topLevel);
- rse.d_node = response.getNode();
- Assert(!rse.d_node.isNull(), "node illegally rewritten to null");
- Theory* thy2 = theoryOf(rse.d_node);
- Assert(thy2 != NULL, "node illegally rewritten to null theory");
- Debug("theory-rewrite") << "got back " << rse.d_node << " "
- << thy2 << "[" << *thy2 << "]"
- << (response.needsMoreRewriting() ?
- (response.needsFullRewriting() ?
- " FULL-REWRITING" : " MORE-REWRITING")
- : " DONE")
- << endl;
- if(rse.d_theory != thy2) {
- Debug("theory-rewrite") << "post-rewritten from " << *rse.d_theory
- << " into " << *thy2
- << ", marking top-level and !done" << endl;
- rse.d_theory = thy2;
- done = false;
- // FIXME how to handle the "top-levelness" of a node that's
- // rewritten from theory T1 into T2, then back to T1 ?
- rse.d_topLevel = true;
- } else {
- done = response.isDone();
- }
- if(response.needsFullRewriting()) {
- Debug("theory-rewrite") << "full-rewrite requested for node "
- << rse.d_node.getId() << ", invoking..."
- << endl;
- Node n = rewrite(rse.d_node, rse.d_topLevel);
- Debug("theory-rewrite") << "full-rewrite finished for node "
- << rse.d_node.getId() << ", got node "
- << n << " output." << endl;
- rse.d_node = n;
- done = true;
- }
- } while(!done);
-
- /* If extra-checking is on, do _another_ rewrite before putting
- * in the cache to make sure they are the same. This is
- * especially necessary if a theory post-rewrites something into
- * a term of another theory. */
- if(Debug.isOn("extra-checking") &&
- !Debug.isOn("$extra-checking:inside-rewrite")) {
- ScopedDebug d("$extra-checking:inside-rewrite");
- Node rewrittenAgain = rewrite(rse.d_node, rse.d_topLevel);
- Assert(rewrittenAgain == rse.d_node,
- "\nExtra-checking assumption failed, "
- "node is not completely rewritten.\n\n"
- "Original : %s\n"
- "Rewritten: %s\n"
- "Again : %s\n",
- original.toString().c_str(),
- rse.d_node.toString().c_str(),
- rewrittenAgain.toString().c_str());
- }
- setPostRewriteCache(original, wasTopLevel, rse.d_node);
-
- out = rse.d_node;
- } else {
- Debug("theory-rewrite") << "in post-cache: " << cached << endl;
- out = cached;
- Theory* thy2 = theoryOf(cached);
- if(rse.d_theory != thy2) {
- Debug("theory-rewrite") << "[cache-]post-rewritten from "
- << *rse.d_theory << " into " << *thy2 << endl;
- rse.d_theory = thy2;
- }
- }
-
- stack.pop_back();
- if(!stack.empty()) {
- Debug("theory-rewrite") << "asserting " << out << " to previous builder "
- << &stack.back().d_builder << endl;
- stack.back().d_builder << out;
- }
- } while(!stack.empty());
-
- Debug("theory-rewrite") << "DONE with theory rewriter." << endl;
- Debug("theory-rewrite") << "result is:" << endl << out << endl;
-
- return out;
-}/* TheoryEngine::rewrite(TNode in) */
-
Node TheoryEngine::getValue(TNode node) {
kind::MetaKind metakind = node.getMetaKind();
@@ -617,36 +297,16 @@ Node TheoryEngine::getValue(TNode node) {
return theoryOf(node)->getValue(node, this);
}/* TheoryEngine::getValue(TNode node) */
-
bool TheoryEngine::presolve() {
d_theoryOut.d_conflictNode = Node::null();
d_theoryOut.d_propagatedLiterals.clear();
try {
- /*
- d_builtin->presolve();
- if(!d_theoryOut.d_conflictNode.get().isNull()) {
- return true;
- }
- d_bool->presolve();
- if(!d_theoryOut.d_conflictNode.get().isNull()) {
- return true;
- }
- */
- d_uf->presolve();
- if(!d_theoryOut.d_conflictNode.get().isNull()) {
- return true;
- }
- d_arith->presolve();
- /*
- if(!d_theoryOut.d_conflictNode.get().isNull()) {
- return true;
- }
- d_arrays->presolve();
- if(!d_theoryOut.d_conflictNode.get().isNull()) {
- return true;
- }
- d_bv->presolve();
- */
+ for(unsigned i = 0; i < THEORY_LAST; ++ i) {
+ d_theoryTable[i]->presolve();
+ if(!d_theoryOut.d_conflictNode.get().isNull()) {
+ return true;
+ }
+ }
} catch(const theory::Interrupted&) {
Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl;
}
@@ -656,26 +316,20 @@ bool TheoryEngine::presolve() {
void TheoryEngine::notifyRestart() {
- /*
- d_builtin->notifyRestart();
- d_bool->notifyRestart();
- */
- d_uf->notifyRestart();
- /*
- d_arith->notifyRestart();
- d_arrays->notifyRestart();
- d_bv->notifyRestart();
- */
+ for(unsigned i = 0; i < THEORY_LAST; ++ i) {
+ if (d_theoryTable[i]) {
+ d_theoryTable[i]->notifyRestart();
+ }
+ }
}
void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
- d_builtin->staticLearning(in, learned);
- d_bool->staticLearning(in, learned);
- d_uf->staticLearning(in, learned);
- d_arith->staticLearning(in, learned);
- d_arrays->staticLearning(in, learned);
- d_bv->staticLearning(in, learned);
+ for(unsigned i = 0; i < THEORY_LAST; ++ i) {
+ if (d_theoryTable[i]) {
+ d_theoryTable[i]->staticLearning(in, learned);
+ }
+ }
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback