Make QEffort an enum (#1366)

* Make QEffort an enum.

* Format

* Minor

* Fix

diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index e9c646f0725f6b5b463e51077b384ab0d8ff7898..681c168f26b13d2007cbcc0538a2604dcf30852d 100644 (file)
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -92,8 +92,10 @@ QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe)
 QuantAntiSkolem::~QuantAntiSkolem() { delete d_sqc; }
 
 /* Call during quantifier engine's check */
-void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) {
-  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e)
+{
+  if (quant_e == QEFFORT_STANDARD)
+  {
     d_sqtc.clear();
     for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );

diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h
index 078675420e476a4a7336dedc44777e8acceac80b..bad98c04b7e325a397ba9534ca65cb5bf6dd1bc5 100644 (file)
--- a/src/theory/quantifiers/anti_skolem.h
+++ b/src/theory/quantifiers/anti_skolem.h
@@ -40,7 +40,7 @@ public:
                                bool pconnected = true );
 
   /* Call during quantifier engine's check */
-  void check( Theory::Effort e, unsigned quant_e );
+  void check(Theory::Effort e, QEffort quant_e);
   /* Called for new quantifiers */
   void registerQuantifier( Node q ) {}
   void assertNode( Node n ) {}

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 972b404de179e88d1bd6f138eb1edc6ebc766f97..f99d0b080a3c41d9e73624386c29d0619073bb84 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -350,8 +350,10 @@ bool BoundedIntegers::needsCheck( Theory::Effort e ) {
   return e==Theory::EFFORT_LAST_CALL;
 }
 
