Internal sygus type checking (#1734)

1 files changed, 10 insertions, 0 deletions

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++ ){