diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-03 10:48:34 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-03 10:48:34 -0500 |
commit | 77c09d4c79224b726183cfd59df3cf5eff3ff4ea (patch) | |
tree | d9ca97838d69109cc3d12e2d0480c0defeb1fbce /src | |
parent | 4a516e33436fb0abd9efd9b8ec92a8e65534ce3a (diff) |
Internal sygus type checking (#1734)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 10 |
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++ ){ |