diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 15:28:24 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 15:28:24 +0000 |
| commit | b11f6d3a27d33b9075e57b37f77ad9d11732fce5 (patch) | |
| tree | b00e257f54c8adebe15f92927fc7b51cb61887c7 /src/theory/uf | |
| parent | 19f0a337307ce0e424b12acf6102829d81dbbf99 (diff) | |
more updates to inst gen: fixed partial instantiations, recognize duplicate defaults for uf
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf_model.cpp | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index f7272f7ba..02e2412a4 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -386,9 +386,9 @@ Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* for( size_t i=0; i<d_values.size(); i++ ){ Node v = d_values[i]; double score = ( 1.0 + (double)d_value_pro_con[0][v].size() )/( 1.0 + (double)d_value_pro_con[1][v].size() ); - Debug("fmf-model-cons") << " - score( "; - m->printRepresentativeDebug( "fmf-model-cons", v ); - Debug("fmf-model-cons") << " ) = " << score << std::endl; + Debug("fmf-model-cons-debug") << " - score( "; + m->printRepresentativeDebug( "fmf-model-cons-debug", v ); + Debug("fmf-model-cons-debug") << " ) = " << score << std::endl; if( score>maxScore ){ defaultVal = v; maxScore = score; @@ -416,10 +416,10 @@ Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* } #endif //get the default term (this term must be defined non-ground in model) - Debug("fmf-model-cons") << " Choose "; - m->printRepresentativeDebug("fmf-model-cons", defaultVal ); - Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl; - Debug("fmf-model-cons") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl; - Debug("fmf-model-cons") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl; + Debug("fmf-model-cons-debug") << " Choose "; + m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal ); + Debug("fmf-model-cons-debug") << " as default value (" << defaultTerm << ")" << std::endl; + Debug("fmf-model-cons-debug") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl; + Debug("fmf-model-cons-debug") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl; return defaultVal; } |