diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-14 07:33:01 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-14 09:33:01 -0500 |
commit | c13527bfa6b47ff4675b429b5e7bb7c6f43ff595 (patch) | |
tree | f182e942b3bc4ad99a8fdf765959781f1a2570dd /src/theory/sep | |
parent | 1cd3c3c5dad84093aa6b2db164798c8fff473fec (diff) |
Use TypeNode in EmptySet (#4740)
This commit changes EmptySet to use TypeNode instead of Type.
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 18 | ||||
-rw-r--r-- | src/theory/sep/theory_sep_rewriter.cpp | 3 |
2 files changed, 13 insertions, 8 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 372800b2b..e9b186ae2 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -378,7 +378,8 @@ void TheorySep::check(Effort e) { } std::vector< Node > labels; getLabelChildren( s_atom, s_lbl, children, labels ); - Node empSet = NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType())); + Node empSet = + NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType())); Assert(children.size() > 1); if( s_atom.getKind()==kind::SEP_STAR ){ //reduction for heap : union, pairwise disjoint @@ -429,9 +430,11 @@ void TheorySep::check(Effort e) { //conc = conc.isNull() ? ssn : NodeManager::currentNM()->mkNode( kind::AND, conc, ssn ); }else if( s_atom.getKind()==kind::SEP_EMP ){ - //conc = s_lbl.eqNode( NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType())) ); + // conc = s_lbl.eqNode( + // NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType())) ); Node lem; - Node emp_s = NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType())); + Node emp_s = + NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType())); if( polarity ){ lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), s_lbl.eqNode( emp_s ) ); }else{ @@ -1235,7 +1238,7 @@ Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { Node u; if( locs.empty() ){ TypeNode ltn = NodeManager::currentNM()->mkSetType(tn); - return NodeManager::currentNM()->mkConst(EmptySet(ltn.toType())); + return NodeManager::currentNM()->mkConst(EmptySet(ltn)); }else{ for( unsigned i=0; i<locs.size(); i++ ){ Node s = locs[i]; @@ -1343,7 +1346,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: return Node::null(); } } - Node empSet = NodeManager::currentNM()->mkConst(EmptySet(rtn.toType())); + Node empSet = NodeManager::currentNM()->mkConst(EmptySet(rtn)); if( n.getKind()==kind::SEP_STAR ){ //disjoint contraints @@ -1435,7 +1438,8 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: return ret; }else if( n.getKind()==kind::SEP_EMP ){ //return NodeManager::currentNM()->mkConst( lbl_v.getKind()==kind::EMPTYSET ); - return lbl_v.eqNode( NodeManager::currentNM()->mkConst(EmptySet(lbl_v.getType().toType())) ); + return lbl_v.eqNode( + NodeManager::currentNM()->mkConst(EmptySet(lbl_v.getType()))); }else{ std::map< Node, Node >::iterator it = visited.find( n ); if( it==visited.end() ){ @@ -1780,7 +1784,7 @@ void TheorySep::debugPrintHeap( HeapInfo& heap, const char * c ) { Node TheorySep::HeapInfo::getValue( TypeNode tn ) { Assert(d_heap_locs.size() == d_heap_locs_model.size()); if( d_heap_locs.empty() ){ - return NodeManager::currentNM()->mkConst(EmptySet(tn.toType())); + return NodeManager::currentNM()->mkConst(EmptySet(tn)); }else if( d_heap_locs.size()==1 ){ return d_heap_locs[0]; }else{ diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index e993d05dd..10348a415 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -110,7 +110,8 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) { } } if( node[0].getKind()==kind::SEP_EMP ){ - retNode = node[1].eqNode( NodeManager::currentNM()->mkConst(EmptySet(node[1].getType().toType())) ); + retNode = node[1].eqNode( + NodeManager::currentNM()->mkConst(EmptySet(node[1].getType()))); } break; } |