From 1af890ef4fed0c0151dc2ab954dce0121dd283d8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 17 May 2018 16:31:30 -0500
Subject: [PATCH] Catch type errors in sygus grammars for lambda (define-fun)
 constructors (#1937)

---
 .../quantifiers/sygus/term_database_sygus.cpp | 34 +++++++++++++++----
 .../quantifiers/sygus/term_database_sygus.h   |  7 +++-
 2 files changed, 34 insertions(+), 7 deletions(-)

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index b530edeaa..85ff5c896 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -685,6 +685,14 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
         }else{
           // no arguments to synthesis functions
         }
+        // register connected types
+        for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+        {
+          for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+          {
+            registerSygusType(getArgType(dt[i], j));
+          }
+        }
         //iterate over constructors
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
           Expr sop = dt[i].getSygusOp();
@@ -701,6 +709,26 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
             d_consts[tn][n] = i;
             d_arg_const[tn][i] = n;
           }
+          else if (sop.getKind() == LAMBDA)
+          {
+            // do type checking
+            Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
+            for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+            {
+              TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
+              TypeNode cbt = sygusToBuiltinType(ct);
+              TypeNode lat = TypeNode::fromType(sop[0][j].getType());
+              CVC4_CHECK(cbt.isSubtypeOf(lat))
+                  << "In sygus datatype " << dt.getName()
+                  << ", argument to a lambda constructor is not " << lat
+                  << std::endl;
+            }
+          }
+          // TODO (as part of #1170): we still do not properly catch type
+          // errors in sygus grammars for arguments of builtin operators.
+          // The challenge is that we easily ask for expected argument types of
+          // builtin operators e.g. PLUS. Hence the call to mkGeneric below
+          // will throw a type exception.
           d_ops[tn][n] = i;
           d_arg_ops[tn][i] = n;
           Trace("sygus-db") << std::endl;
@@ -714,12 +742,6 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
               << "Sygus datatype " << dt.getName()
               << " encodes terms that are not of type " << btn << std::endl;
         }
-        //register connected types
-        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-          for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-            registerSygusType( getArgType( dt[i], j ) );
-          }
-        }
       }
     }
   }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 9466a6a10..a9e17fdf9 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -189,6 +189,12 @@ class TermDbSygus {
    * and constants c1...cn.
    */
   bool isEvaluationPoint(Node n) const;
+  /** return the builtin type of tn
+   *
+   * The type tn should be a sygus datatype type that has been registered to
+   * this database.
+   */
+  TypeNode sygusToBuiltinType(TypeNode tn);
   //-----------------------------end conversion from sygus to builtin
 
  private:
@@ -285,7 +291,6 @@ private:
   unsigned getSelectorWeight(TypeNode tn, Node sel);
 
  public:
-  TypeNode sygusToBuiltinType( TypeNode tn );
   int getKindConsNum( TypeNode tn, Kind k );
   int getConstConsNum( TypeNode tn, Node n );
   int getOpConsNum( TypeNode tn, Node n );
-- 
2.30.2