From c13527bfa6b47ff4675b429b5e7bb7c6f43ff595 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 14 Jul 2020 07:33:01 -0700 Subject: Use TypeNode in EmptySet (#4740) This commit changes EmptySet to use TypeNode instead of Type. --- src/theory/sets/normal_form.h | 4 ++-- src/theory/sets/solver_state.cpp | 2 +- src/theory/sets/theory_sets_private.cpp | 2 +- src/theory/sets/theory_sets_rewriter.cpp | 24 ++++++++++++++++-------- src/theory/sets/theory_sets_type_enumerator.cpp | 2 +- src/theory/sets/theory_sets_type_rules.h | 5 ++--- 6 files changed, 23 insertions(+), 16 deletions(-) (limited to 'src/theory/sets') diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index 56f09e2a5..0607a0e6c 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -34,7 +34,7 @@ class NormalForm { NodeManager* nm = NodeManager::currentNM(); if (elements.size() == 0) { - return nm->mkConst(EmptySet(nm->toType(setType))); + return nm->mkConst(EmptySet(setType)); } else { @@ -128,7 +128,7 @@ class NormalForm { } static Node mkBop( Kind k, std::vector< Node >& els, TypeNode tn, unsigned index = 0 ){ if( index>=els.size() ){ - return NodeManager::currentNM()->mkConst(EmptySet(tn.toType())); + return NodeManager::currentNM()->mkConst(EmptySet(tn)); }else if( index==els.size()-1 ){ return els[index]; }else{ diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 057d3a791..d3c23454e 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -453,7 +453,7 @@ Node SolverState::getEmptySet(TypeNode tn) { return it->second; } - Node n = NodeManager::currentNM()->mkConst(EmptySet(tn.toType())); + Node n = NodeManager::currentNM()->mkConst(EmptySet(tn)); d_emptyset[tn] = n; return n; } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index fc2a992a9..4c3affe99 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1504,7 +1504,7 @@ TrustNode TheorySetsPrivate::expandDefinition(Node node) Node witnessVariable = nm->mkBoundVar(setType.getSetElementType()); Node equal = witnessVariable.eqNode(apply); - Node emptySet = nm->mkConst(EmptySet(setType.toType())); + Node emptySet = nm->mkConst(EmptySet(setType)); Node isEmpty = set.eqNode(emptySet); Node member = nm->mkNode(MEMBER, witnessVariable, set); Node memberAndEqual = member.andNode(equal); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index c26a3852c..a7fbc8a38 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -120,7 +120,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { case kind::SETMINUS: { if(node[0] == node[1]) { - Node newNode = nm->mkConst(EmptySet(nm->toType(node[0].getType()))); + Node newNode = nm->mkConst(EmptySet(node[0].getType())); Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; return RewriteResponse(REWRITE_DONE, newNode); } else if(node[0].getKind() == kind::EMPTYSET || @@ -128,7 +128,9 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; return RewriteResponse(REWRITE_AGAIN, node[0]); }else if( node[1].getKind() == kind::UNIVERSE_SET ){ - return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkConst(EmptySet(node[1].getType().toType()))); + return RewriteResponse( + REWRITE_AGAIN, + NodeManager::currentNM()->mkConst(EmptySet(node[1].getType()))); } else if(node[0].isConst() && node[1].isConst()) { std::set left = NormalForm::getElementsFromNormalConstant(node[0]); std::set right = NormalForm::getElementsFromNormalConstant(node[1]); @@ -244,7 +246,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { } if(node[0].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + return RewriteResponse(REWRITE_DONE, + nm->mkConst(EmptySet(node.getType()))); } else if(node[0].isConst()) { std::set new_tuple_set; std::set tuple_set = NormalForm::getElementsFromNormalConstant(node[0]); @@ -271,7 +274,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { Trace("sets-rels-postrewrite") << "Sets::postRewrite processing " << node << std::endl; if( node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + return RewriteResponse(REWRITE_DONE, + nm->mkConst(EmptySet(node.getType()))); } else if( node[0].isConst() && node[1].isConst() ) { Trace("sets-rels-postrewrite") << "Sets::postRewrite processing **** " << node << std::endl; std::set new_tuple_set; @@ -315,7 +319,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { case kind::JOIN: { if( node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + return RewriteResponse(REWRITE_DONE, + nm->mkConst(EmptySet(node.getType()))); } else if( node[0].isConst() && node[1].isConst() ) { Trace("sets-rels-postrewrite") << "Sets::postRewrite processing " << node << std::endl; std::set new_tuple_set; @@ -359,7 +364,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { case kind::TCLOSURE: { if(node[0].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + return RewriteResponse(REWRITE_DONE, + nm->mkConst(EmptySet(node.getType()))); } else if (node[0].isConst()) { std::set rel_mems = NormalForm::getElementsFromNormalConstant(node[0]); std::set tc_rel_mems = RelsUtils::computeTC(rel_mems, node); @@ -379,7 +385,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { case kind::IDEN: { if(node[0].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + return RewriteResponse(REWRITE_DONE, + nm->mkConst(EmptySet(node.getType()))); } else if (node[0].isConst()) { std::set iden_rel_mems; std::set rel_mems = NormalForm::getElementsFromNormalConstant(node[0]); @@ -409,7 +416,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { if( min_card == 0) { return RewriteResponse(REWRITE_DONE, nm->mkNullaryOperator( node.getType(), kind::UNIVERSE_SET )); } else if(node[0].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType())))); + return RewriteResponse(REWRITE_DONE, + nm->mkConst(EmptySet(node.getType()))); } else if (node[0].isConst()) { std::set has_checked; std::set join_img_mems; diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp index 5a949a95b..7f5628c66 100644 --- a/src/theory/sets/theory_sets_type_enumerator.cpp +++ b/src/theory/sets/theory_sets_type_enumerator.cpp @@ -28,7 +28,7 @@ SetEnumerator::SetEnumerator(TypeNode type, TypeEnumeratorProperties* tep) d_currentSetIndex(0), d_currentSet() { - d_currentSet = d_nodeManager->mkConst(EmptySet(type.toType())); + d_currentSet = d_nodeManager->mkConst(EmptySet(type)); } SetEnumerator::SetEnumerator(const SetEnumerator& enumerator) diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 753dcaf76..5d01a966a 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -139,8 +139,7 @@ struct EmptySetTypeRule { { Assert(n.getKind() == kind::EMPTYSET); EmptySet emptySet = n.getConst(); - Type setType = emptySet.getType(); - return TypeNode::fromType(setType); + return emptySet.getType(); } };/* struct EmptySetTypeRule */ @@ -444,7 +443,7 @@ struct SetsProperties { inline static Node mkGroundTerm(TypeNode type) { Assert(type.isSet()); - return NodeManager::currentNM()->mkConst(EmptySet(type.toType())); + return NodeManager::currentNM()->mkConst(EmptySet(type)); } };/* struct SetsProperties */ -- cgit v1.2.3