From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 3 Apr 2018 15:48:34 +0000 (-0500)
Subject: Internal sygus type checking (#1734)
X-Git-Tag: cvc5-1.0.0~5187
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=77c09d4c79224b726183cfd59df3cf5eff3ff4ea;p=cvc5.git

Internal sygus type checking (#1734)
---

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 40183fe9c..5c073aa0d 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
+#include "base/cvc4_check.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -662,6 +663,15 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
           d_ops[tn][n] = i;
           d_arg_ops[tn][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.
+          std::map<int, Node> pre;
+          Node g = mkGeneric(dt, i, pre);
+          TypeNode gtn = g.getType();
+          CVC4_CHECK(gtn.isSubtypeOf(btn))
+              << "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++ ){