diff options
Diffstat (limited to 'src/theory/theory_model_builder.cpp')
-rw-r--r-- | src/theory/theory_model_builder.cpp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 47355aa81..6df412ae3 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -13,6 +13,7 @@ **/ #include "theory/theory_model_builder.h" +#include "expr/dtype.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/uf_options.h" @@ -198,7 +199,7 @@ bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) } else if (tn.isDatatype()) { - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + const DType& dt = tn.getDType(); return dt.involvesUninterpretedType(); } else @@ -264,12 +265,12 @@ void TheoryEngineModelBuilder::addToTypeList( } else if (tn.isDatatype()) { - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + const DType& dt = tn.getDType(); for (unsigned i = 0; i < dt.getNumConstructors(); i++) { for (unsigned j = 0; j < dt[i].getNumArgs(); j++) { - TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType()); + TypeNode ctn = dt[i][j].getRangeType(); addToTypeList(ctn, type_list, visiting); } } @@ -627,10 +628,9 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) bool isCorecursive = false; if (t.isDatatype()) { - const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype(); - isCorecursive = - dt.isCodatatype() && (!dt.isFinite(t.toType()) - || dt.isRecursiveSingleton(t.toType())); + const DType& dt = t.getDType(); + isCorecursive = dt.isCodatatype() + && (!dt.isFinite(t) || dt.isRecursiveSingleton(t)); } #ifdef CVC4_ASSERTIONS bool isUSortFiniteRestricted = false; |