From 97555307af3415d6fbbac3fc9dccdafec51056b7 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 30 Apr 2012 14:42:28 +0000 Subject: [PATCH] Added map from skolem variables to new ite formulas in ite removal. d_sharedTermsExist is now set based on logicInfo instead of dynamically when shared terms are found. --- src/prop/prop_engine.cpp | 6 +----- src/prop/prop_engine.h | 5 ----- src/smt/smt_engine.cpp | 17 ++++++++++++++--- src/theory/theory_engine.cpp | 5 +---- src/theory/theory_engine.h | 5 +++-- src/util/ite_removal.cpp | 14 +++++++++----- 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 @@ -173,11 +173,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. 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 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_mapprocessAssertionsStart(); + // 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::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 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 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 IteRewriteAttr; -void RemoveITE::run(std::vector& output) { +void RemoveITE::run(std::vector& 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& output) { +Node RemoveITE::run(TNode node, std::vector& output, + IteSkolemMap& iteSkolemMap) { // Current node Debug("ite") << "removeITEs(" << node << ")" << endl; @@ -67,7 +69,9 @@ Node RemoveITE::run(TNode node, std::vector& 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& 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 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& assertions); + static void run(std::vector& 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& additionalAssertions); + static Node run(TNode node, std::vector& additionalAssertions, + IteSkolemMap& iteSkolemMap); };/* class RemoveTTE */ -- 2.30.2