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.

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 212a99a8e39b8b91afeea30ec0d95582b6fb333d..03746c9b29f62bf6af937506bf0f270e6c248e49 100644 (file)
--- 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 3d114db3a4310baa0024a14aea2202dc5cedc312..9e49cf3f10b8fb580d61f485882d877b8ec44491 100644 (file)
--- 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 4b3410cf7993e968e0ba91b07a8766f2588683d8..81af14031744c8c3f3cfd4175862d199fa899348 100644 (file)
--- 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 d5616221df0826fdacad6af354f8c6ca5d6c3563..a7e1f0cd7a87c595b571c41e53a72dabb2a2fafb 100644 (file)
--- 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 5dfc4c36c32d3344ada35580f6acf10ba329ea3e..e353850aa010edbc9d49ec96356dbdd7643ea69a 100644 (file)
--- 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 dfa6e3cba7f70f198bbde24baa1596afa72c3c96..9d25241704efe81dd6632483f832b6b1c75fdc79 100644 (file)
--- 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 bfb0d4ac81767920a1fcbe709acac43576360bda..248ce4efa83731793879c153c4152175a3e5aab0 100644 (file)
--- 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 */