From: ajreynol Date: Wed, 20 Jul 2016 18:28:01 +0000 (-0500) Subject: Infrastructure for storing and printing heap models for separation logic. Ensure... X-Git-Tag: cvc5-1.0.0~6040^2~38 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f827fb06c949d421fb32f6629c2c353ca7bd026e;p=cvc5.git Infrastructure for storing and printing heap models for separation logic. Ensure value of sep.nil is correct in models. Print instantiations as sexprs. --- diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 4cdf5a9fb..7b7d569b7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1068,6 +1068,15 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() { while( std::getline( c, ln ) ){ out << "; " << ln << std::endl; } + //print the heap model, if it exists + Expr h, neq; + if( m.getHeapModel( h, neq ) ){ + // description of the heap+what nil is equal to fully describes model + out << "(heap" << endl; + out << h << endl; + out << neq << endl; + out << ")" << std::endl; + } //print the model out << "(model" << endl; this->Printer::toStream(out, m); diff --git a/src/smt/model.h b/src/smt/model.h index eadeb1c4b..fd31655f4 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -67,6 +67,8 @@ public: virtual Cardinality getCardinality(Type t) const = 0; /** print comments */ virtual void getComments(std::ostream& out) const {} + /** get heap model (for separation logic) */ + virtual bool getHeapModel( Expr& h, Expr& ne ) const { return false; } };/* class Model */ class ModelBuilder { diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index c419bbc46..7e5424d9c 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -229,7 +229,7 @@ void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& term } if( print ){ if( firstTime ){ - out << "Instantiations of " << q << " : " << std::endl; + out << "(instantiation " << q << std::endl; firstTime = false; } out << " ( "; @@ -403,12 +403,12 @@ void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& te } if( print ){ if( firstTime ){ - out << "Instantiations of " << q << " : " << std::endl; + out << "(instantiation " << q << std::endl; firstTime = false; } out << " ( "; for( unsigned i=0; i0 ) out << ", "; + if( i>0 ) out << " "; out << terms[i]; } out << " )" << std::endl; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index da8233fc1..2975d2e70 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1340,21 +1340,21 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){ Node q = (*it).first; printed = true; - out << "Skolem constants of " << q << " : " << std::endl; + out << "(skolem " << q << std::endl; out << " ( "; for( unsigned i=0; id_skolem_constants[q].size(); i++ ){ - if( i>0 ){ out << ", "; } + if( i>0 ){ out << " "; } out << d_term_db->d_skolem_constants[q][i]; } out << " )" << std::endl; - out << std::endl; + out << ")" << std::endl; } if( options::incrementalSolving() ){ for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ bool firstTime = true; it->second->print( out, it->first, firstTime, useUnsatCore, active_lemmas ); if( !firstTime ){ - out << std::endl; + out << ")" << std::endl; } printed = printed || !firstTime; } @@ -1363,13 +1363,13 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { bool firstTime = true; it->second.print( out, it->first, firstTime, useUnsatCore, active_lemmas ); if( !firstTime ){ - out << std::endl; + out << ")" << std::endl; } printed = printed || !firstTime; } } if( !printed ){ - out << "No instantiations." << std::endl; + out << "No instantiations" << std::endl; } } 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; jsecond].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; jmkNode( 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 diff --git a/src/theory/theory.h b/src/theory/theory.h index 3f9514364..b5a5d4e6d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -593,8 +593,8 @@ public: * class. */ virtual void collectModelInfo( TheoryModel* m, bool fullModel ){ } - /** if theories want to print something as a comment before model printing, do it here */ - virtual void collectModelComments( TheoryModel* m ){ } + /** if theories want to do something with model after building, do it here */ + virtual void postProcessModel( TheoryModel* m ){ } /** * Return a decision request, if the theory has one, or the NULL node diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b4c6c97cd..0ec55a5e6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -798,11 +798,11 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){ } } -void TheoryEngine::collectModelComments( theory::TheoryModel* m ){ +void TheoryEngine::postProcessModel( theory::TheoryModel* m ){ for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) { if(d_logicInfo.isTheoryEnabled(theoryId)) { - Trace("model-builder-debug") << " CollectModelComments on theory: " << theoryId << endl; - d_theoryTable[theoryId]->collectModelComments( m ); + Trace("model-builder-debug") << " PostProcessModel on theory: " << theoryId << endl; + d_theoryTable[theoryId]->postProcessModel( m ); } } } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index aae6fce17..eed58864a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -711,7 +711,8 @@ public: * collect model info */ void collectModelInfo( theory::TheoryModel* m, bool fullModel ); - void collectModelComments( theory::TheoryModel* m ); + /** post process model */ + void postProcessModel( theory::TheoryModel* m ); /** * Get the current model diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 062ae78ed..cccd5c350 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -56,6 +56,9 @@ TheoryModel::~TheoryModel() throw() { void TheoryModel::reset(){ d_modelCache.clear(); + d_comment_str.clear(); + d_sep_heap = Node::null(); + d_sep_nil_eq = Node::null(); d_reps.clear(); d_rep_set.clear(); d_uf_terms.clear(); @@ -69,6 +72,21 @@ void TheoryModel::getComments(std::ostream& out) const { out << d_comment_str.str(); } +void TheoryModel::setHeapModel( Node h, Node neq ) { + d_sep_heap = h; + d_sep_nil_eq = neq; +} + +bool TheoryModel::getHeapModel( Expr& h, Expr& neq ) const { + if( d_sep_heap.isNull() || d_sep_nil_eq.isNull() ){ + return false; + }else{ + h = d_sep_heap.toExpr(); + neq = d_sep_nil_eq.toExpr(); + return true; + } +} + Node TheoryModel::getValue(TNode n, bool useDontCares) const { //apply substitutions Node nn = d_substitutions.apply(n); @@ -945,7 +963,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // Collect model comments from the theories if( fullModel ){ Trace("model-builder") << "TheoryEngineModelBuilder: Collect model comments..." << std::endl; - d_te->collectModelComments(tm); + d_te->postProcessModel(tm); } #ifdef CVC4_ASSERTIONS diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 3ee1be530..7157433f9 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -53,10 +53,18 @@ public: Node d_true; Node d_false; mutable std::hash_map d_modelCache; +public: /** comment stream to include in printing */ std::stringstream d_comment_str; /** get comments */ void getComments(std::ostream& out) const; +private: + /** information for separation logic */ + Node d_sep_heap; + Node d_sep_nil_eq; +public: + void setHeapModel( Node h, Node neq ); + bool getHeapModel( Expr& h, Expr& neq ) const; protected: /** reset the model */ virtual void reset();