* Reversing commit r4258 (which disabled failing regressions). Fixed the problem so they're no longer failing (in the quantifiers rewriter). Resolves bug #381.

* Added LAMBDA kind and type rule, and Node::isClosure().

(this commit was certified error- and warning-free by the test-and-commit script.)

7 files changed, 41 insertions, 15 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 0ce042654..7108ba74a 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -453,6 +453,14 @@ public:
     return getMetaKind() == kind::metakind::VARIABLE;
   }
 
+  inline bool isClosure() const {
+    assertTNodeNotExpired();
+    return getKind() == kind::LAMBDA ||
+           getKind() == kind::FORALL ||
+           getKind() == kind::EXISTS ||
+           getKind() == kind::REWRITE_RULE;
+  }
+
   /**
    * Returns the unique id of this node
    * @return the ud
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 48fe4d84a..c4c3435a2 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -298,6 +298,8 @@ variable BOUND_VARIABLE "bound variable"
 variable SKOLEM "skolem var"
 operator TUPLE 1: "a tuple"
 
+operator LAMBDA 2 "lambda"
+
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
     ::CVC4::TypeConstantHashFunction \
@@ -338,6 +340,7 @@ typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
 typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
+typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 
 constant SUBTYPE_TYPE \
     ::CVC4::Predicate \
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 68d9e8702..95ede1c46 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -145,6 +145,24 @@ public:
   }
 };/* class StringConstantTypeRule */
 
+class LambdaTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    if( n[0].getType(check) != nodeManager->boundVarListType() ) {
+      std::stringstream ss;
+      ss << "expected a bound var list for LAMBDA expression, got `"
+         << n[0].getType().toString() << "'";
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+    std::vector<TypeNode> argTypes;
+    for(TNode::iterator i = n[0].begin(); i != n[0].end(); ++i) {
+      argTypes.push_back((*i).getType());
+    }
+    TypeNode rangeType = n[1].getType(check);
+    return nodeManager->mkFunctionType(argTypes, rangeType);
+  }
+};/* class LambdaTypeRule */
+
 class SortProperties {
 public:
   inline static bool isWellFounded(TypeNode type) {
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index e928010b6..b0728de29 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -473,7 +473,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
         for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
           //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){
           terms.push_back( body[0][i] );
-          subs.push_back( NodeManager::currentNM()->mkSkolem( body[0][i].getType() ) );
+          subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) );
         }
         args.insert( args.end(), subs.begin(), subs.end() );
       }else{
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cc74e3e76..a73d42a31 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -14,11 +14,11 @@
  ** \brief Implementation of term databse class
  **/
 
- #include "theory/quantifiers/term_database.h"
- #include "theory/quantifiers_engine.h"
- #include "theory/uf/theory_uf_instantiator.h"
- #include "theory/theory_engine.h"
- #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/first_order_model.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h
index 605324b20..f03fba73a 100644
--- a/src/theory/rewriterules/theory_rewriterules_type_rules.h
+++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h
@@ -60,7 +60,7 @@ public:
     }
     return nodeManager->booleanType();
   }
-};/* class RewriterulesTypeRule */
+};/* class RewriteRuleTypeRule */
 
 
 class RRRewriteTypeRule {
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 8880bf3ca..38cc59125 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -28,16 +28,13 @@ TESTS =	\
 	opisavailable-12.smt2 \
 	ricart-agrawala6.smt2 \
 	set8.smt2 \
+	smtlib384a03.smt2 \
+	smtlib46f14a.smt2 \
+	smtlibf957ea.smt2 \
+	gauss_init_0030.fof.smt2 \
+	piVC_5581bd.smt2 \
 	set3.smt2
 
-# removed because failing
-#	smtlib384a03.smt2 \
-#	smtlib46f14a.smt2 \
-#	smtlibf957ea.smt2 \
-#	gauss_init_0030.fof.smt2 \
-#	piVC_5581bd.smt2 \
-#
-
 # removed because it now reports unknown
 #	symmetric_unsat_7.smt2 \
 #