diff options
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/theory_sep_rewriter.cpp | 52 | ||||
-rw-r--r-- | src/theory/sep/theory_sep_rewriter.h | 4 |
2 files changed, 0 insertions, 56 deletions
diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index 4d0885dc2..614d4f7c4 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -161,58 +161,6 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) { return RewriteResponse(node==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); } -Node TheorySepRewriter::preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited ) { - std::map< Node, Node >::iterator it = visited[pol].find( n ); - if( it==visited[pol].end() ){ - Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol << std::endl; - Node ret = n; - if( n.getKind()==kind::SEP_EMP ){ - if( !pol ){ - TypeNode tnx = n[0].getType(); - TypeNode tny = n[1].getType(); - Node x = NodeManager::currentNM()->mkSkolem( "ex", tnx, "skolem location for negated emp" ); - Node y = NodeManager::currentNM()->mkSkolem( "ey", tny, "skolem data for negated emp" ); - return NodeManager::currentNM()->mkNode( kind::SEP_STAR, - NodeManager::currentNM()->mkNode( kind::SEP_PTO, x, y ), - NodeManager::currentNM()->mkConst( true ) ).negate(); - } - }else if( n.getKind()!=kind::FORALL && n.getNumChildren()>0 ){ - std::vector< Node > children; - bool childChanged = false; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - bool newPol, newHasPol; - QuantPhaseReq::getPolarity( n, i, true, pol, newHasPol, newPol ); - Node nc = n[i]; - if( newHasPol ){ - nc = preSkolemEmp( n[i], newPol, visited ); - childChanged = childChanged || nc!=n[i]; - } - children.push_back( nc ); - } - if( childChanged ){ - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - } - visited[pol][n] = ret; - return n; - }else{ - return it->second; - } -} - -Node TheorySepRewriter::preprocess( Node n ) { - if( options::sepPreSkolemEmp() ){ - bool pol = true; - std::map< bool, std::map< Node, Node > > visited; - n = preSkolemEmp( n, pol, visited ); - } - return n; -} - - }/* CVC4::theory::sep namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h index e867bc0e9..8ed8c3de2 100644 --- a/src/theory/sep/theory_sep_rewriter.h +++ b/src/theory/sep/theory_sep_rewriter.h @@ -43,10 +43,6 @@ public: static inline void init() {} static inline void shutdown() {} -private: - static Node preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited ); -public: - static Node preprocess( Node n ); };/* class TheorySepRewriter */ }/* CVC4::theory::sep namespace */ |