* Reversing commit r4258 (which disabled failing regressions). Fixed the problem...

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

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

diff --git a/src/expr/node.h b/src/expr/node.h
index 0ce0426544efb7cf20362cfe22d160bfe70ba16a..7108ba74a236937a9e0b90a3b33a42fe370ed3cd 100644 (file)
--- 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 48fe4d84ab0c8823b5669c1b3b88d739e85956dd..c4c3435a2219c158204b34be6119867723365e2d 100644 (file)
--- 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 68d9e8702a52568064af0ea3085d0f6d2a36c29d..95ede1c4666491a3afcf9a277a89f90567bff006 100644 (file)
--- 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 e928010b6413eb9c20f01d2548b483e99eb1b55a..b0728de29c0cd2e5b1c95979985521dd0aa4b9a2 100644 (file)
--- 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 cc74e3e76382db113c92d0333175be7875c525bd..a73d42a3175659314d0b6fcd409a222ef8e64fce 100644 (file)
--- 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 605324b201271a4a001e1103c510917a9d649128..f03fba73af4680f1f1e291357b558631ab864246 100644 (file)
--- 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 8880bf3ca23e6d9e6020528d34f32646dc775aa8..38cc59125e13d15a1e494cc69b805ea14d9db842 100644 (file)
--- 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 \
 #