From 673bb476c2a1b51abbc95acb0afaf4e3b8a9feb7 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 6 Jul 2016 13:33:55 -0500 Subject: [PATCH] Add comment field for model, resolves hack for printing sep logic models. --- src/options/strings_options | 4 +- src/printer/smt2/smt2_printer.cpp | 8 +++ src/smt/model.h | 3 +- src/theory/sep/theory_sep.cpp | 62 ++++++++++++------- src/theory/sep/theory_sep.h | 1 + src/theory/strings/theory_strings.cpp | 4 +- .../strings/theory_strings_preprocess.cpp | 3 + src/theory/theory.h | 4 +- src/theory/theory_engine.cpp | 9 +++ src/theory/theory_engine.h | 1 + src/theory/theory_model.cpp | 11 ++++ src/theory/theory_model.h | 5 +- 12 files changed, 84 insertions(+), 31 deletions(-) diff --git a/src/options/strings_options b/src/options/strings_options index 5c991a1bb..136175d72 100644 --- 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 35e6f1a73..4cdf5a9fb 100644 --- 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 768cb3e6a..eadeb1c4b 100644 --- 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 605537c2d..8b63c3149 100644 --- 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; jsecond].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; jsecond].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 &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 81062d67a..3f9514364 100644 --- 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 f6894e07b..913a6800b 100644 --- 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 c126e89ad..aae6fce17 100644 --- 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 f43a2aa7f..062ae78ed 100644 --- 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 833b124eb..3ee1be530 100644 --- 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 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(); -- 2.30.2