From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 16 Feb 2017 19:26:10 +0000 (-0600)
Subject: Fixes for sets+rels check. Minor.
X-Git-Tag: cvc5-1.0.0~5908
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3a0e9d8d9a1288187db69b103dfd18ad64358f18;p=cvc5.git

Fixes for sets+rels check. Minor.
---

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;
     }
   }