diff options
-rw-r--r-- | src/prop/prop_engine.cpp | 6 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 5 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 17 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 5 | ||||
-rw-r--r-- | src/util/ite_removal.cpp | 14 | ||||
-rw-r--r-- | src/util/ite_removal.h | 11 |
7 files changed, 37 insertions, 26 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 212a99a8e..03746c9b2 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -91,15 +91,11 @@ PropEngine::~PropEngine() { delete d_satSolver; } -void PropEngine::processAssertionsStart() { - d_theoryEngine->preprocessStart(); -} - void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable - d_cnfStream->convertAndAssert(d_theoryEngine->preprocess(node), false, false); + d_cnfStream->convertAndAssert(node, false, false); } void PropEngine::assertLemma(TNode node, bool negated, bool removable) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 3d114db3a..9e49cf3f1 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -174,11 +174,6 @@ public: void shutdown() { } /** - * Signal that a new round of assertions is ready so we can notify the theory engine - */ - void processAssertionsStart(); - - /** * Converts the given formula to CNF and assert the CNF to the SAT solver. * The formula is asserted permanently for the current context. * @param node the formula to assert diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4b3410cf7..81af14031 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -122,6 +122,10 @@ class SmtEnginePrivate { /** Assertions to push to sat */ vector<Node> d_assertionsToCheck; + /** Map from skolem variables to index in d_assertionsToCheck containing + * corresponding introduced Boolean ite */ + IteSkolemMap d_iteSkolemMap; + /** The top level substitutions */ theory::SubstitutionMap d_topLevelSubstitutions; @@ -696,8 +700,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHas void SmtEnginePrivate::removeITEs() { Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl; - // Remove all of the ITE occurances and normalize - RemoveITE::run(d_assertionsToCheck); + // Remove all of the ITE occurrences and normalize + RemoveITE::run(d_assertionsToCheck, d_iteSkolemMap); for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { d_assertionsToCheck[i] = theory::Rewriter::rewrite(d_assertionsToCheck[i]); } @@ -1051,13 +1055,20 @@ void SmtEnginePrivate::processAssertions() { } } - d_smt.d_propEngine->processAssertionsStart(); + // Call the theory preprocessors + d_smt.d_theoryEngine->preprocessStart(); + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]); + } + + // TODO: send formulas and iteSkolemMap to decision engine // Push the formula to SAT for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); } d_assertionsToCheck.clear(); + d_iteSkolemMap.clear(); } void SmtEnginePrivate::addFormula(TNode n) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d5616221d..a7e1f0cd7 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -50,7 +50,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_possiblePropagations(), d_hasPropagated(context), d_inConflict(context, false), - d_sharedTermsExist(context, false), + d_sharedTermsExist(logicInfo.isSharingEnabled()), d_hasShutDown(false), d_incomplete(context, false), d_sharedLiteralsIn(context), @@ -94,8 +94,6 @@ void TheoryEngine::preRegister(TNode preprocessed) { if (multipleTheories) { // Collect the shared terms if there are multipe theories NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed); - // Mark the multiple theories flag - d_sharedTermsExist = true; } } @@ -627,7 +625,6 @@ void TheoryEngine::assertFact(TNode node) TNode atom = negated ? node[0] : node; Theory* theory = theoryOf(atom); - //TODO: there is probably a bug here if shared terms start to exist after some asseritons have been processed if (d_sharedTermsExist) { // If any shared terms, notify the theories diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5dfc4c36c..e353850aa 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -259,7 +259,7 @@ class TheoryEngine { /** * Does the context contain terms shared among multiple theories. */ - context::CDO<bool> d_sharedTermsExist; + bool d_sharedTermsExist; /** * Explain the equality literals and push all the explaining literals @@ -437,8 +437,9 @@ class TheoryEngine { // Remove the ITEs and assert to prop engine std::vector<Node> additionalLemmas; + IteSkolemMap iteSkolemMap; additionalLemmas.push_back(node); - RemoveITE::run(additionalLemmas); + RemoveITE::run(additionalLemmas, iteSkolemMap); additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); d_propEngine->assertLemma(additionalLemmas[0], negated, removable); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index dfa6e3cba..9d2524170 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -30,13 +30,15 @@ namespace CVC4 { struct IteRewriteAttrTag {}; typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr; -void RemoveITE::run(std::vector<Node>& output) { +void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap) +{ for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { - output[i] = run(output[i], output); + output[i] = run(output[i], output, iteSkolemMap); } } -Node RemoveITE::run(TNode node, std::vector<Node>& output) { +Node RemoveITE::run(TNode node, std::vector<Node>& output, + IteSkolemMap& iteSkolemMap) { // Current node Debug("ite") << "removeITEs(" << node << ")" << endl; @@ -67,7 +69,9 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output) { nodeManager->setAttribute(node, IteRewriteAttr(), skolem); // Remove ITEs from the new assertion, rewrite it and push it to the output - output.push_back(run(newAssertion, output)); + newAssertion = run(newAssertion, output, iteSkolemMap); + iteSkolemMap[skolem] = output.size(); + output.push_back(newAssertion); // The representation is now the skolem return skolem; @@ -82,7 +86,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output) { } // Remove the ITEs from the children for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = run(*it, output); + Node newChild = run(*it, output, iteSkolemMap); somethingChanged |= (newChild != *it); newChildren.push_back(newChild); } diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h index bfb0d4ac8..248ce4efa 100644 --- a/src/util/ite_removal.h +++ b/src/util/ite_removal.h @@ -26,19 +26,26 @@ namespace CVC4 { +typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap; + class RemoveITE { public: /** * Removes the ITE nodes by introducing skolem variables. All additional assertions are pushed into assertions. + * iteSkolemMap contains a map from introduced skolem variables to the index in assertions containing the new + * Boolean ite created in conjunction with that skolem variable. */ - static void run(std::vector<Node>& assertions); + static void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap); /** * Removes the ITE from the node by introducing skolem variables. All additional assertions are pushed into assertions. + * iteSkolemMap contains a map from introduced skolem variables to the index in assertions containing the new + * Boolean ite created in conjunction with that skolem variable. */ - static Node run(TNode node, std::vector<Node>& additionalAssertions); + static Node run(TNode node, std::vector<Node>& additionalAssertions, + IteSkolemMap& iteSkolemMap); };/* class RemoveTTE */ |