-void BoundedIntegers::check( Theory::Effort e, unsigned quant_e ) {
-  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+void BoundedIntegers::check(Theory::Effort e, QEffort quant_e)
+{
+  if (quant_e == QEFFORT_STANDARD)
+  {
     Trace("bint-engine") << "---Bounded Integers---" << std::endl;
     bool addedLemma = false;
     //make sure proxies are up-to-date with range

diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index f0a3a85f5b8bff3940338560f9a839f734041d7f..a91b04ab36a4392dc50721244c25a9d53502be44 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -146,7 +146,7 @@ public:
   
   void presolve();
   bool needsCheck( Theory::Effort e );
-  void check( Theory::Effort e, unsigned quant_e );
+  void check(Theory::Effort e, QEffort quant_e);
   void registerQuantifier( Node q );
   void preRegisterQuantifier( Node q );
   void assertNode( Node n );

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 12c3c8464e435f03189cfc7ec93e483699a00f41..b54ce48057980ac79a5017425af76c3c0d745aa4 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -44,12 +44,15 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
   return e>=Theory::EFFORT_LAST_CALL;
 }
 
-unsigned CegInstantiation::needsModel( Theory::Effort e ) {
-  return d_conj->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
+QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e)
+{
+  return d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL;
 }
 
-void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
-  unsigned echeck = d_conj->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
+void CegInstantiation::check(Theory::Effort e, QEffort quant_e)
+{
+  unsigned echeck =
+      d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL;
   if( quant_e==echeck ){
     Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
     Trace("cegqi-engine-debug") << std::endl;

diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 5e6cb3864681639cd1dfef743cdd3cf9a405b5f2..86f0c4c9ff478d81016b143220738eee9390472f 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -44,9 +44,9 @@ public:
   ~CegInstantiation();
 public:
   bool needsCheck( Theory::Effort e );
-  unsigned needsModel( Theory::Effort e );
+  QEffort needsModel(Theory::Effort e);
   /* Call during quantifier engine's check */
-  void check( Theory::Effort e, unsigned quant_e );
+  void check(Theory::Effort e, QEffort quant_e);
   /* Called for new quantifiers */
   void registerQuantifier( Node q );
   /** get the next decision request */

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index e5a096c87d448c277dad873cca070cbb7baa32f7..b7d1fe404dbad563a6bdc6dfe8a67fa4aa6d149f 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -334,9 +334,10 @@ bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
 void ConjectureGenerator::reset_round( Theory::Effort e ) {
 
 }
-
-void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
-  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
+{
+  if (quant_e == QEFFORT_STANDARD)
+  {
     d_fullEffortCount++;
     if( d_fullEffortCount%optFullCheckFrequency()==0 ){
       d_hasAddedLemma = false;

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index e4246e2ab0775955f958e0782798963d76ec3ec7..a675305569c5f746092b83b96da828f7193716e9 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -407,7 +407,7 @@ public:
   /* reset at a round */
   void reset_round( Theory::Effort e );
   /* Call during quantifier engine's check */
-  void check( Theory::Effort e, unsigned quant_e );
+  void check(Theory::Effort e, QEffort quant_e);
   /* Called for new quantifiers */
   void registerQuantifier( Node q );
   void assertNode( Node n );

diff --git a/src/theory/quantifiers/fun_def_engine.cpp b/src/theory/quantifiers/fun_def_engine.cpp
index 354d90b8baf744285f943579de8604e92f457e72..650a68aa0b9ff2691a3acd6493f12e80fcb39a9b 100644 (file)
--- a/src/theory/quantifiers/fun_def_engine.cpp
+++ b/src/theory/quantifiers/fun_def_engine.cpp
@@ -39,7 +39,8 @@ void FunDefEngine::reset_round( Theory::Effort e ){
 }
 
 /* Call during quantifier engine's check */
-void FunDefEngine::check( Theory::Effort e, unsigned quant_e ) {
+void FunDefEngine::check(Theory::Effort e, QEffort quant_e)
+{
   //TODO
 }
 

diff --git a/src/theory/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h
index ea1dbbc59ef67333fb9de3e2e6162e56f6c28881..48de4f36ce24b329316bc4656e4dae3a3a2cfde9 100644 (file)
--- a/src/theory/quantifiers/fun_def_engine.h
+++ b/src/theory/quantifiers/fun_def_engine.h
@@ -42,7 +42,7 @@ public:
   /* reset at a round */
   void reset_round( Theory::Effort e );
   /* Call during quantifier engine's check */
-  void check( Theory::Effort e, unsigned quant_e );
+  void check(Theory::Effort e, QEffort quant_e);
   /* Called for new quantifiers */
   void registerQuantifier( Node q );
   /** called for everything that gets asserted */

diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 0ae7adfecdc200b704d154938429bb5971c2beb0..3c351cad57c347c344fb80025fdff88be42f13fd 100644 (file)
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -623,7 +623,12 @@ bool InstPropagator::reset( Theory::Effort e ) {
   return d_qy.reset( e );
 }
 
-bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
+bool InstPropagator::notifyInstantiation(QuantifiersModule::QEffort quant_e,
+                                         Node q,
+                                         Node lem,
+                                         std::vector<Node>& terms,
+                                         Node body)
+{
   if( !d_conflict ){
     if( Trace.isOn("qip-prop") ){
       Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl;

diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 580923fc95c5ad4c20ec9961f26d31bf0b100ba2..b8ea2c49ed3f94f7484d840ee0735b9b9adb3fc2 100644 (file)
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -113,14 +113,23 @@ private:
     InstPropagator& d_ip;
   public:
     InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
-    virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
+    virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
+                                     Node q,
+                                     Node lem,
+                                     std::vector<Node>& terms,
+                                     Node body)
+    {
       return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
     }
     virtual void filterInstantiations() { d_ip.filterInstantiations(); }
   };
   InstantiationNotifyInstPropagator d_notify;
   /** notify instantiation method */
-  bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );
+  bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
+                           Node q,
+                           Node lem,
+                           std::vector<Node>& terms,
+                           Node body);
   /** remove instance ids */
   void filterInstantiations();  
   /** allocate instantiation */

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 8b5332c9db5b453efb596c22b490cb4a1adc128c..24a9f1bdf651d6788e6f032919af76965546a874 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -53,14 +53,15 @@ bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
   return e>=Theory::EFFORT_LAST_CALL;
 }
 
-unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) {
+QuantifiersModule::QEffort InstStrategyCbqi::needsModel(Theory::Effort e)
+{
   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
-      return QuantifiersEngine::QEFFORT_STANDARD;
+      return QEFFORT_STANDARD;
     }
   }
-  return QuantifiersEngine::QEFFORT_NONE;
+  return QEFFORT_NONE;
 }
 
 bool InstStrategyCbqi::registerCbqiLemma( Node q ) {
@@ -239,8 +240,10 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
   processResetInstantiationRound( effort );
 }
 
-void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
-  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+void InstStrategyCbqi::check(Theory::Effort e, QEffort quant_e)
+{
+  if (quant_e == QEFFORT_STANDARD)
+  {
     Assert( !d_quantEngine->inConflict() );
     double clSet = 0;
     if( Trace.isOn("cbqi-engine") ){

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index a1e6a2bdc24d535a0d3bb3aac253db5688f33da2..0b23de10d8f02b38d9fd51bb9af98579f1090cb8 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -100,9 +100,9 @@ public:
   bool doCbqi( Node q );
   /** process functions */
   bool needsCheck( Theory::Effort e );
-  unsigned needsModel( Theory::Effort e );
+  QEffort needsModel(Theory::Effort e);
   void reset_round( Theory::Effort e );
-  void check( Theory::Effort e, unsigned quant_e );
+  void check(Theory::Effort e, QEffort quant_e);
   bool checkComplete();
   bool checkCompleteFor( Node q );
   void preRegisterQuantifier( Node q );

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 3bd1ac4952329ddf4676735e8507dda2d5282005..edd15fa2c8c458740d914a65fdbe9b8eb924c8ec 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -55,19 +55,18 @@ bool InstStrategyEnum::needsCheck(Theory::Effort e)
 }
 
 void InstStrategyEnum::reset_round(Theory::Effort e) {}
-void InstStrategyEnum::check(Theory::Effort e, unsigned quant_e)
+void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
 {
   bool doCheck = false;
   bool fullEffort = false;
   if (options::fullSaturateInterleave())
   {
     // we only add when interleaved with other strategies
-    doCheck = quant_e == QuantifiersEngine::QEFFORT_STANDARD
-              && d_quantEngine->hasAddedLemma();
+    doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
   }
   if (options::fullSaturateQuant() && !doCheck)
   {
-    doCheck = quant_e == QuantifiersEngine::QEFFORT_LAST_CALL;
+    doCheck = quant_e == QEFFORT_LAST_CALL;
     fullEffort = !d_quantEngine->hasAddedLemma();
   }
   if (doCheck)

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index d79917eda6b2f5feabb3d2c304152947f20f93e4..cf97518fc0e9e5b6099887d53527166d7090518c 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -71,7 +71,7 @@ class InstStrategyEnum : public QuantifiersModule
    * Adds instantiations for all currently asserted
    * quantified formulas via calls to process(...)
    */
-  void check(Theory::Effort e, unsigned quant_e) override;
+  void check(Theory::Effort e, QEffort quant_e) override;
   /** Register quantifier. */
   void registerQuantifier(Node q) override;
   /** Identify. */

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 22af9dd009158a23b0542b5a4d37a330edf2e896..0c847b597caef33371dce67a09671b37c36395a9 100644 (file)
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -111,9 +111,11 @@ void InstantiationEngine::reset_round( Theory::Effort e ){
   }
 }
 
-void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
+void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
+{
   CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time);
-  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+  if (quant_e == QEFFORT_STANDARD)
+  {
     double clSet = 0;
     if( Trace.isOn("inst-engine") ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);

diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 140ea9250a3687d5fa8ae3888f6cc50c787a52f6..18b5ea19cadaf73612355a871a44dff5cf056892 100644 (file)
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -79,7 +79,7 @@ class InstantiationEngine : public QuantifiersModule {
   void presolve();
   bool needsCheck(Theory::Effort e);
   void reset_round(Theory::Effort e);
-  void check(Theory::Effort e, unsigned quant_e);
+  void check(Theory::Effort e, QEffort quant_e);
   bool checkCompleteFor(Node q);
   void preRegisterQuantifier(Node q);
   void registerQuantifier(Node q);

diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
index e26c464e2ea2daf9ad654b1b78f57236fdf20f31..375754b26ccecb943aac74ad320931d375f9aa4b 100644 (file)
--- a/src/theory/quantifiers/local_theory_ext.cpp
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -128,9 +128,11 @@ bool LtePartialInst::needsCheck( Theory::Effort e ) {
   return e>=Theory::EFFORT_FULL && d_needsCheck;
 }
 /* Call during quantifier engine's check */
-void LtePartialInst::check( Theory::Effort e, unsigned quant_e ) {
+void LtePartialInst::check(Theory::Effort e, QEffort quant_e)
+{
   //flush lemmas ASAP (they are a reduction)
-  if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT && d_needsCheck ){
+  if (quant_e == QEFFORT_CONFLICT && d_needsCheck)
+  {
     std::vector< Node > lemmas;
     getInstantiations( lemmas );
     //add lemmas to quantifiers engine

diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 68b6a562a95df9083ae858d25aa13589487f85e1..3b19b8d5521c81f81747afa98cbba97b7d69c44a 100644 (file)
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -63,7 +63,7 @@ public:
   /* whether this module needs to check this round */
   bool needsCheck( Theory::Effort e );
   /* Call during quantifier engine's check */
-  void check( Theory::Effort e, unsigned quant_e );
+  void check(Theory::Effort e, QEffort quant_e);
   /* Called for new quantifiers */
   void registerQuantifier( Node q ) {}
   /* check complete */

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index c4a0b5c5da02bada196c2b2d7e4c25dd0dce6d52..5d01e04e6acd01f7419ddc0e269174e7eac5a9b3 100644 (file)
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -53,25 +53,26 @@ bool ModelEngine::needsCheck( Theory::Effort e ) {
   return e==Theory::EFFORT_LAST_CALL;
 }
 
-unsigned ModelEngine::needsModel( Theory::Effort e ) {
+QuantifiersModule::QEffort ModelEngine::needsModel(Theory::Effort e)
+{
   if( options::mbqiInterleave() ){
-    return QuantifiersEngine::QEFFORT_STANDARD;
+    return QEFFORT_STANDARD;
   }else{
-    return QuantifiersEngine::QEFFORT_MODEL;
+    return QEFFORT_MODEL;
   }
 }
 
 void ModelEngine::reset_round( Theory::Effort e ) {
   d_incomplete_check = true;
 }
-
-void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
+void ModelEngine::check(Theory::Effort e, QEffort quant_e)
+{
   bool doCheck = false;
   if( options::mbqiInterleave() ){
-    doCheck = quant_e==QuantifiersEngine::QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
+    doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
   }
   if( !doCheck ){
-    doCheck = quant_e==QuantifiersEngine::QEFFORT_MODEL;
+    doCheck = quant_e == QEFFORT_MODEL;
   }
   if( doCheck ){
     Assert( !d_quantEngine->inConflict() );

diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index ad77ae8dc80ecde86c70d3d95eeeaf61712f54b0..840ff424257b813e268b5e0d8664d28f9e0b1eff 100644 (file)
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -50,9 +50,9 @@ public:
   virtual ~ModelEngine();
 public:
   bool needsCheck( Theory::Effort e );
-  unsigned needsModel( Theory::Effort e );
+  QEffort needsModel(Theory::Effort e);
   void reset_round( Theory::Effort e );
-  void check( Theory::Effort e, unsigned quant_e );
+  void check(Theory::Effort e, QEffort quant_e);
   bool checkComplete();
   bool checkCompleteFor( Node q );
   void registerQuantifier( Node f );

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index bd56b9d9ba3414762da37eb4dc84b2f8a363c8fc..baf499d671a3d2439fe67834c02dc386b01f67ba 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2031,9 +2031,11 @@ void QuantConflictFind::setIrrelevantFunction( TNode f ) {
 }
 
 /** check */
-void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
+void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
+{
   CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time);
-  if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
+  if (quant_e == QEFFORT_CONFLICT)
+  {
     Trace("qcf-check") << "QCF : check : " << level << std::endl;
     if( d_conflict ){
       Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 794787bfc93885b8976a1931d750c9b97d84cd2e..0e5fe3c183f4fed4a05cb73dbf2a71121098e919 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -243,8 +243,9 @@ public:
   /** reset round */
   void reset_round( Theory::Effort level );
   /** check */
-  void check( Theory::Effort level, unsigned quant_e );
-private:
+  void check(Theory::Effort level, QEffort quant_e);
+
+ private:
   bool d_needs_computeRelEqr;
 public:
   void computeRelevantEqr();

diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp
index dab95f83b5f11278a3d3273fb16ddc838f668a35..859c4f3ea466f39d7343da427fdd75bb7fb1af2e 100644 (file)
--- a/src/theory/quantifiers/quant_equality_engine.cpp
+++ b/src/theory/quantifiers/quant_equality_engine.cpp
@@ -74,7 +74,8 @@ void QuantEqualityEngine::reset_round( Theory::Effort e ){
 }
 
 /* Call during quantifier engine's check */
-void QuantEqualityEngine::check( Theory::Effort e, unsigned quant_e ) {
+void QuantEqualityEngine::check(Theory::Effort e, QEffort quant_e)
+{
   //TODO
 }
 

diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h
index f827b4fd706debc8126e524ed16d915a53273308..d2e9ec77bc7d2e1ee2278f594c3603b416a2f3d3 100644 (file)
--- a/src/theory/quantifiers/quant_equality_engine.h
+++ b/src/theory/quantifiers/quant_equality_engine.h
@@ -80,7 +80,7 @@ public:
   /* reset at a round */
   void reset_round( Theory::Effort e );
   /* Call during quantifier engine's check */
-  void check( Theory::Effort e, unsigned quant_e );
+  void check(Theory::Effort e, QEffort quant_e);
   /* Called for new quantifiers */
   void registerQuantifier( Node q );
   /** called for everything that gets asserted */

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 282ff3bc4fa84566a53f35a3f7a6be612599ad1b..68a0f30dc876e74102fddf289c0e7ad0d79b9bb2 100644 (file)
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -83,9 +83,11 @@ bool QuantDSplit::checkCompleteFor( Node q ) {
 }
 
 /* Call during quantifier engine's check */
-void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
+void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
+{
   //add lemmas ASAP (they are a reduction)
-  if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
+  if (quant_e == QEFFORT_CONFLICT)
+  {
     std::vector< Node > lemmas;
     for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) {
       Node q = it->first;

diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index daf4114bc097710c9e5915a0e0dd7a562a219768..644583f043ff49e8b25d5304b11e6cedc8177cda 100644 (file)
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -39,7 +39,7 @@ public:
   /* whether this module needs to check this round */
   bool needsCheck( Theory::Effort e );
   /* Call during quantifier engine's check */
-  void check( Theory::Effort e, unsigned quant_e );
+  void check(Theory::Effort e, QEffort quant_e);
   /* Called for new quantifiers */
   void registerQuantifier( Node q ) {}
   void assertNode( Node n ) {}

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index b8e29280d6c82b4d2dea3542c22755269a39d2b5..571c3846a05cc99ef65446fb6a74b522cf27ce2d 100644 (file)
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -25,8 +25,9 @@ using namespace CVC4::context;
 namespace CVC4 {
 namespace theory {
 
-unsigned QuantifiersModule::needsModel( Theory::Effort e ) {
-  return QuantifiersEngine::QEFFORT_NONE;
+QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
+{
+  return QEFFORT_NONE;
 }
 
 eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 95cd7e5e44722446192827e5e9144d7186be2463..f958605b14474a978444ebf7c01dd5f6a537c9dc 100644 (file)
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -40,7 +40,23 @@ namespace quantifiers {
 * It has a similar interface to a Theory object.
 */
 class QuantifiersModule {
-public:
+ public:
+  /** effort levels for quantifiers modules check */
+  enum QEffort
+  {
+    // conflict effort, for conflict-based instantiation
+    QEFFORT_CONFLICT,
+    // standard effort, for heuristic instantiation
+    QEFFORT_STANDARD,
+    // model effort, for model-based instantiation
+    QEFFORT_MODEL,
+    // last call effort, for last resort techniques
+    QEFFORT_LAST_CALL,
+    // none
+    QEFFORT_NONE,
+  };
+
+ public:
   QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
   virtual ~QuantifiersModule(){}
   /** Presolve.
@@ -62,7 +78,7 @@ public:
    * which specifies the quantifiers effort in which it requires the model to
    * be built.
    */
-  virtual unsigned needsModel( Theory::Effort e );
+  virtual QEffort needsModel(Theory::Effort e);
   /** Reset.
    *
    * Called at the beginning of QuantifiersEngine::check(e).
@@ -73,7 +89,7 @@ public:
    *   Called during QuantifiersEngine::check(e) depending
    *   if needsCheck(e) returns true.
    */
-  virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
+  virtual void check(Theory::Effort e, QEffort quant_e) = 0;
   /** Check complete?
    *
    * Returns false if the module's reasoning was globally incomplete

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index b28dca1ed18caa89d020efa0bcad4b85a600ccc1..2c85bceb8c2c7fe9ce7b3656e73ac679c6b903cd 100644 (file)
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -69,8 +69,10 @@ bool RewriteEngine::needsCheck( Theory::Effort e ){
   //return e>=Theory::EFFORT_LAST_CALL;
 }
 
-void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) {
-  if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+void RewriteEngine::check(Theory::Effort e, QEffort quant_e)
+{
+  if (quant_e == QEFFORT_STANDARD)
+  {
     Assert( !d_quantEngine->inConflict() );
     Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl;
     //if( e==Theory::EFFORT_LAST_CALL ){

diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 34994f993e5fac671487e7e2218b7745e6a9ee36..5d19182055e08c75e9fe164c7817ecf3a071c9ec 100644 (file)
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -53,7 +53,7 @@ public:
   ~RewriteEngine() throw() {}
 
   bool needsCheck( Theory::Effort e );
-  void check( Theory::Effort e, unsigned quant_e );
+  void check(Theory::Effort e, QEffort quant_e);
   void registerQuantifier( Node f );
   void assertNode( Node n );
   bool checkCompleteFor( Node q );

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f6b920cda58a41c159a597d5b3ea93fb8ec91126..bc2b533bebb15e4f8656ebc960d2cb4eef16e083 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -120,7 +120,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   }
 
   d_tr_trie = new inst::TriggerTrie;
-  d_curr_effort_level = QEFFORT_NONE;
+  d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
   d_conflict = false;
   d_hasAddedLemma = false;
   d_useModelEe = false;
@@ -444,7 +444,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     return;
   }
   bool needsCheck = !d_lemmas_waiting.empty();
-  unsigned needsModelE = QEFFORT_NONE;
+  QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
   std::vector< QuantifiersModule* > qm;
   if( d_model->checkNeeded() ){
     needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
@@ -454,7 +454,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
         needsCheck = true;
         //can only request model at last call since theory combination can find inconsistencies
         if( e>=Theory::EFFORT_LAST_CALL ){
-          unsigned me = d_modules[i]->needsModel( e );
+          QuantifiersModule::QEffort me = d_modules[i]->needsModel(e);
           needsModelE = me<needsModelE ? me : needsModelE;
         }
       }
@@ -559,7 +559,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
       ++(d_statistics.d_instantiation_rounds);
     }
     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
-    for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){
+    for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT;
+         qef <= QuantifiersModule::QEFFORT_LAST_CALL;
+         ++qef)
+    {
+      QuantifiersModule::QEffort quant_e =
+          static_cast<QuantifiersModule::QEffort>(qef);
       d_curr_effort_level = quant_e;
       //build the model if any module requested it
       if( needsModelE==quant_e && !d_model->isBuilt() ){
@@ -590,7 +595,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
         break;
       }else{
         Assert( !d_conflict );
-        if( quant_e==QEFFORT_CONFLICT ){
+        if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
+        {
           if( e==Theory::EFFORT_FULL ){
             //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
             if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
@@ -601,7 +607,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
           }else if( e==Theory::EFFORT_LAST_CALL ){
             d_ierCounter_lc = d_ierCounter_lc + 1;
           }
-        }else if( quant_e==QEFFORT_MODEL ){
+        }
+        else if (quant_e == QuantifiersModule::QEFFORT_MODEL)
+        {
           if( e==Theory::EFFORT_LAST_CALL ){
             //sources of incompleteness
             if( !d_recorded_inst.empty() ){
@@ -655,7 +663,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
         }
       }
     }
-    d_curr_effort_level = QEFFORT_NONE;
+    d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
     if( d_hasAddedLemma ){
       //debug information
@@ -1293,7 +1301,9 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
         setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 );
       }
     }
-    if( d_curr_effort_level>QEFFORT_CONFLICT && d_curr_effort_level<QEFFORT_NONE ){
+    if (d_curr_effort_level > QuantifiersModule::QEFFORT_CONFLICT
+        && d_curr_effort_level < QuantifiersModule::QEFFORT_NONE)
+    {
       //notify listeners
       for( unsigned j=0; j<d_inst_notify.size(); j++ ){
         if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index ffede2a5bf98367c1616d77f4cfc6939305a25f5..37691488e7f6c816ab2aaa5e09e52589a0b723ea 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -44,7 +44,11 @@ class InstantiationNotify {
 public:
   InstantiationNotify(){}
   virtual ~InstantiationNotify() {}
-  virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
+  virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
+                                   Node q,
+                                   Node lem,
+                                   std::vector<Node>& terms,
+                                   Node body) = 0;
   virtual void filterInstantiations() = 0;
 };
 
@@ -141,8 +145,6 @@ private:
   std::unique_ptr<quantifiers::Skolemize> d_skolemize;
   /** term enumeration utility */
   std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
-
- private:
   /** instantiation engine */
   quantifiers::InstantiationEngine* d_inst_engine;
   /** model engine */
@@ -174,26 +176,17 @@ private:
   /** quantifiers instantiation propagtor */
   quantifiers::InstPropagator * d_inst_prop;
 
- public:  // effort levels (TODO : make an enum and use everywhere #1293)
-  enum {
-    QEFFORT_CONFLICT,
-    QEFFORT_STANDARD,
-    QEFFORT_MODEL,
-    QEFFORT_LAST_CALL,
-    //none
-    QEFFORT_NONE,
-  };
-private:  //this information is reset during check
-  /** current effort level */
-  unsigned d_curr_effort_level;
+ private:  //this information is reset during check
+    /** current effort level */
+  QuantifiersModule::QEffort d_curr_effort_level;
   /** are we in conflict */
   bool d_conflict;
-  context::CDO< bool > d_conflict_c;
+  context::CDO<bool> d_conflict_c;
   /** has added lemma this round */
   bool d_hasAddedLemma;
   /** whether to use model equality engine */
   bool d_useModelEe;
-private:
+ private:
   /** list of all quantifiers seen */
   std::map< Node, bool > d_quants;
   /** quantifiers reduced */