summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/strings_options4
-rw-r--r--src/printer/smt2/smt2_printer.cpp8
-rw-r--r--src/smt/model.h3
-rw-r--r--src/theory/sep/theory_sep.cpp62
-rw-r--r--src/theory/sep/theory_sep.h1
-rw-r--r--src/theory/strings/theory_strings.cpp4
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp3
-rw-r--r--src/theory/theory.h4
-rw-r--r--src/theory/theory_engine.cpp9
-rw-r--r--src/theory/theory_engine.h1
-rw-r--r--src/theory/theory_model.cpp11
-rw-r--r--src/theory/theory_model.h5
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; 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 2c87e79f9..85d987cc9 100644
--- 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 57344236e..434ae9dd7 100644
--- 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 ba811644a..4c69a8eb3 100644
--- 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 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<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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback