//if( options::finiteModelFind() ){
// ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
//}
+ Trace("quant-debug") << "...finish." << std::endl;
d_quants[f] = true;
return true;
}
}
d_sentLemma = false;
Trace("sets-check") << "Sets finished assertions effort " << level << std::endl;
- if( level == Theory::EFFORT_FULL && !d_conflict && !d_external.d_valuation.needCheck() ){
- fullEffortCheck();
- }
- // invoke the relational solver
- if( !d_conflict && !d_sentLemma && ( level == Theory::EFFORT_FULL || options::setsRelEager() ) ){
- d_rels->check(level);
- //incomplete if we have both cardinality constraints and relational operators?
- // TODO: should internally check model, return unknown if fail
- if( level == Theory::EFFORT_FULL && d_card_enabled && d_rels_enabled ){
- d_external.d_out->setIncomplete();
+ //invoke full effort check, relations check
+ if( !d_conflict ){
+ if( level == Theory::EFFORT_FULL ){
+ if( !d_external.d_valuation.needCheck() ){
+ fullEffortCheck();
+ if( !d_conflict && !d_sentLemma ){
+ //invoke relations solver
+ d_rels->check(level);
+ if( d_card_enabled && d_rels_enabled ){
+ //incomplete if we have both cardinality constraints and relational operators?
+ // TODO: should internally check model, return unknown if fail
+ d_external.d_out->setIncomplete();
+ }
+ }
+ }
+ }else{
+ if( options::setsRelEager() ){
+ d_rels->check(level);
+ }
}
}
Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
int TheorySetsRels::EqcInfo::counter = 0;
void TheorySetsRels::check(Theory::Effort level) {
- Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver *******************************\n" << std::endl;
+ Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver, effort = " << level << " *******************************\n" << std::endl;
if(Theory::fullEffort(level)) {
collectRelsInfo();
check();
void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) {
if( !holds( fact ) ) {
+ Trace("rels-send-lemma") << "[Theory::Rels] **** Generate an infered fact "
+ << fact << " with reason " << exp << " by "<< c << std::endl;
d_pending_facts[fact] = exp;
} else {
- Trace("rels-send-infer") << "[Theory::Rels] **** Generate an infered fact fact = "
- << fact << " with reason = " << exp << " by "<< c
- << ", but it holds already, thus skip it!" << std::endl;
+ Trace("rels-send-lemma-debug") << "[Theory::Rels] **** Generate an infered fact "
+ << fact << " with reason " << exp << " by "<< c
+ << ", but it holds already, thus skip it!" << std::endl;
}
}