From 1bceb5036a208746bfba1ec42d65862d0d231a83 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 9 Nov 2019 16:09:11 -0600 Subject: [PATCH] Fixes in relations related to datatypes not passed by reference (#3449) The current code is creating/destroying datatypes unnecessarily. --- src/theory/sets/rels_utils.h | 6 +++--- src/theory/sets/theory_sets_rels.cpp | 24 ++++++++++++++---------- src/theory/sets/theory_sets_rewriter.cpp | 2 +- 3 files changed, 18 insertions(+), 14 deletions(-) diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h index 6354b59e9..8ce314c94 100644 --- a/src/theory/sets/rels_utils.h +++ b/src/theory/sets/rels_utils.h @@ -67,7 +67,7 @@ public: return tuple[n_th]; } TypeNode tn = tuple.getType(); - Datatype dt = tn.getDatatype(); + const Datatype& dt = tn.getDatatype(); return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal( tn.toType(), n_th ), tuple); } @@ -77,7 +77,7 @@ public: std::vector tuple_types = tuple.getType().getTupleTypes(); std::reverse( tuple_types.begin(), tuple_types.end() ); TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types ); - Datatype dt = tn.getDatatype(); + const Datatype& dt = tn.getDatatype(); elements.push_back( Node::fromExpr(dt[0].getConstructor() ) ); for(int i = tuple_types.size() - 1; i >= 0; --i) { elements.push_back( nthElementOfTuple(tuple, i) ); @@ -85,7 +85,7 @@ public: return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements ); } static Node constructPair(Node rel, Node a, Node b) { - Datatype dt = rel.getType().getSetElementType().getDatatype(); + const Datatype& dt = rel.getType().getSetElementType().getDatatype(); return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b); } diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 5c24cb088..e8724aa8b 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -299,7 +299,8 @@ void TheorySetsRels::check(Theory::Effort level) } hasChecked.insert( fst_mem_rep ); - Datatype dt = join_image_term.getType().getSetElementType().getDatatype(); + 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 ), @@ -428,7 +429,8 @@ 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 ); - Datatype dt = iden_term[0].getType().getSetElementType().getDatatype(); + 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] ); if( exp[1] != iden_term ) { @@ -765,18 +767,18 @@ void TheorySetsRels::check(Theory::Effort level) Node mem = exp[0]; std::vector r1_element; std::vector r2_element; - Datatype dt = pt_rel[0].getType().getSetElementType().getDatatype(); + const Datatype& dt1 = pt_rel[0].getType().getSetElementType().getDatatype(); 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(dt[0].getConstructor())); + r1_element.push_back(Node::fromExpr(dt1[0].getConstructor())); unsigned int i = 0; for(; i < s1_len; ++i) { r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); } - dt = pt_rel[1].getType().getSetElementType().getDatatype(); - r2_element.push_back(Node::fromExpr(dt[0].getConstructor())); + const Datatype& dt2 = pt_rel[1].getType().getSetElementType().getDatatype(); + r2_element.push_back(Node::fromExpr(dt2[0].getConstructor())); for(; i < tup_len; ++i) { r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); } @@ -823,18 +825,20 @@ 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"); - Datatype dt = join_rel[0].getType().getSetElementType().getDatatype(); + const Datatype& dt1 = + join_rel[0].getType().getSetElementType().getDatatype(); 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(dt[0].getConstructor())); + r1_element.push_back(Node::fromExpr(dt1[0].getConstructor())); for(; i < s1_len-1; ++i) { r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); } r1_element.push_back(shared_x); - dt = join_rel[1].getType().getSetElementType().getDatatype(); - r2_element.push_back(Node::fromExpr(dt[0].getConstructor())); + const Datatype& dt2 = + join_rel[1].getType().getSetElementType().getDatatype(); + r2_element.push_back(Node::fromExpr(dt2[0].getConstructor())); r2_element.push_back(shared_x); for(; i < tup_len; ++i) { r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i)); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index aa6f4de3f..a7c506582 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -431,7 +431,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { ++rel_mems_it_snd; } if( existing_mems.size() >= min_card ) { - Datatype dt = node.getType().getSetElementType().getDatatype(); + const Datatype& dt = node.getType().getSetElementType().getDatatype(); join_img_mems.insert(NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem )); } ++rel_mems_it; -- 2.30.2