diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-16 13:26:10 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-16 13:26:10 -0600 |
commit | 3a0e9d8d9a1288187db69b103dfd18ad64358f18 (patch) | |
tree | 80efb64a7fcbdcde4e5097a9ee4d72d34b4d0ee9 /src | |
parent | 4604e6119a0a5e968e47cf23ce93b09c17a726b8 (diff) |
Fixes for sets+rels check. Minor.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 29 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 10 |
3 files changed, 26 insertions, 14 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2d79826a6..573c97f00 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -724,6 +724,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ //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; } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index d3c596664..edd63bddc 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1532,16 +1532,25 @@ void TheorySetsPrivate::check(Theory::Effort level) { } 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; diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index a0a929ff9..ac5463e13 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -34,7 +34,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > 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(); @@ -862,11 +862,13 @@ int TheorySetsRels::EqcInfo::counter = 0; 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; } } |