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.

2 files changed, 18 insertions, 7 deletions

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 */