Better front-end type checking for SyGuS (#3496)

4 files changed, 105 insertions, 8 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index b693eae5b..6dc29b8fe 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1435,6 +1435,10 @@ void Smt2::addSygusConstructorTerm(Datatype& dt,
                                    std::map<Expr, Type>& ntsToUnres) const
 {
   Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl;
+  // Ensure that we do type checking here to catch sygus constructors with
+  // malformed builtin operators. The argument "true" to getType here forces
+  // a recursive well-typedness check.
+  term.getType(true);
   // purify each occurrence of a non-terminal symbol in term, replace by
   // free variables. These become arguments to constructors. Notice we must do
   // a tree traversal in this function, since unique paths to the same term
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index 1ff0457c4..71ccd60c9 100644
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -140,17 +140,17 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
       d_sym_cons_any_constant = i;
       d_has_subterm_sym_cons = true;
     }
-    // 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[n] = i;
     d_arg_ops[i] = n;
     Trace("sygus-db") << std::endl;
-    // ensure that terms that this constructor encodes are
-    // of the type specified in the datatype. This will fail if
-    // e.g. bitvector-and is a constructor of an integer grammar.
+    // We must 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 we use a call to
+    // mkGeneric below. This ensures that terms that this constructor encodes
+    // are of the type specified in the datatype. This will fail if
+    // e.g. bitvector-and is a constructor of an integer grammar. Our (version
+    // 2) SyGuS parser ensures that sygus constructors are built from well-typed
+    // terms, so the term created by mkGeneric will also be well-typed here.
     Node g = tds->mkGeneric(dt, i);
     TypeNode gtn = g.getType();
     AlwaysAssert(gtn.isSubtypeOf(btn))
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 841b18fce..71ea1badd 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -923,6 +923,7 @@ set(regress_0_tests
   regress0/sygus/no-syntax-test.sy
   regress0/sygus/parity-AIG-d0.sy
   regress0/sygus/parse-bv-let.sy
+  regress0/sygus/pLTL-sygus-syntax-err.sy
   regress0/sygus/real-si-all.sy
   regress0/sygus/sygus-no-wf.sy
   regress0/sygus/sygus-uf.sy
diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
new file mode 100644
index 000000000..7a90d7427
--- /dev/null
+++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
@@ -0,0 +1,92 @@
+; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
+; EXPECT-ERROR: CVC4 Error:
+; EXPECT-ERROR: Parse Error: pLTL-sygus-syntax-err.sy:79.19: number of arguments does not match the constructor type
+; EXPECT-ERROR: 
+; EXPECT-ERROR: (Op2 <O2> <F>)
+; EXPECT-ERROR: ^
+; EXIT: 1
+(set-logic ALL)
+(set-option :lang sygus2)
+;(set-option :sygus-out status)
+(set-option :sygus-rec-fun true)
+(set-option :uf-ho true)
+
+(define-sort Time () Int)
+
+(declare-datatype Var ( (X0) (X1) ))
+
+; Declare Unary Operators.
+(declare-datatype UNARY_OP ( (NOT) (Y) (G) (H) ))
+
+; Declare Binary Operators.
+(declare-datatype BINARY_OP ( (AND) (OR) (IMPLIES) )) ; (S) ))
+
+; Formula Declaration.
+(declare-datatype Formula (
+  (P (Id Var))
+  (Op1 (op1 UNARY_OP) (f Formula))
+  (Op2 (op2 BINARY_OP) (f1 Formula) (f2 Formula))
+  )
+)
+
+; Trace Length.
+(declare-const tn Int)
+(assert (= tn 2))
+
+;cTrace Declaration (trace_index, variable_index)
+(define-fun val ((i Int) (x Var)) Bool
+  (or (and (= i 0) (= x X0))
+      (and (= i 0) (= x X1))
+      (and (= i 1) (= x X1))
+  )
+)
+
+;cpLTL Semantics
+(define-fun-rec holds ((f Formula) (t Time)) Bool
+  (and (<= 0 t tn)
+       (match f (
+         ((P i) (val t i))
+      
+         ((Op1 op g) 
+           (match op (
+             (NOT (not (holds g t))) 
+
+             (Y (and (< 0 t) (holds g (- t 1))))    
+
+             (G (and (holds g t) (or (= t tn) (holds f (+ t 1)))))
+
+             (H (and (holds g t) (or (= t 0) (holds f (- t 1)))))
+          )))
+
+         ((Op2 op f g)     
+           (match op (
+             (AND (and (holds f t) (holds g t)))
+
+             (OR  (or (holds f t) (holds g t)))
+
+             (IMPLIES (or (not (holds f t)) (holds g t)))
+         )))))
+    )
+)
+
+(synth-fun phi ((x0 Var) (x1 Var)) Formula
+  ((<F> Formula) (<O1> UNARY_OP) (<O2> BINARY_OP))
+  (
+   (<F> Formula (
+     (P x0)
+     (P x1)
+     (Op1 <O1> <F>)
+     (Op2 <O2> <F>)
+     )
+   )
+   (<O1> UNARY_OP (NOT Y G H))
+   (<O2> BINARY_OP (AND OR IMPLIES))
+  )
+)
+
+(constraint (holds (Op1 G (phi X0 X1)) 0))
+
+(check-synth)
+
+
+