Ho Lambda Lifting (#1116)

* Do lambda lifting in term formula removal pass. Set option in SMT engine related to higher-order.

* Better documentation

1 files changed, 28 insertions, 16 deletions

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index a008868c7..0cd166c87 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -101,40 +101,52 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
 
   // If an ITE, replace it
   TypeNode nodeType = node.getType();
+  Node skolem;
+  Node newAssertion;
   if(node.getKind() == kind::ITE) {
     if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
-      Node skolem;
       // Make the skolem to represent the ITE
       skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal");
 
       // The new assertion
-      Node newAssertion =
+      newAssertion =
         nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
                             skolem.eqNode(node[2]));
-      Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
-
-      // Attach the skolem
-      d_iteCache.insert(cacheKey, skolem);
-
-      // Remove ITEs from the new assertion, rewrite it and push it to the output
-      newAssertion = run(newAssertion, output, iteSkolemMap, false, false);
-
-      iteSkolemMap[skolem] = output.size();
-      output.push_back(newAssertion);
+    }
+  }
+  //if a lambda, do lambda-lifting
+  if( node.getKind() == kind::LAMBDA && !inQuant ){
+    // Make the skolem to represent the ITE
+    skolem = nodeManager->mkSkolem("lambdaF", nodeType, "a function introduced due to term-level lambda removal");
 
-      // The representation is now the skolem
-      return skolem;
+    // The new assertion
+    std::vector< Node > children;
+    // bound variable list
+    children.push_back( node[0] );
+    // body
+    std::vector< Node > skolem_app_c;
+    skolem_app_c.push_back( skolem );
+    for( unsigned i=0; i<node[0].getNumChildren(); i++ ){
+      skolem_app_c.push_back( node[0][i] );
     }
+    Node skolem_app = nodeManager->mkNode( kind::APPLY_UF, skolem_app_c );
+    children.push_back( skolem_app.eqNode( node[1] ) );
+    // axiom defining skolem
+    newAssertion = nodeManager->mkNode( kind::FORALL, children );
   }
   //if a non-variable Boolean term, replace it
   if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){
-    Node skolem;
+
     // Make the skolem to represent the Boolean term
     //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal");
     skolem = nodeManager->mkBooleanTermVariable();
 
     // The new assertion
-    Node newAssertion = skolem.eqNode( node );
+    newAssertion = skolem.eqNode( node );
+  }
+
+  // if we introduced a skolem
+  if( !skolem.isNull() ){
     Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
 
     // Attach the skolem