diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-20 13:28:01 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-20 13:28:01 -0500 |
commit | f827fb06c949d421fb32f6629c2c353ca7bd026e (patch) | |
tree | 04b3563aa2467784517193dd22ef95f2ce1e612a /src/theory/sep | |
parent | daf2eca9a4bb32680cbf35945bb09cfd13be76a7 (diff) |
Infrastructure for storing and printing heap models for separation logic. Ensure value of sep.nil is correct in models. Print instantiations as sexprs.
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 71 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.h | 2 |
2 files changed, 53 insertions, 20 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 53fcce26b..f4c3a712e 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -279,39 +279,66 @@ void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ) } -void TheorySep::collectModelComments(TheoryModel* m) { +void TheorySep::postProcessModel(TheoryModel* m) { Trace("sep-model") << "Printing model for TheorySep..." << std::endl; + std::vector< Node > sep_children; + Node m_neq; + Node m_heap; 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; - m->d_comment_str << "Model for heap, type = " << it->first << " : " << std::endl; + //should only be constructing for one heap type + Assert( m_heap.isNull() ); + Assert( d_loc_to_data_type.find( it->first )!=d_loc_to_data_type.end() ); + Trace("sep-model") << "Model for heap, type = " << it->first << " with data type " << d_loc_to_data_type[it->first] << " : " << std::endl; + TypeEnumerator te_range( d_loc_to_data_type[it->first] ); + //m->d_comment_str << "Model for heap, type = " << it->first << " : " << std::endl; computeLabelModel( it->second, d_tmodel ); if( d_label_model[it->second].d_heap_locs_model.empty() ){ Trace("sep-model") << " [empty]" << std::endl; - m->d_comment_str << " [empty]" << std::endl; + //m->d_comment_str << " [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 ); + std::vector< Node > pto_children; Node l = d_label_model[it->second].d_heap_locs_model[j][0]; + Assert( l.isConst() ); + pto_children.push_back( l ); Trace("sep-model") << " " << l << " -> "; - m->d_comment_str << " " << l << " -> "; + //m->d_comment_str << " " << l << " -> "; if( d_pto_model[l].isNull() ){ Trace("sep-model") << "_"; - m->d_comment_str << "_"; + //m->d_comment_str << "_"; + pto_children.push_back( *te_range ); }else{ Trace("sep-model") << d_pto_model[l]; - m->d_comment_str << d_pto_model[l]; + //m->d_comment_str << d_pto_model[l]; + Node vpto = d_valuation.getModel()->getRepresentative( d_pto_model[l] ); + Assert( vpto.isConst() ); + pto_children.push_back( vpto ); } Trace("sep-model") << std::endl; - m->d_comment_str << std::endl; + //m->d_comment_str << std::endl; + sep_children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_PTO, pto_children ) ); } } Node nil = getNilRef( it->first ); Node vnil = d_valuation.getModel()->getRepresentative( nil ); + m_neq = NodeManager::currentNM()->mkNode( nil.getType().isBoolean() ? kind::IFF : kind::EQUAL, nil, vnil ); Trace("sep-model") << "sep.nil = " << vnil << std::endl; Trace("sep-model") << std::endl; - m->d_comment_str << "sep.nil = " << vnil << std::endl; - m->d_comment_str << std::endl; + //m->d_comment_str << "sep.nil = " << vnil << std::endl; + //m->d_comment_str << std::endl; + if( sep_children.empty() ){ + TypeEnumerator te_domain( it->first ); + m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain ); + }else if( sep_children.size()==1 ){ + m_heap = sep_children[0]; + }else{ + m_heap = NodeManager::currentNM()->mkNode( kind::SEP_STAR, sep_children ); + } + m->setHeapModel( m_heap, m_neq ); + //m->d_comment_str << m->d_sep_heap << std::endl; + //m->d_comment_str << m->d_sep_nil_eq << std::endl; } Trace("sep-model") << "Finished printing model for TheorySep." << std::endl; } @@ -469,6 +496,11 @@ void TheorySep::check(Effort e) { Node ilem = s.eqNode( empSet ); Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, disjoint : " << ilem << std::endl; c_lems.push_back( ilem ); + //nil does not occur in labels[0] + Node nr = getNilRef( tn ); + Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, labels[0] ).negate(); + Trace("sep-lemma") << "Sep::Lemma: sep.nil not in wand antecedant heap : " << nrlem << std::endl; + d_out->lemma( nrlem ); } //send out definitional lemmas for introduced sets for( unsigned j=0; j<c_lems.size(); j++ ){ @@ -482,8 +514,9 @@ void TheorySep::check(Effort e) { if( s_lbl!=ss ){ conc = s_lbl.eqNode( ss ); } - Node ssn = NodeManager::currentNM()->mkNode( kind::EQUAL, s_atom[0], getNilRef(s_atom[0].getType()) ).negate(); - conc = conc.isNull() ? ssn : NodeManager::currentNM()->mkNode( kind::AND, conc, ssn ); + //not needed anymore: semantics of sep.nil is enforced globally + //Node ssn = NodeManager::currentNM()->mkNode( kind::EQUAL, s_atom[0], getNilRef(s_atom[0].getType()) ).negate(); + //conc = conc.isNull() ? ssn : NodeManager::currentNM()->mkNode( kind::AND, conc, ssn ); }else{ //labeled emp should be rewritten Assert( false ); @@ -1036,6 +1069,13 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] ); //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl; //d_out->lemma( slem ); + + //assert that nil ref is not in base label + Node nr = getNilRef( tn ); + Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, n_lbl ).negate(); + Trace("sep-lemma") << "Sep::Lemma: sep.nil not in base label " << tn << " : " << nrlem << std::endl; + d_out->lemma( nrlem ); + return n_lbl; }else{ return it->second; @@ -1056,13 +1096,6 @@ Node TheorySep::getNilRef( TypeNode tn ) { void TheorySep::setNilRef( TypeNode tn, Node n ) { Assert( n.getType()==tn ); d_nil_ref[tn] = n; - /* - //must add unit lemma to ensure nil is always a term in model construction - Node k = NodeManager::currentNM()->mkSkolem( "nk", tn ); - Node eq = NodeManager::currentNM()->mkNode( tn.isBoolean() ? kind::IFF : kind::EQUAL, k, n ); - d_out->lemma( eq ); - */ - //TODO: must not occur in base label } Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 98a4f63c5..29e7a008c 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -108,7 +108,7 @@ class TheorySep : public Theory { public: void collectModelInfo(TheoryModel* m, bool fullModel); - void collectModelComments(TheoryModel* m); + void postProcessModel(TheoryModel* m); ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS |