Infrastructure for storing and printing heap models for separation logic. Ensure value of sep.nil is correct in models. Print instantiations as sexprs.

11 files changed, 107 insertions, 36 deletions

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; i<terms.size(); i++ ){
-          if( i>0 ) 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; i<d_term_db->d_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; 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
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<Node, Node, NodeHashFunction> 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();