diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-12 14:38:42 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-12 14:38:42 -0600 |
commit | e6d20229cf21a3614ac546514f42bd06002d52b8 (patch) | |
tree | d47a2d716ab17151ae3e622a9e372b15cbdf605f /src/theory/theory_model_builder.cpp | |
parent | 7fa164c306dbfe9aad68110cf3fd9cedd3d2e004 (diff) |
Use the node-level datatypes API (#3556)
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; |