Fixes in relations related to datatypes not passed by reference (#3449)

The current code is creating/destroying datatypes unnecessarily.

diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index 6354b59e9547cd4cc9b7f99fb65dcac1f2f57e13..8ce314c94d1cc69d1555b15eb29541bf594a63e2 100644 (file)
--- 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<TypeNode> 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 5c24cb088cc10005e161e171ed35007e9ee9dfe8..e8724aa8bc84e7ce71167fc18274b9dc9bc10905 100644 (file)
--- 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<Node>   r1_element;
     std::vector<Node>   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 aa6f4de3f5e1db17f6876a0de3b319f7822ea67c..a7c5065825bf2fe5a6aa31ca7d71740dd169f5f1 100644 (file)
--- 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;