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/quant_split.cpp | |
parent | 7fa164c306dbfe9aad68110cf3fd9cedd3d2e004 (diff) |
Use the node-level datatypes API (#3556)
Diffstat (limited to 'src/theory/quantifiers/quant_split.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index e425cd345..32bd2b0e8 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -47,16 +47,19 @@ void QuantDSplit::checkOwnership(Node q) for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ TypeNode tn = q[0][i].getType(); if( tn.isDatatype() ){ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( dt.isRecursiveSingleton( tn.toType() ) ){ + const DType& dt = tn.getDType(); + if (dt.isRecursiveSingleton(tn)) + { Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl; - }else{ + } + else + { if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ // split if it is a finite datatype - doSplit = dt.isInterpretedFinite(tn.toType()); + doSplit = dt.isInterpretedFinite(tn); }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){ if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){ - if (dt.isInterpretedFinite(tn.toType())) + if (dt.isInterpretedFinite(tn)) { // split if goes from being unhandled -> handled by finite // instantiation. An example is datatypes with uninterpreted sort @@ -144,20 +147,20 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) TypeNode tn = svar.getType(); Assert(tn.isDatatype()); std::vector<Node> cons; - const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); + const DType& dt = tn.getDType(); for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) { std::vector<Node> vars; for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++) { - TypeNode tns = TypeNode::fromType(dt[j][k].getRangeType()); + TypeNode tns = dt[j][k].getRangeType(); Node v = nm->mkBoundVar(tns); vars.push_back(v); } std::vector<Node> bvs_cmb; bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end()); bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end()); - vars.insert(vars.begin(), Node::fromExpr(dt[j].getConstructor())); + vars.insert(vars.begin(), dt[j].getConstructor()); Node c = nm->mkNode(kind::APPLY_CONSTRUCTOR, vars); TNode ct = c; Node body = q[1].substitute(svar, ct); |