Ho Lambda Lifting (#1116)

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

* Better documentation

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0999806537aaadc9390d45a1eb0dced788e7affe..5c37861089926766c2c4bed52ed6ce5b9a8acfa4 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1762,6 +1762,12 @@ void SmtEngine::setDefaults() {
       options::prenexQuant.set( quantifiers::PRENEX_QUANT_NONE );
     }
   }
+  if( options::ufHo() ){
+    //if higher-order, then current variants of model-based instantiation cannot be used
+    if( options::mbqiMode()!=quantifiers::MBQI_NONE ){
+      options::mbqiMode.set( quantifiers::MBQI_NONE );
+    }
+  }
   if( options::mbqiMode()==quantifiers::MBQI_ABS ){
     if( !d_logic.isPure(THEORY_UF) ){
       //MBQI_ABS is only supported in pure quantified UF

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index a008868c766d2b2987fc2f43e0b324c6c14faedb..0cd166c87424bb53b92126187454636bb3df29f4 100644 (file)
--- 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

diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 854ddc61ec6ec0377f0f7eecb9c94af37538ab4a..48b1c36c5a65c57b85add1a9dba0c3efc5259eb9 100644 (file)
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -49,23 +49,47 @@ public:
   ~RemoveTermFormulas();
 
   /**
-   * Removes the ITE nodes by introducing skolem variables. All
-   * additional assertions are pushed into assertions. iteSkolemMap
+   * By introducing skolem variables, this function removes all occurrences of:
+   * (1) term ITEs 
+   * (2) terms of type Boolean that are not Boolean term variables, and
+   * (3) lambdas
+   * from assertions.
+   * 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
+   * assertions containing the new definition created in conjunction
    * with that skolem variable.
    *
+   * As an example of (1): 
+   *   f( (ite C 0 1)) = 2
+   *   becomes
+   *   f( k ) = 2 ^ ite( C, k=0, k=1 )
+   *
+   * As an example of (2):
+   *   g( (and C1 C2) ) = 3
+   *   becomes
+   *   g( k ) = 3 ^ ( k <=> (and C1 C2) )
+   *
+   * As an example of (3): 
+   *   (lambda x. t[x]) = f
+   *   becomes
+   *   (forall x. k(x) = t[x]) ^ k = f
+   * where k is a fresh skolem. This is sometimes called "lambda lifting"
+   *
    * With reportDeps true, report reasoning dependences to the proof
    * manager (for unsat cores).
    */
   void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false);
 
   /**
-   * Removes the ITE from the node by introducing skolem
-   * variables. All additional assertions are pushed into
+   * Removes terms of the form (1), (2), (3) described above from node.
+   * 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.
+   *
+   * inQuant is whether we are processing node in the body of quantified formula
+   * inTerm is whether we are are processing node in a "term" position, that is, it is a subterm
+   *        of a parent term that is not a Boolean connective.
    */
   Node run(TNode node, std::vector<Node>& additionalAssertions,
            IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm);