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/sets | |
parent | 7fa164c306dbfe9aad68110cf3fd9cedd3d2e004 (diff) |
Use the node-level datatypes API (#3556)
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/rels_utils.h | 17 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 42 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 11 |
3 files changed, 39 insertions, 31 deletions
diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h index 8ce314c94..79757d311 100644 --- a/src/theory/sets/rels_utils.h +++ b/src/theory/sets/rels_utils.h @@ -17,6 +17,9 @@ #ifndef SRC_THEORY_SETS_RELS_UTILS_H_ #define SRC_THEORY_SETS_RELS_UTILS_H_ +#include "expr/dtype.h" +#include "expr/node.h" + namespace CVC4 { namespace theory { namespace sets { @@ -67,8 +70,9 @@ public: return tuple[n_th]; } TypeNode tn = tuple.getType(); - const Datatype& dt = tn.getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal( tn.toType(), n_th ), tuple); + const DType& dt = tn.getDType(); + return NodeManager::currentNM()->mkNode( + kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, n_th), tuple); } static Node reverseTuple( Node tuple ) { @@ -77,16 +81,17 @@ public: std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes(); std::reverse( tuple_types.begin(), tuple_types.end() ); TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types ); - const Datatype& dt = tn.getDatatype(); - elements.push_back( Node::fromExpr(dt[0].getConstructor() ) ); + const DType& dt = tn.getDType(); + elements.push_back(dt[0].getConstructor()); for(int i = tuple_types.size() - 1; i >= 0; --i) { elements.push_back( nthElementOfTuple(tuple, i) ); } return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements ); } static Node constructPair(Node rel, Node a, Node b) { - const Datatype& dt = rel.getType().getSetElementType().getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b); + const DType& dt = rel.getType().getSetElementType().getDType(); + return NodeManager::currentNM()->mkNode( + kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b); } }; diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index e8724aa8b..2f0997982 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -299,12 +299,12 @@ void TheorySetsRels::check(Theory::Effort level) } hasChecked.insert( fst_mem_rep ); - const Datatype& dt = - join_image_term.getType().getSetElementType().getDatatype(); - Node new_membership = NodeManager::currentNM()->mkNode(kind::MEMBER, - NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, - Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ), - join_image_term); + const DType& dt = + join_image_term.getType().getSetElementType().getDType(); + Node new_membership = nm->mkNode( + MEMBER, + nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem_rep), + join_image_term); if (d_state.isEntailed(new_membership, true)) { ++mem_rep_it; @@ -429,9 +429,11 @@ void TheorySetsRels::check(Theory::Effort level) Node reason = exp; Node fst_mem = RelsUtils::nthElementOfTuple( exp[0], 0 ); Node snd_mem = RelsUtils::nthElementOfTuple( exp[0], 1 ); - const Datatype& dt = - iden_term[0].getType().getSetElementType().getDatatype(); - Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ), iden_term[0] ); + const DType& dt = iden_term[0].getType().getSetElementType().getDType(); + Node fact = nm->mkNode( + MEMBER, + nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem), + iden_term[0]); if( exp[1] != iden_term ) { reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], iden_term ) ); @@ -767,18 +769,18 @@ void TheorySetsRels::check(Theory::Effort level) Node mem = exp[0]; std::vector<Node> r1_element; std::vector<Node> r2_element; - const Datatype& dt1 = pt_rel[0].getType().getSetElementType().getDatatype(); + const DType& dt1 = pt_rel[0].getType().getSetElementType().getDType(); unsigned int s1_len = pt_rel[0].getType().getSetElementType().getTupleLength(); unsigned int tup_len = pt_rel.getType().getSetElementType().getTupleLength(); - r1_element.push_back(Node::fromExpr(dt1[0].getConstructor())); + r1_element.push_back(dt1[0].getConstructor()); unsigned int i = 0; for(; i < s1_len; ++i) { r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); } - const Datatype& dt2 = pt_rel[1].getType().getSetElementType().getDatatype(); - r2_element.push_back(Node::fromExpr(dt2[0].getConstructor())); + const DType& dt2 = pt_rel[1].getType().getSetElementType().getDType(); + r2_element.push_back(dt2[0].getConstructor()); for(; i < tup_len; ++i) { r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); } @@ -825,20 +827,18 @@ void TheorySetsRels::check(Theory::Effort level) TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0]; Node shared_x = d_state.getSkolemCache().mkTypedSkolemCached( shared_type, mem, join_rel, SkolemCache::SK_JOIN, "srj"); - const Datatype& dt1 = - join_rel[0].getType().getSetElementType().getDatatype(); + const DType& dt1 = join_rel[0].getType().getSetElementType().getDType(); unsigned int s1_len = join_rel[0].getType().getSetElementType().getTupleLength(); unsigned int tup_len = join_rel.getType().getSetElementType().getTupleLength(); unsigned int i = 0; - r1_element.push_back(Node::fromExpr(dt1[0].getConstructor())); + r1_element.push_back(dt1[0].getConstructor()); for(; i < s1_len-1; ++i) { r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); } r1_element.push_back(shared_x); - const Datatype& dt2 = - join_rel[1].getType().getSetElementType().getDatatype(); - r2_element.push_back(Node::fromExpr(dt2[0].getConstructor())); + const DType& dt2 = join_rel[1].getType().getSetElementType().getDType(); + r2_element.push_back(dt2[0].getConstructor()); r2_element.push_back(shared_x); for(; i < tup_len; ++i) { r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); @@ -1041,7 +1041,7 @@ void TheorySetsRels::check(Theory::Effort level) TypeNode tn = rel.getType().getSetElementType(); Node r1_rmost = RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], r1_tuple_len-1 ); Node r2_lmost = RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 ); - tuple_elements.push_back( Node::fromExpr(tn.getDatatype()[0].getConstructor()) ); + tuple_elements.push_back(tn.getDType()[0].getConstructor()); if( (areEqual(r1_rmost, r2_lmost) && rel.getKind() == kind::JOIN) || rel.getKind() == kind::PRODUCT ) { @@ -1226,7 +1226,7 @@ void TheorySetsRels::check(Theory::Effort level) if(d_symbolic_tuples.find(n) == d_symbolic_tuples.end()) { Trace("rels-debug") << "[Theory::Rels] Reduce tuple var: " << n[0] << " to a concrete one " << " node = " << n << std::endl; std::vector<Node> tuple_elements; - tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor())); + tuple_elements.push_back((n[0].getType().getDType())[0].getConstructor()); for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) { Node element = RelsUtils::nthElementOfTuple(n[0], i); makeSharedTerm(element); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index a7c506582..d8f5f8c4f 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -21,6 +21,8 @@ #include "theory/sets/normal_form.h" #include "theory/sets/rels_utils.h" +using namespace CVC4::kind; + namespace CVC4 { namespace theory { namespace sets { @@ -281,7 +283,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { while(left_it != left.end()) { Trace("rels-debug") << "Sets::postRewrite processing left_it = " << *left_it << std::endl; std::vector<Node> left_tuple; - left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor())); + left_tuple.push_back(tn.getDType()[0].getConstructor()); for(int i = 0; i < left_len; i++) { left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i)); } @@ -324,7 +326,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { TypeNode tn = node.getType().getSetElementType(); while(left_it != left.end()) { std::vector<Node> left_tuple; - left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor())); + left_tuple.push_back(tn.getDType()[0].getConstructor()); for(int i = 0; i < left_len - 1; i++) { left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i)); } @@ -431,8 +433,9 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { ++rel_mems_it_snd; } if( existing_mems.size() >= min_card ) { - const Datatype& dt = node.getType().getSetElementType().getDatatype(); - join_img_mems.insert(NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem )); + const DType& dt = node.getType().getSetElementType().getDType(); + join_img_mems.insert( + nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem)); } ++rel_mems_it; } |