From 77c09d4c79224b726183cfd59df3cf5eff3ff4ea Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 3 Apr 2018 10:48:34 -0500 Subject: [PATCH] Internal sygus type checking (#1734) --- src/theory/quantifiers/sygus/term_database_sygus.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) 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 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