diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-17 18:38:16 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-17 18:38:16 -0500 |
commit | f5ed28fe24f6b887630a48dcf476c462c0c227a1 (patch) | |
tree | edd8b8c35b474ed051ace7c861799d734ab5b99d /src/theory/sep | |
parent | 1a2547995acc5a98c8969e628ac5e1c45b0efe94 (diff) |
Cleanup from last commit, treat sep.nil as variable kind.
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/kinds | 12 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 72 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.h | 4 | ||||
-rw-r--r-- | src/theory/sep/theory_sep_rewriter.cpp | 20 | ||||
-rw-r--r-- | src/theory/sep/theory_sep_type_rules.h | 28 |
5 files changed, 69 insertions, 67 deletions
diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index 52418aefb..4ad615c1f 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -11,7 +11,7 @@ properties polite stable-infinite parametric properties check propagate presolve getNextDecisionRequest # constants -constant NIL_REF \ +constant SEP_NIL_REF \ ::CVC4::NilRef \ ::CVC4::NilRefHashFunction \ "expr/sepconst.h" \ @@ -19,16 +19,16 @@ constant NIL_REF \ rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h" -operator SEP_NIL 1 "separation nil" -operator EMP_STAR 1 "separation empty heap" +variable SEP_NIL "separation nil" + +operator SEP_EMP 1 "separation empty heap" operator SEP_PTO 2 "points to relation" operator SEP_STAR 2: "separation star" operator SEP_WAND 2 "separation magic wand" operator SEP_LABEL 2 "separation label" -typerule NIL_REF ::CVC4::theory::sep::NilRefTypeRule -typerule SEP_NIL ::CVC4::theory::sep::SepNilTypeRule -typerule EMP_STAR ::CVC4::theory::sep::EmpStarTypeRule +typerule SEP_NIL_REF ::CVC4::theory::sep::SepNilRefTypeRule +typerule SEP_EMP ::CVC4::theory::sep::SepEmpTypeRule typerule SEP_PTO ::CVC4::theory::sep::SepPtoTypeRule typerule SEP_STAR ::CVC4::theory::sep::SepStarTypeRule typerule SEP_WAND ::CVC4::theory::sep::SepWandTypeRule diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 6fec57852..836a04afa 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -78,10 +78,10 @@ Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) { Node TheorySep::ppRewrite(TNode term) { -/* Trace("sep-pp") << "ppRewrite : " << term << std::endl; +/* Node s_atom = term.getKind()==kind::NOT ? term[0] : term; - if( s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::EMP_STAR ){ + if( s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_EMP ){ //get the reference type (will compute d_type_references) int card = 0; TypeNode tn = getReferenceType( s_atom, card ); @@ -102,7 +102,7 @@ void TheorySep::processAssertions( std::vector< Node >& assertions ) { void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) { if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::EMP_STAR ){ + if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){ //get the reference type (will compute d_type_references) int card = 0; TypeNode tn = getReferenceType( n, card ); @@ -159,8 +159,41 @@ void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) { } } -void TheorySep::preRegisterTerm(TNode node){ +void TheorySep::preRegisterTermRec(TNode t, std::map< TNode, bool >& visited ) { + if( visited.find( t )==visited.end() ){ + visited[t] = true; + Trace("sep-prereg-debug") << "Preregister : " << t << std::endl; + if( t.getKind()==kind::SEP_NIL ){ + Trace("sep-prereg") << "Preregister nil : " << t << std::endl; + //per type, all nil variable references are equal + TypeNode tn = t.getType(); + std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); + if( it==d_nil_ref.end() ){ + Trace("sep-prereg") << "...set as reference." << std::endl; + d_nil_ref[tn] = t; + }else{ + Node nr = it->second; + Trace("sep-prereg") << "...reference is " << nr << "." << std::endl; + if( t!=nr ){ + if( d_reduce.find( t )==d_reduce.end() ){ + d_reduce.insert( t ); + Node lem = NodeManager::currentNM()->mkNode( tn.isBoolean() ? kind::IFF : kind::EQUAL, t, nr ); + Trace("sep-lemma") << "Sep::Lemma: nil ref eq : " << lem << std::endl; + d_out->lemma( lem ); + } + } + } + }else{ + for( unsigned i=0; i<t.getNumChildren(); i++ ){ + preRegisterTermRec( t[i], visited ); + } + } + } +} +void TheorySep::preRegisterTerm(TNode term){ + std::map< TNode, bool > visited; + preRegisterTermRec( term, visited ); } @@ -241,16 +274,15 @@ void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ) if( fullModel ){ for( std::map< TypeNode, Node >::iterator it = d_base_label.begin(); it != d_base_label.end(); ++it ){ + Trace("sep-model") << "; Model for heap, type = " << it->first << " : " << std::endl; computeLabelModel( it->second, d_tmodel ); - //, (label = " << it->second << ") - Trace("sep-model") << "Model for heap, type = " << it->first << " : " << std::endl; if( d_label_model[it->second].d_heap_locs_model.empty() ){ - Trace("sep-model") << " [empty]" << std::endl; + Trace("sep-model") << "; [empty]" << std::endl; }else{ for( unsigned j=0; j<d_label_model[it->second].d_heap_locs_model.size(); j++ ){ Assert( d_label_model[it->second].d_heap_locs_model[j].getKind()==kind::SINGLETON ); Node l = d_label_model[it->second].d_heap_locs_model[j][0]; - Trace("sep-model") << " " << l << " -> "; + Trace("sep-model") << "; " << l << " -> "; if( d_pto_model[l].isNull() ){ Trace("sep-model") << "_"; }else{ @@ -261,7 +293,7 @@ void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ) } Node nil = getNilRef( it->first ); Node vnil = d_valuation.getModel()->getRepresentative( nil ); - Trace("sep-model") << "sep.nil = " << vnil << std::endl; + Trace("sep-model") << "; sep.nil = " << vnil << std::endl; Trace("sep-model") << std::endl; } } @@ -302,7 +334,7 @@ void TheorySep::check(Effort e) { bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; - if( atom.getKind()==kind::EMP_STAR ){ + if( atom.getKind()==kind::SEP_EMP ){ TypeNode tn = atom[0].getType(); if( d_emp_arg.find( tn )==d_emp_arg.end() ){ d_emp_arg[tn] = atom[0]; @@ -312,7 +344,7 @@ void TheorySep::check(Effort e) { } TNode s_atom = atom.getKind()==kind::SEP_LABEL ? atom[0] : atom; TNode s_lbl = atom.getKind()==kind::SEP_LABEL ? atom[1] : TNode::null(); - bool is_spatial = s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::EMP_STAR; + bool is_spatial = s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_EMP; if( is_spatial && s_lbl.isNull() ){ if( d_reduce.find( fact )==d_reduce.end() ){ Trace("sep-lemma-debug") << "Reducing unlabelled assertion " << atom << std::endl; @@ -807,7 +839,7 @@ TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) { TypeNode TheorySep::getReferenceType( Node atom, int& card, int index ) { Trace("sep-type") << "getReference type " << atom << " " << index << std::endl; - Assert( atom.getKind()==kind::SEP_PTO || atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND || atom.getKind()==kind::EMP_STAR || index!=-1 ); + Assert( atom.getKind()==kind::SEP_PTO || atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND || atom.getKind()==kind::SEP_EMP || index!=-1 ); std::map< int, TypeNode >::iterator it = d_reference_type[atom].find( index ); if( it==d_reference_type[atom].end() ){ card = 0; @@ -890,7 +922,7 @@ TypeNode TheorySep::getReferenceType2( Node atom, int& card, int index, Node n, visited[n] = card; return tn1; //return n[1].getType(); - }else if( n.getKind()==kind::EMP_STAR ){ + }else if( n.getKind()==kind::SEP_EMP ){ card = 1; visited[n] = card; return n[0].getType(); @@ -998,8 +1030,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { Node TheorySep::getNilRef( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); if( it==d_nil_ref.end() ){ - TypeEnumerator te(tn); - Node nil = NodeManager::currentNM()->mkNode( kind::SEP_NIL, *te ); + Node nil = NodeManager::currentNM()->mkSepNil( tn ); d_nil_ref[tn] = nil; return nil; }else{ @@ -1047,7 +1078,7 @@ Node TheorySep::getLabel( Node atom, int child, Node lbl ) { Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ) { Assert( n.getKind()!=kind::SEP_LABEL ); - if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR ){ + if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP ){ return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl ); }else if( !n.getType().isBoolean() || n.getNumChildren()==0 ){ return n; @@ -1084,7 +1115,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: return Node::null(); }else{ if( Trace.isOn("sep-inst") ){ - if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR ){ + if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP ){ for( unsigned j=0; j<ind; j++ ){ Trace("sep-inst") << " "; } Trace("sep-inst") << n << "[" << lbl << "] :: " << lbl_v << std::endl; } @@ -1154,7 +1185,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: Node ret = children.empty() ? NodeManager::currentNM()->mkConst( true ) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) ); Trace("sep-inst-debug") << "Return " << ret << std::endl; return ret; - }else if( n.getKind()==kind::EMP_STAR ){ + }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())) ); }else{ @@ -1225,8 +1256,8 @@ void TheorySep::computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ) { if( !d_label_model[lbl].d_computed ){ d_label_model[lbl].d_computed = true; - //Node v_val = d_valuation.getModelValue( s_lbl ); - //hack FIXME + //we must get the value of lbl from the model: this is being run at last call, after the model is constructed + //Assert(...); TODO Node v_val = d_valuation.getModel()->getRepresentative( lbl ); Trace("sep-process") << "Model value (from valuation) for " << lbl << " : " << v_val << std::endl; if( v_val.getKind()!=kind::EMPTYSET ){ @@ -1297,6 +1328,7 @@ bool TheorySep::areDisequal( Node a, Node b ){ return false; } + void TheorySep::eqNotifyPreMerge(TNode t1, TNode t2) { } diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 506cb77cd..852a36721 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -86,9 +86,10 @@ class TheorySep : public Theory { /** Explain why this literal is true by adding assumptions */ void explain(TNode literal, std::vector<TNode>& assumptions); + void preRegisterTermRec(TNode t, std::map< TNode, bool >& visited ); public: - void preRegisterTerm(TNode n); + void preRegisterTerm(TNode t); void propagate(Effort e); Node explain(TNode n); @@ -274,7 +275,6 @@ private: bool hasTerm( Node a ); bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); - /** called when two equivalence classes will merge */ void eqNotifyPreMerge(TNode t1, TNode t2); void eqNotifyPostMerge(TNode t1, TNode t2); diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index ce0b20cbd..d58c2c13d 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -25,7 +25,7 @@ namespace sep { void TheorySepRewriter::getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ){ Assert( n.getKind()==kind::SEP_STAR ); for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( n[i].getKind()==kind::EMP_STAR ){ + if( n[i].getKind()==kind::SEP_EMP ){ s_children.push_back( n[i] ); }else if( n[i].getKind()==kind::SEP_STAR ){ getStarChildren( n[i], s_children, ns_children ); @@ -41,7 +41,7 @@ void TheorySepRewriter::getStarChildren( Node n, std::vector< Node >& s_children //remove empty star std::vector< Node > temp_s_children2; for( unsigned i=0; i<temp_s_children.size(); i++ ){ - if( temp_s_children[i].getKind()!=kind::EMP_STAR ){ + if( temp_s_children[i].getKind()!=kind::SEP_EMP ){ temp_s_children2.push_back( temp_s_children[i] ); } } @@ -87,7 +87,7 @@ void TheorySepRewriter::getAndChildren( Node n, std::vector< Node >& s_children, bool TheorySepRewriter::isSpatial( Node n, std::map< Node, bool >& visited ) { if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR || n.getKind()==kind::SEP_LABEL ){ + if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP || n.getKind()==kind::SEP_LABEL ){ return true; }else if( n.getType().isBoolean() ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ @@ -104,14 +104,6 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) { Trace("sep-postrewrite") << "Sep::postRewrite start " << node << std::endl; Node retNode = node; switch (node.getKind()) { - case kind::SEP_NIL: { - TypeEnumerator te(node[0].getType()); - Node n = *te; - if( n!=node[0] ){ - retNode = NodeManager::currentNM()->mkNode( kind::SEP_NIL, n ); - } - break; - } case kind::SEP_LABEL: { if( node[0].getKind()==kind::SEP_PTO ){ Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, node[0][0] ); @@ -121,7 +113,7 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkNode( kind::AND, c1, c2 ); } } - if( node[0].getKind()==kind::EMP_STAR ){ + if( node[0].getKind()==kind::SEP_EMP ){ retNode = node[1].eqNode( NodeManager::currentNM()->mkConst(EmptySet(node[1].getType().toType())) ); } break; @@ -177,9 +169,9 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) { /* RewriteResponse TheorySepRewriter::preRewrite(TNode node) { - if( node.getKind()==kind::EMP_STAR ){ + if( node.getKind()==kind::SEP_EMP ){ Trace("sep-prerewrite") << "Sep::preRewrite emp star " << std::endl; - return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkNode( kind::EMP_STAR, NodeManager::currentNM()->mkConst( true ) ) ); + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkNode( kind::SEP_EMP, NodeManager::currentNM()->mkConst( true ) ) ); }else{ Trace("sep-prerewrite") << "Sep::preRewrite returning " << node << std::endl; return RewriteResponse(REWRITE_DONE, node); diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h index f47941b03..7d4eb303e 100644 --- a/src/theory/sep/theory_sep_type_rules.h +++ b/src/theory/sep/theory_sep_type_rules.h @@ -25,7 +25,7 @@ namespace CVC4 { namespace theory { namespace sep { -class NilRefTypeRule { +class SepNilRefTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { @@ -33,18 +33,11 @@ public: } }; -class SepNilTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - return n[0].getType(check); - } -}; - -class EmpStarTypeRule { +class SepEmpTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::SEP_EMP); return nodeManager->booleanType(); } }; @@ -55,14 +48,7 @@ struct SepPtoTypeRule { Assert(n.getKind() == kind::SEP_PTO); if( check ) { TypeNode refType = n[0].getType(check); - //SEP-POLY - //if(!refType.isRef()) { - // throw TypeCheckingExceptionPrivate(n, "pto applied to non-reference term"); - //} TypeNode ptType = n[1].getType(check); - //if(!ptType.isComparableTo(refType.getRefConstituentType())){ - // throw TypeCheckingExceptionPrivate(n, "pto maps reference to term of different type"); - //} } return nodeManager->booleanType(); } @@ -102,14 +88,6 @@ struct SepWandTypeRule { } };/* struct SepWandTypeRule */ -class EmpStarInternalTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - return nodeManager->booleanType(); - } -};/* struct EmpStarInternalTypeRule */ - struct SepLabelTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { |