Fixes for sets+rels check. Minor.

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2d79826a6451a1f68a1b300a4928201b48e060af..573c97f00dd6e09a4c353d15c1351ba44a29310f 100644 (file)
--- 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 d3c596664e4b4713edf40657def56d94af2d68fb..edd63bddc9cb4c11a85f9f21f3c851e3bae52f72 100644 (file)
--- 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 a0a929ff944e5141bb28cd5d4b99a97ef111726a..ac5463e13a9304d13fac0e19015963db505c5e4f 100644 (file)
--- 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;
     }
   }