diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-03 17:23:04 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-03 17:23:04 +0200 |
| commit | ec2a8ad5e5be550f4f0c5c3be92ee20bf2977efa (patch) | |
| tree | 6df6b309d0e85a2ab56a293c1849be8b2988044e /src/theory/quantifiers/quant_conflict_find.cpp | |
| parent | 83f91b92090ef0231156560f337affc6e5c2a33f (diff) | |
Implement and enable --dt-var-exp-quant, cleanup trace messages, minor changes for relevant term filtering.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
| -rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 504c3dcff..ee4464f87 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2010,9 +2010,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { //try to make a matches making the body false
Trace("qcf-check-debug") << "Get next match..." << std::endl;
while( qi->d_mg->getNextMatch( this, qi ) ){
- Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;
- qi->debugPrintMatch("qcf-check");
- Trace("qcf-check") << std::endl;
+ Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
+ qi->debugPrintMatch("qcf-inst");
+ Trace("qcf-inst") << std::endl;
std::vector< int > assigned;
if( !qi->isMatchSpurious( this ) ){
if( qi->completeMatch( this, assigned ) ){
@@ -2042,7 +2042,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { ++(d_statistics.d_prop_inst);
}
}else{
- Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;
+ Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl;
//Assert( false );
}
}
@@ -2050,10 +2050,10 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { qi->revertMatch( assigned );
d_tempCache.clear();
}else{
- Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
+ Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
}
}else{
- Trace("qcf-check") << " ... Spurious instantiation (match is inconsistent)" << std::endl;
+ Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl;
}
}
if( d_conflict ){
|