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/quantifiers/sygus/sygus_explain.cpp | |
| parent | 7fa164c306dbfe9aad68110cf3fd9cedd3d2e004 (diff) | |
Use the node-level datatypes API (#3556)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_explain.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.cpp | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index cf1993efb..8fb7cf2e7 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/sygus_explain.h" +#include "expr/dtype.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -138,7 +139,7 @@ void SygusExplain::getExplanationForEquality(Node n, return; } Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR); - const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); + const DType& dt = tn.getDType(); int i = datatypes::utils::indexOf(vn.getOperator()); Node tst = datatypes::utils::mkTester(n, i, dt); exp.push_back(tst); @@ -147,9 +148,7 @@ void SygusExplain::getExplanationForEquality(Node n, if (cexc.find(j) == cexc.end()) { Node sel = NodeManager::currentNM()->mkNode( - kind::APPLY_SELECTOR_TOTAL, - Node::fromExpr(dt[i].getSelectorInternal(tn.toType(), j)), - n); + kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(tn, j), n); getExplanationForEquality(sel, vn[j], exp); } } @@ -227,7 +226,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, trb.replaceChild(i, vn[i]); } } - const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype(); + const DType& dt = ntn.getDType(); int cindex = datatypes::utils::indexOf(vn.getOperator()); Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors()); Node tst = datatypes::utils::mkTester(n, cindex, dt); @@ -245,9 +244,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, for (unsigned i = 0; i < vn.getNumChildren(); i++) { Node sel = NodeManager::currentNM()->mkNode( - kind::APPLY_SELECTOR_TOTAL, - Node::fromExpr(dt[cindex].getSelectorInternal(ntn.toType(), i)), - n); + kind::APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(ntn, i), n); Node vnr_c = vnr.isNull() ? vnr : (vn[i] == vnr[i] ? Node::null() : vnr[i]); if (cexc.find(i) == cexc.end()) { |