Add isConst check for lambda expressions. (#1084)

Add isConst check for lambda expressions by conversions to and from an Array representation where isConst is implemented. This enables check-model to succeed on higher-order benchmarks. Change the builtin rewriter for lambda to attempt to put lambdas into constant form. Update regression.

2 files changed, 24 insertions, 0 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 33f057274..85f5e3c75 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -83,6 +83,12 @@ struct NVReclaim {
 
 } // namespace
 
+namespace attr {
+  struct LambdaBoundVarListTag { };
+}/* CVC4::attr namespace */
+
+// attribute that stores the canonical bound variable list for function types
+typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAttr;
 
 NodeManager::NodeManager(ExprManager* exprManager) :
   d_options(new Options()),
@@ -692,6 +698,21 @@ Node* NodeManager::mkBoundVarPtr(const std::string& name,
   return n;
 }
 
+Node NodeManager::getBoundVarListForFunctionType( TypeNode tn ) {
+  Assert( tn.isFunction() );
+  Node bvl = tn.getAttribute(LambdaBoundVarListAttr());
+  if( bvl.isNull() ){
+    std::vector< Node > vars;
+    for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){
+      vars.push_back( NodeManager::currentNM()->mkBoundVar( tn[i] ) );
+    }
+    bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, vars );
+    Trace("functions") << "Make standard bound var list " << bvl << " for " << tn << std::endl;
+    tn.setAttribute(LambdaBoundVarListAttr(),bvl);
+  }
+  return bvl;
+}
+
 Node NodeManager::mkVar(const TypeNode& type, uint32_t flags) {
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index b1b0bc974..d5d296579 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -491,6 +491,9 @@ public:
   Node mkBoundVar(const TypeNode& type);
   Node* mkBoundVarPtr(const TypeNode& type);
 
+  /** get the canonical bound variable list for function type tn */
+  static Node getBoundVarListForFunctionType( TypeNode tn );
+
   /**
    * Optional flags used to control behavior of NodeManager::mkSkolem().
    * They should be composed with a bitwise OR (e.g.,