Add comment field for model, resolves hack for printing sep logic models.

diff --git a/src/options/strings_options b/src/options/strings_options
index 5c991a1bb8c2a3a1c07ccf4b5a5a3c3e7c519a7d..136175d721d9dc0dd7f1c641d86d04de219da36d 100644 (file)
--- a/src/options/strings_options
+++ b/src/options/strings_options
@@ -38,9 +38,7 @@ option stringIgnNegMembership strings-inm --strings-inm bool :default false
 # the cardinality of the characters used by the theory of strings, default 128 (for standard ASCII) or 256 (for extended ASCII)
 
 option stringLazyPreproc strings-lazy-pp --strings-lazy-pp bool :default true
- perform string preprocessing lazily upon assertion
-option stringLazyPreproc2 strings-lazy-pp2 --strings-lazy-pp2 bool :default true
- perform string preprocessing lazily upon failure to reduce 
+ perform string preprocessing lazily
 
 option stringLenGeqZ strings-len-geqz --strings-len-geqz bool :default false
  strings length greater than zero lemmas

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 35e6f1a73076acbf927389d699b243e7640cbb39..4cdf5a9fb8eba56e26421718737ff587045c1271 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1061,6 +1061,14 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core, const std::
 
 
 void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
+  //print the model comments
+  std::stringstream c;
+  m.getComments( c );
+  std::string ln;
+  while( std::getline( c, ln ) ){
+    out << "; " << ln << std::endl;
+  }
+  //print the model
   out << "(model" << endl;
   this->Printer::toStream(out, m);
   out << ")" << endl;

diff --git a/src/smt/model.h b/src/smt/model.h
index 768cb3e6a24e5361d922f5669c1cb3e2b4ffce06..eadeb1c4b0246aea76a57d8c83cecee06827e218 100644 (file)
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -58,7 +58,6 @@ public:
   const SmtEngine* getSmtEngine() const { return &d_smt; }
   /** get the input name (file name, etc.) this model is associated to */
   std::string getInputName() const { return d_inputName; }
-
 public:
   /** Check whether this expr is a don't-care in the model */
   virtual bool isDontCare(Expr expr) const { return false; }
@@ -66,6 +65,8 @@ public:
   virtual Expr getValue(Expr expr) const = 0;
   /** get cardinality for sort */
   virtual Cardinality getCardinality(Type t) const = 0;
+  /** print comments */
+  virtual void getComments(std::ostream& out) const {}
 };/* class Model */
 
 class ModelBuilder {

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 605537c2d7966a53abea44c02823fa192fd1ad6e..8b63c3149a99caebc544b606b5539031b1fbf524 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -276,32 +276,44 @@ void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel )
 {
   // Send the equality engine information to the model
   m->assertEqualityEngine( &d_equalityEngine );
+ 
+}
+
+void TheorySep::collectModelComments(TheoryModel* m) {
+  Trace("sep-model") << "Printing model for TheorySep..." << std::endl;
   
-  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 );
-      if( d_label_model[it->second].d_heap_locs_model.empty() ){
-        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 << " -> ";
-          if( d_pto_model[l].isNull() ){
-            Trace("sep-model") << "_";
-          }else{
-            Trace("sep-model") << d_pto_model[l];
-          }
-          Trace("sep-model") << std::endl;
+  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;
+    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;
+    }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 << " -> ";
+        m->d_comment_str << "  " << l << " -> ";
+        if( d_pto_model[l].isNull() ){
+          Trace("sep-model") << "_";
+          m->d_comment_str << "_";
+        }else{
+          Trace("sep-model") << d_pto_model[l];
+          m->d_comment_str << d_pto_model[l];
         }
+        Trace("sep-model") << std::endl;
+        m->d_comment_str << std::endl;
       }
-      Node nil = getNilRef( it->first );
-      Node vnil = d_valuation.getModel()->getRepresentative( nil );
-      Trace("sep-model") << "; sep.nil = " << vnil << std::endl;
-      Trace("sep-model") << std::endl;
     }
+    Node nil = getNilRef( it->first );
+    Node vnil = d_valuation.getModel()->getRepresentative( nil );
+    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;
   }
+  Trace("sep-model") << "Finished printing model for TheorySep." << std::endl;
 }
 
 /////////////////////////////////////////////////////////////////////////////
@@ -1282,8 +1294,12 @@ void TheorySep::computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ) {
         d_label_model[lbl].d_heap_locs_model.push_back( v_val[1] );
         v_val = v_val[0];
       }
