From 7342d1ca87397f3d5beb2c04b819243303e69a7c Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Tue, 5 Jul 2011 16:21:50 +0000 Subject: updated preprocessing and rewriting input equalities into inequalities for LRA --- src/theory/theory_engine.cpp | 208 ++++++++++++++++++------------------------- 1 file changed, 87 insertions(+), 121 deletions(-) (limited to 'src/theory/theory_engine.cpp') diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index db22d8981..fa885590b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -29,6 +29,8 @@ #include "theory/rewriter.h" #include "theory/theory_traits.h" +#include "util/ite_removal.h" + using namespace std; using namespace CVC4; @@ -46,9 +48,6 @@ typedef CVC4::expr::CDAttribute RegisteredAttr; struct PreRegisteredAttrTag {}; typedef expr::Attribute PreRegistered; -struct IteRewriteAttrTag {}; -typedef expr::Attribute IteRewriteAttr; - }/* CVC4::theory namespace */ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { @@ -125,11 +124,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { // traversing a DAG as a tree and that can really blow up @CB if(! n.getAttribute(RegisteredAttr())) { n.setAttribute(RegisteredAttr(), true); - if (n.getKind() == kind::EQUAL) { - d_engine->theoryOf(n[0])->registerTerm(n); - } else { - d_engine->theoryOf(n)->registerTerm(n); - } + d_engine->theoryOf(n)->registerTerm(n); } } }/* Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr()) */ @@ -167,24 +162,13 @@ TheoryEngine::~TheoryEngine() { delete d_sharedTermManager; } -struct preprocess_stack_element { +struct preregister_stack_element { TNode node; bool children_added; - preprocess_stack_element(TNode node) + preregister_stack_element(TNode node) : node(node), children_added(false) {} };/* struct preprocess_stack_element */ -Node TheoryEngine::preprocess(TNode node) { - // Make sure the node is type-checked first (some rewrites depend on - // typechecking having succeeded to be safe). - if(Options::current()->typeChecking) { - node.getType(true); - } - // Remove ITEs and rewrite the node - Node preprocessed = Rewriter::rewrite(removeITEs(node)); - return preprocessed; -} - void TheoryEngine::preRegister(TNode preprocessed) { // If we are pre-registered already we are done if (preprocessed.getAttribute(PreRegistered())) { @@ -192,10 +176,10 @@ void TheoryEngine::preRegister(TNode preprocessed) { } // Do a topological sort of the subexpressions and preregister them - vector toVisit; + vector toVisit; toVisit.push_back((TNode) preprocessed); while (!toVisit.empty()) { - preprocess_stack_element& stackHead = toVisit.back(); + preregister_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 @@ -208,22 +192,11 @@ void TheoryEngine::preRegister(TNode preprocessed) { if(d_logic == "QF_AX") { d_theoryTable[theory::THEORY_ARRAY]->preRegisterTerm(current); } else { - TheoryId theoryLHS = Theory::theoryOf(current[0]); + Theory* theory = theoryOf(current); + TheoryId theoryLHS = theory->getId(); Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl; markActive(theoryLHS); - d_theoryTable[theoryLHS]->preRegisterTerm(current); -// TheoryId theoryRHS = Theory::theoryOf(current[1]); -// if (theoryLHS != theoryRHS) { -// markActive(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) { -// markActive(typeTheory); -// d_theoryTable[typeTheory]->preRegisterTerm(current); -// Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; -// } + theory->preRegisterTerm(current); } } else { TheoryId theory = Theory::theoryOf(current); @@ -297,68 +270,6 @@ void TheoryEngine::propagate() { CVC4_FOR_EACH_THEORY; } -/* Our goal is to tease out any ITE's sitting under a theory operator. */ -Node TheoryEngine::removeITEs(TNode node) { - Debug("ite") << "removeITEs(" << node << ")" << endl; - - /* The result may be cached already */ - Node cachedRewrite; - NodeManager *nodeManager = NodeManager::currentNM(); - if(nodeManager->getAttribute(node, theory::IteRewriteAttr(), cachedRewrite)) { - Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl; - return cachedRewrite.isNull() ? Node(node) : cachedRewrite; - } - - if(node.getKind() == kind::ITE){ - Assert( node.getNumChildren() == 3 ); - TypeNode nodeType = node.getType(); - if(!nodeType.isBoolean()){ - Node skolem = nodeManager->mkVar(nodeType); - Node newAssertion = - nodeManager->mkNode(kind::ITE, - node[0], - nodeManager->mkNode(kind::EQUAL, skolem, node[1]), - nodeManager->mkNode(kind::EQUAL, skolem, node[2])); - nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem); - - Debug("ite") << "removeITEs([" << node.getId() << "," << node << "," << nodeType << "])" - << "->" - << "[" << newAssertion.getId() << "," << newAssertion << "]" - << endl; - - Node preprocessed = preprocess(newAssertion); - d_propEngine->assertFormula(preprocessed); - - return skolem; - } - } - vector newChildren; - bool somethingChanged = false; - if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { - // Make sure to push operator or it will be missing in new - // (reformed) node. This was crashing on the very simple input - // "(f (ite c 0 1))" - newChildren.push_back(node.getOperator()); - } - for(TNode::const_iterator it = node.begin(), end = node.end(); - it != end; - ++it) { - Node newChild = removeITEs(*it); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } - - if(somethingChanged) { - cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren); - nodeManager->setAttribute(node, theory::IteRewriteAttr(), cachedRewrite); - return cachedRewrite; - } else { - nodeManager->setAttribute(node, theory::IteRewriteAttr(), Node::null()); - return node; - } -} - - Node TheoryEngine::getValue(TNode node) { kind::MetaKind metakind = node.getMetaKind(); // special case: prop engine handles boolean vars @@ -451,36 +362,91 @@ bool TheoryEngine::hasRegisterTerm(TheoryId th) const { } } -Node TheoryEngine::simplify(TNode in, theory::Substitutions& outSubstitutions) { - SimplifyCache::Scope cache(d_simplifyCache, in); - if(cache) { - outSubstitutions.insert(outSubstitutions.end(), - cache.get().second.begin(), - cache.get().second.end()); - return cache.get().first; - } +theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) { + TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; + Debug("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl; + Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitionOut); + Debug("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << std::endl; + return solveStatus; +} + +struct preprocess_stack_element { + TNode node; + bool children_added; + preprocess_stack_element(TNode node) + : node(node), children_added(false) {} +};/* struct preprocess_stack_element */ - size_t prevSize = outSubstitutions.size(); - TNode atom = in.getKind() == kind::NOT ? in[0] : in; +Node TheoryEngine::preprocess(TNode assertion) { + + Debug("theory") << "TheoryEngine::preprocess(" << assertion << ")" << std::endl; + + // Do a topological sort of the subexpressions and substitute them + vector toVisit; + toVisit.push_back(assertion); + + while (!toVisit.empty()) + { + // The current node we are processing + preprocess_stack_element& stackHead = toVisit.back(); + TNode current = stackHead.node; - theory::Theory* theory = theoryOf(atom); + Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << std::endl; - Debug("simplify") << push << "simplifying " << in << " to " << theory->identify() << std::endl; - Node n = theory->simplify(in, outSubstitutions); - Debug("simplify") << "got from " << theory->identify() << " : " << n << std::endl << pop; + // If node already in the cache we're done, pop from the stack + NodeMap::iterator find = d_atomPreprocessingCache.find(current); + if (find != d_atomPreprocessingCache.end()) { + toVisit.pop_back(); + continue; + } - atom = n.getKind() == kind::NOT ? n[0] : n; + // If this is an atom, we preprocess it with the theory + if (Theory::theoryOf(current) != THEORY_BOOL) { + d_atomPreprocessingCache[current] = theoryOf(current)->preprocess(current); + continue; + } - if(atom.getKind() == kind::EQUAL) { - theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType()); - Debug("simplify") << push << "simplifying " << n << " to " << typeTheory << std::endl; - n = d_theoryTable[typeTheory]->simplify(n, outSubstitutions); - Debug("simplify") << "got from " << d_theoryTable[typeTheory]->identify() << " : " << n << std::endl << pop; + // Not yet substituted, so process + if (stackHead.children_added) { + // Children have been processed, so substitute + NodeBuilder<> builder(current.getKind()); + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << current.getOperator(); + } + for (unsigned i = 0; i < current.getNumChildren(); ++ i) { + Assert(d_atomPreprocessingCache.find(current[i]) != d_atomPreprocessingCache.end()); + builder << d_atomPreprocessingCache[current[i]]; + } + // Mark the substitution and continue + Node result = builder; + Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << std::endl; + d_atomPreprocessingCache[current] = result; + toVisit.pop_back(); + } else { + // Mark that we have added the children if any + if (current.getNumChildren() > 0) { + 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; + NodeMap::iterator childFind = d_atomPreprocessingCache.find(childNode); + if (childFind == d_atomPreprocessingCache.end()) { + toVisit.push_back(childNode); + } + } + } else { + // No children, so we're done + Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << std::endl; + d_atomPreprocessingCache[current] = current; + toVisit.pop_back(); + } + } } - cache(std::make_pair(n, theory::Substitutions(outSubstitutions.begin() + prevSize, outSubstitutions.end()))); - return n; + // Return the substituted version + return d_atomPreprocessingCache[assertion]; } + }/* CVC4 namespace */ -- cgit v1.2.3