Minor cleanup from previous commit. Better organization for how quantifiers modules...

[cvc5.git] / src / theory / quantifiers / quant_conflict_find.cpp

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 4e4d92d2800099fc079e41310dcc5955cc88c4f0..504c3dcffaf1898bcc94e7a92e4535d8dc04f281 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1922,22 +1922,36 @@ void QuantConflictFind::assertDisequal( Node a, Node b ) {
 \r
 //-------------------------------------------------- check function\r
 \r
+bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
+  bool performCheck = false;\r
+  if( options::quantConflictFind() && !d_conflict ){\r
+    if( level==Theory::EFFORT_LAST_CALL ){\r
+      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;\r
+    }else if( level==Theory::EFFORT_FULL ){\r
+      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;\r
+    }else if( level==Theory::EFFORT_STANDARD ){\r
+      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;\r
+    }\r
+  }\r
+  return performCheck;\r
+}\r
+\r
 void QuantConflictFind::reset_round( Theory::Effort level ) {\r
   d_needs_computeRelEqr = true;\r
 }\r
 \r
 /** check */\r
-void QuantConflictFind::check( Theory::Effort level ) {\r
-  Trace("qcf-check") << "QCF : check : " << level << std::endl;\r
-  if( d_conflict ){\r
-    Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;\r
-    if( level>=Theory::EFFORT_FULL ){\r
-      Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;\r
-      //Assert( false );\r
-    }\r
-  }else{\r
-    int addedLemmas = 0;\r
-    if( d_performCheck ){\r
+void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {\r
+  if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){\r
+    Trace("qcf-check") << "QCF : check : " << level << std::endl;\r
+    if( d_conflict ){\r
+      Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;\r
+      if( level>=Theory::EFFORT_FULL ){\r
+        Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;\r
+        //Assert( false );\r
+      }\r
+    }else{\r
+      int addedLemmas = 0;\r
       ++(d_statistics.d_inst_rounds);\r
       double clSet = 0;\r
       int prevEt = 0;\r
@@ -2048,7 +2062,6 @@ void QuantConflictFind::check( Theory::Effort level ) {
           }\r
         }\r
         if( addedLemmas>0 ){\r
-          d_quantEngine->flushLemmas();\r
           break;\r
         }\r
       }\r
@@ -2065,23 +2078,9 @@ void QuantConflictFind::check( Theory::Effort level ) {
           Trace("qcf-engine") << "  Entailment checks = " << ( currEt - prevEt ) << std::endl;\r
         }\r
       }\r
-    }\r
-    Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
-  }\r
-}\r
-\r
-bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
-  d_performCheck = false;\r
-  if( options::quantConflictFind() && !d_conflict ){\r
-    if( level==Theory::EFFORT_LAST_CALL ){\r
-      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;\r
-    }else if( level==Theory::EFFORT_FULL ){\r
-      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;\r
-    }else if( level==Theory::EFFORT_STANDARD ){\r
-      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;\r
+      Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
     }\r
   }\r
-  return d_performCheck;\r
 }\r
 \r
 void QuantConflictFind::computeRelevantEqr() {\r