From 00785f2b65eb9dfdfbfcd8b58b0cc57255919c31 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 16 Mar 2017 14:05:23 -0500
Subject: [PATCH] Minor fixes, always expand applications of lambdas at
 preprocess.

---
 src/parser/smt2/Smt2.g                        |  7 +-
 src/smt/smt_engine.cpp                        | 68 +++++++++++--------
 test/regress/regress0/datatypes/Makefile.am   |  3 +-
 .../datatypes/dt-match-pat-param-2.6.smt2     | 14 ++++
 4 files changed, 59 insertions(+), 33 deletions(-)
 create mode 100644 test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index bb7ac9fb8..c52f2ad51 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2074,10 +2074,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
            if( !type.isConstructor() ){
              PARSER_STATE->parseError("Pattern must be application of a constructor or a variable.");
            }
-           //TODO
-           //if( Datatype::datatypeOf(f).isParametric() ){
-           //  type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType());
-           //}
+           if( Datatype::datatypeOf(f).isParametric() ){
+             type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType());
+           }
            match_ptypes = ((ConstructorType)type).getArgTypes();
          }
          //arguments
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 306843c81..998967c5e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2305,7 +2305,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
       }
 
       // otherwise expand it
-      bool doExpand = ( k == kind::APPLY && n.getOperator().getKind() != kind::LAMBDA );
+      bool doExpand = k == kind::APPLY;
       if( !doExpand ){
         if( options::macrosQuant() ){
           //expand if we have inferred an operator corresponds to a defined function
@@ -2313,35 +2313,47 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
         }
       }
       if (doExpand) {
-        // application of a user-defined symbol
-        TNode func = n.getOperator();
-        SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(func);
-        if(i == d_smt.d_definedFunctions->end()) {
-          throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'");
-        }
-        DefinedFunction def = (*i).second;
-        vector<Node> formals = def.getFormals();
-
-        if(Debug.isOn("expand")) {
-          Debug("expand") << "found: " << n << endl;
-          Debug("expand") << " func: " << func << endl;
-          string name = func.getAttribute(expr::VarNameAttr());
-          Debug("expand") << "     : \"" << name << "\"" << endl;
-        }
-        if(Debug.isOn("expand")) {
-          Debug("expand") << " defn: " << def.getFunction() << endl
-                          << "       [";
-          if(formals.size() > 0) {
-            copy( formals.begin(), formals.end() - 1,
-                  ostream_iterator<Node>(Debug("expand"), ", ") );
-            Debug("expand") << formals.back();
+        vector<Node> formals;
+        TNode fm;
+        if( n.getOperator().getKind() == kind::LAMBDA ){
+          TNode op = n.getOperator();
+          // lambda
+          for( unsigned i=0; i<op[0].getNumChildren(); i++ ){
+            formals.push_back( op[0][i] );
+          }
+          fm = op[1];
+        }else{
+          // application of a user-defined symbol
+          TNode func = n.getOperator();
+          SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(func);
+          if(i == d_smt.d_definedFunctions->end()) {
+            throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'");
+          }
+          DefinedFunction def = (*i).second;
+          formals = def.getFormals();
+
+          if(Debug.isOn("expand")) {
+            Debug("expand") << "found: " << n << endl;
+            Debug("expand") << " func: " << func << endl;
+            string name = func.getAttribute(expr::VarNameAttr());
+            Debug("expand") << "     : \"" << name << "\"" << endl;
+          }
+          if(Debug.isOn("expand")) {
+            Debug("expand") << " defn: " << def.getFunction() << endl
+                            << "       [";
+            if(formals.size() > 0) {
+              copy( formals.begin(), formals.end() - 1,
+                    ostream_iterator<Node>(Debug("expand"), ", ") );
+              Debug("expand") << formals.back();
+            }
+            Debug("expand") << "]" << endl
+                            << "       " << def.getFunction().getType() << endl
+                            << "       " << def.getFormula() << endl;
           }
-          Debug("expand") << "]" << endl
-                          << "       " << def.getFunction().getType() << endl
-                          << "       " << def.getFormula() << endl;
-        }
 
-        TNode fm = def.getFormula();
+          fm = def.getFormula();
+        }
+        
         Node instance = fm.substitute(formals.begin(), formals.end(),
                                       n.begin(), n.end());
         Debug("expand") << "made : " << instance << endl;
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 24c289650..d9db39b40 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -78,7 +78,8 @@ TESTS =	\
 	dt-2.6.smt2  \
 	dt-sel-2.6.smt2 \
 	dt-param-2.6.smt2 \
-	dt-color-2.6.smt2
+	dt-color-2.6.smt2 \
+	dt-match-pat-param-2.6.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 b/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2
new file mode 100644
index 000000000..e2f4a779b
--- /dev/null
+++ b/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --lang=smt2.6
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ( ( Tree 0) ( TreeList 0) ) (
+ ( ( node ( value Int ) ( children TreeList) ))
+( ( empty ) ( insert ( head Tree) ( tail TreeList)) )
+))
+
+
+(declare-fun t () TreeList)
+(assert (<= 100 (match t ((empty (- 1)) ((insert x1 x2) (value x1))))))
+
+(check-sat)
-- 
2.30.2