-      Assert( v_val.getKind()==kind::SINGLETON );
-      d_label_model[lbl].d_heap_locs_model.push_back( v_val );
+      if( v_val.getKind()==kind::SINGLETON ){
+        d_label_model[lbl].d_heap_locs_model.push_back( v_val );
+      }else{
+        throw Exception("Could not establish value of heap in model.");
+        Assert( false );
+      }
     }
     //end hack
     for( unsigned j=0; j<d_label_model[lbl].d_heap_locs_model.size(); j++ ){

diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 2c87e79f9d1743adb1f3e079edaa6163876a88a7..85d987cc972dba6fc71cacf150c291e6aaa95e7e 100644 (file)
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -108,6 +108,7 @@ class TheorySep : public Theory {
   public:
 
   void collectModelInfo(TheoryModel* m, bool fullModel);
+  void collectModelComments(TheoryModel* m);
 
   /////////////////////////////////////////////////////////////////////////////
   // NOTIFICATIONS

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 57344236eeb3fbf4306bf55b14b1f4e6caf29aa7..434ae9dd770a4a3f0e229e1cd73fbddd1fe7be5d 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -658,9 +658,9 @@ void TheoryStrings::checkReduction( Node atom, int pol, int effort ) {
   }else{
     if( options::stringLazyPreproc() ){
       if( atom.getKind()==kind::STRING_SUBSTR ){
-        r_effort = options::stringLazyPreproc2() ? 1 : 0;
+        r_effort = 1;
       }else{
-        r_effort = options::stringLazyPreproc2() ? 2 : 0;
+        r_effort = 2;
       }
     }
   }

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index ba811644a4112fd2e9ec2f672b38f127071fe49a..4c69a8eb3a070fc5ccf4f5a111a27ecb19fc58a5 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -450,6 +450,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       d_cache[t] = skw;
       retNode = skw;
     }
+  } else if( t.getKind() == kind::STRING_STRCTN ){
+    //TODO?
+    d_cache[t] = Node::null();
   } else{
     d_cache[t] = Node::null();
   }

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 81062d67a6f00f3d1b34615a3ca23b305d41fb61..3f951436413b88ba9506941e19485d148c450469 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -593,7 +593,9 @@ 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 ){ }
+  
   /**
    * Return a decision request, if the theory has one, or the NULL node
    * otherwise.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f6894e07b9ee65a59b91d7a9153349ff174dbe79..913a6800b327d4b158e24982d42c1dadd7f3928b 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -796,6 +796,15 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
   }
 }
 
+void TheoryEngine::collectModelComments( 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 );
+    }
+  }
+}
+
 /* get model */
 TheoryModel* TheoryEngine::getModel() {
   return d_curr_model;

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index c126e89ad21e314281c04662254fb981cdd3e66d..aae6fce1747034dd76102ebaafba867d2a88fd7b 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -711,6 +711,7 @@ public:
    * collect model info
    */
   void collectModelInfo( theory::TheoryModel* m, bool fullModel );
+  void collectModelComments( theory::TheoryModel* m );
 
   /**
    * Get the current model

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index f43a2aa7f6e55816a3149545bcabc64aeffaac51..062ae78ed81b9bb90eaf5c6e8e3116fe8bfc261c 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -64,6 +64,11 @@ void TheoryModel::reset(){
   d_eeContext->push();
 }
 
+void TheoryModel::getComments(std::ostream& out) const {
+  Trace("model-builder") << "get comments..." << std::endl;
+  out << d_comment_str.str();
+}
+
 Node TheoryModel::getValue(TNode n, bool useDontCares) const {
   //apply substitutions
   Node nn = d_substitutions.apply(n);
@@ -937,6 +942,12 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   //modelBuilder-specific initialization
   processBuildModel( tm, fullModel );
 
+  // Collect model comments from the theories
+  if( fullModel ){
+    Trace("model-builder") << "TheoryEngineModelBuilder: Collect model comments..." << std::endl;
+    d_te->collectModelComments(tm);
+  }
+  
 #ifdef CVC4_ASSERTIONS
   if (fullModel) {
     // Check that every term evaluates to its representative in the model

diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 833b124eb16120888bc466726b92f931d04bbdbc..3ee1be530fffb398a751e38d7d0bb0f7c801e6b2 100644 (file)
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -53,7 +53,10 @@ public:
   Node d_true;
   Node d_false;
   mutable std::hash_map<Node, Node, NodeHashFunction> d_modelCache;
-
+  /** comment stream to include in printing */
+  std::stringstream d_comment_str;
+  /** get comments */
+  void getComments(std::ostream& out) const;
 protected:
   /** reset the model */
   virtual void reset();