diff options
author | ajreynol <reynolds@larapc05.epfl.ch> | 2014-05-01 13:28:56 +0200 |
---|---|---|
committer | ajreynol <reynolds@larapc05.epfl.ch> | 2014-05-01 13:28:56 +0200 |
commit | f040f95e28f2f9fda6c88243f550ff63b3faac22 (patch) | |
tree | f93c1543de373c80e1cefad22162e74f933d5dfb /src/theory/quantifiers/quant_conflict_find.cpp | |
parent | 400b89526fe95c9d5b3ddac1d38686d1d05cf4eb (diff) |
Minor optimizations to datatypes, revert to checkClash not mod eq. Minor clean up.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 2f399be33..7c71313de 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -137,7 +137,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;
if( n.getKind()==FORALL ){
registerNode( n[1], hasPol, pol, true );
- }else{ + }else{
if( !MatchGen::isHandledBoolConnective( n ) ){
if( n.hasBoundVar() ){
//literals
@@ -147,7 +147,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) }
}else if( MatchGen::isHandledUfTerm( n ) ){
flatten( n, beneathQuant );
- }else if( n.getKind()==ITE ){ + }else if( n.getKind()==ITE ){
for( unsigned i=1; i<=2; i++ ){
flatten( n[i], beneathQuant );
}
@@ -2110,7 +2110,7 @@ void QuantConflictFind::check( Theory::Effort level ) { Trace("qcf-debug") << std::endl;
debugPrint("qcf-debug");
Trace("qcf-debug") << std::endl;
- } + }
short end_e = getMaxQcfEffort();
for( short e = effort_conflict; e<=end_e; e++ ){
d_effort = e;
@@ -2223,7 +2223,7 @@ void QuantConflictFind::check( Theory::Effort level ) { }
}else{
Trace("qcf-check") << " ... Spurious instantiation (match is inconsistent)" << std::endl;
- } + }
}
if( d_conflict ){
break;
@@ -2244,7 +2244,9 @@ void QuantConflictFind::check( Theory::Effort level ) { }
Trace("qcf-engine") << std::endl;
int currEt = d_statistics.d_entailment_checks.getData();
- Trace("qcf-engine") << " Entailment checks = " << ( currEt - prevEt ) << std::endl;
+ if( currEt!=prevEt ){
+ Trace("qcf-engine") << " Entailment checks = " << ( currEt - prevEt ) << std::endl;
+ }
}
}
Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
@@ -2310,7 +2312,7 @@ void QuantConflictFind::computeRelevantEqr() { }
}else{
d_eqcs[rtn].push_back( r );
- } + }
/*
eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );
while( !eqc_i.isFinished() ){
@@ -2320,9 +2322,10 @@ void QuantConflictFind::computeRelevantEqr() { exit( 199 );
}
++eqc_i;
- } -
*/
- + }
+
+ */
+
//if( r.getType().isInteger() ){
// Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;
//}
|