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/cegqi | |
parent | 7fa164c306dbfe9aad68110cf3fd9cedd3d2e004 (diff) |
Use the node-level datatypes API (#3556)
Diffstat (limited to 'src/theory/quantifiers/cegqi')
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp | 22 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 12 |
2 files changed, 14 insertions, 20 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp index 6c4f2c620..9fd682aaf 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp @@ -14,7 +14,9 @@ #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h" +#include "expr/dtype.h" #include "expr/node_algorithm.h" +#include "theory/datatypes/theory_datatypes_utils.h" using namespace std; using namespace CVC4::kind; @@ -57,16 +59,14 @@ bool DtInstantiator::processEqualTerms(CegInstantiator* ci, << "...try based on constructor term " << n << std::endl; std::vector<Node> children; children.push_back(n.getOperator()); - const Datatype& dt = - static_cast<DatatypeType>(d_type.toType()).getDatatype(); - unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); + const DType& dt = d_type.getDType(); + unsigned cindex = datatypes::utils::indexOf(n.getOperator()); // now must solve for selectors applied to pv for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++) { - Node c = nm->mkNode( - APPLY_SELECTOR_TOTAL, - Node::fromExpr(dt[cindex].getSelectorInternal(d_type.toType(), j)), - pv); + Node c = nm->mkNode(APPLY_SELECTOR_TOTAL, + dt[cindex].getSelectorInternal(d_type, j), + pv); ci->pushStackVariable(c); children.push_back(c); } @@ -146,15 +146,13 @@ Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb) else { NodeManager* nm = NodeManager::currentNM(); - unsigned cindex = Datatype::indexOf(a.getOperator().toExpr()); + unsigned cindex = DType::indexOf(a.getOperator().toExpr()); TypeNode tn = a.getType(); - const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); + const DType& dt = tn.getDType(); for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++) { Node nn = nm->mkNode( - APPLY_SELECTOR_TOTAL, - Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)), - sb); + APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), sb); Node s = solve_dt(v, a[i], Node::null(), sa[i], nn); if (!s.isNull()) { diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index bed382e28..1d4a23af1 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -341,13 +341,12 @@ CegHandledStatus CegInstantiator::isCbqiSort( // we initialize to handled, we remain handled as long as all subfields // of this datatype are not unhandled. ret = CEG_HANDLED; - const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); + const DType& dt = tn.getDType(); for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) { for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) { - TypeNode crange = TypeNode::fromType( - static_cast<SelectorType>(dt[i][j].getType()).getRangeType()); + TypeNode crange = dt[i].getArgType(j); CegHandledStatus cret = isCbqiSort(crange, visited, qe); if (cret == CEG_UNHANDLED) { @@ -520,15 +519,12 @@ void CegInstantiator::registerTheoryIds(TypeNode tn, registerTheoryId(tid); 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++) { - registerTheoryIds( - TypeNode::fromType( - ((SelectorType)dt[i][j].getType()).getRangeType()), - visited); + registerTheoryIds(dt[i].getArgType(j), visited); } } } |