diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-11-30 18:11:48 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-11-30 18:11:48 +0000 |
| commit | 4d6d4e0b4082d4c8624e04d040f84070138c3f72 (patch) | |
| tree | 22d44bf2fa823a1f2a8f8cfac62a2e3575878bf5 /src/theory | |
| parent | a0cce22b009afac40122c01a57404c94db241ea6 (diff) | |
Partial fix for bug 435; still needs some effort.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/datatypes/kinds | 6 | ||||
| -rw-r--r-- | src/theory/datatypes/type_enumerator.h | 5 |
2 files changed, 10 insertions, 1 deletions
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index d1fbf82bc..3968af4dd 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -63,11 +63,15 @@ operator PARAMETRIC_DATATYPE 1: "parametric datatype" cardinality PARAMETRIC_DATATYPE \ "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality()" \ "util/datatype.h" -well-founded PARAMETRIC_DATATYPE\ +well-founded PARAMETRIC_DATATYPE \ "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \ "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm(%TYPE%.toType())" \ "util/datatype.h" +enumerator PARAMETRIC_DATATYPE \ + "::CVC4::theory::datatypes::DatatypesEnumerator" \ + "theory/datatypes/type_enumerator.h" + parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \ "type ascription, for datatype constructor applications" constant ASCRIPTION_TYPE \ diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index ea68e8957..d8557fcaf 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -66,6 +66,11 @@ public: d_zeroCtor(0), d_argEnumerators(NULL) { + //Assert(type.isDatatype()); + Debug("te") << "datatype is datatype? " << type.isDatatype() << std::endl; + Debug("te") << "datatype is kind " << type.getKind() << std::endl; + Debug("te") << "datatype is " << type << std::endl; + /* find the "zero" constructor (the first non-recursive one) */ /* FIXME: this isn't sufficient for mutually-recursive datatypes! */ while(d_zeroCtor < d_datatype.getNumConstructors()) { |