Add stats to quantifiers conflict find. Added option for qcf. Working on handling...

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index bc717bbbc5b05720f74debe44e81689f0469d4f9..9e3e77c8e5a10d19fa4d7b1495a6b99d6ce9df67 100644 (file)
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -242,7 +242,6 @@ int ModelEngine::checkModel(){
   Trace("model-engine-debug") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
   Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
   Trace("model-engine") << d_totalLemmas << std::endl;
-  d_statistics.d_exh_inst_lemmas += d_addedLemmas;
   return d_addedLemmas;
 }
 
@@ -256,6 +255,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     d_triedLemmas += d_builder->d_triedLemmas;
     d_addedLemmas += d_builder->d_addedLemmas;
     d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check;
+    d_statistics.d_mbqi_inst_lemmas += d_builder->d_addedLemmas;
   }else{
     Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
     Debug("inst-fmf-ei") << "   Instantiation Constants: ";
@@ -287,6 +287,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
       }
       d_addedLemmas += addedLemmas;
       d_triedLemmas += triedLemmas;
+      d_statistics.d_exh_inst_lemmas += addedLemmas;
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
     d_incomplete_check = d_incomplete_check || riter.d_incomplete;
@@ -310,15 +311,18 @@ void ModelEngine::debugPrint( const char* c ){
 
 ModelEngine::Statistics::Statistics():
   d_inst_rounds("ModelEngine::Inst_Rounds", 0),
-  d_exh_inst_lemmas("ModelEngine::Exhaustive_Instantiation_Lemmas", 0 )
+  d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ),
+  d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 )
 {
   StatisticsRegistry::registerStat(&d_inst_rounds);
   StatisticsRegistry::registerStat(&d_exh_inst_lemmas);
+  StatisticsRegistry::registerStat(&d_mbqi_inst_lemmas);
 }
 
 ModelEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_inst_rounds);
   StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas);
+  StatisticsRegistry::unregisterStat(&d_mbqi_inst_lemmas);
 }
 
 

diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index fcbba7aee30c057e166bb075b4ceb8a66a5f01ff..ba54d7ba4ebec6f0236c12f2bd045ecedead5b29 100644 (file)
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -68,6 +68,7 @@ public:
   public:
     IntStat d_inst_rounds;
     IntStat d_exh_inst_lemmas;
+    IntStat d_mbqi_inst_lemmas;
     Statistics();
     ~Statistics();
   };

diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index d5c755ad20d5492db98b6d26be2b96d97349efd6..7a7ce9b5400ca440cf060e6ef34c5241a6823bcd 100644 (file)
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -70,7 +70,14 @@ typedef enum {
   MBQI_INTERVAL,
 } MbqiMode;
 
-
+typedef enum {
+  /** default, apply at full effort */
+  QCF_WHEN_MODE_DEFAULT,
+  /** apply at standard effort */
+  QCF_WHEN_MODE_STD,
+  /** default */
+  QCF_WHEN_MODE_STD_H,
+} QcfWhenMode;
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 652526cc9f4bececea55c8436c1daeae4779d1d3..dc016be3f3751a565887ca2c5f26fa9c5b077ffa 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -120,6 +120,9 @@ option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode
  policy for instantiating axioms
 
 option quantConflictFind --quant-cf bool :default false
- enable eager conflict find mechanism for quantifiers
+ enable conflict find mechanism for quantifiers
+option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h"
+ when to invoke conflict find mechanism for quantifiers
+
 
 endmodule

diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 4929fa60b913455992561b91b5e36d3ef71ff43f..e0b1e30e8732bd4b782c36777849010b6728422d 100644 (file)
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -97,6 +97,19 @@ interval \n\
 + Use algorithm that abstracts domain elements as intervals. \n\
 \n\
 ";
+static const std::string qcfWhenModeHelp = "\
+Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\
+\n\
+default \n\
++ Default, apply conflict finding at full effort.\n\
+\n\
+std \n\
++ Apply conflict finding at standard effort.\n\
+\n\
+std-h \n\
++ Apply conflict finding at standard effort when heuristic says to. \n\
+\n\
+";
 
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
@@ -186,6 +199,22 @@ inline void checkMbqiMode(std::string option, MbqiMode mode, SmtEngine* smt) thr
 
 }
 
+inline QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "default") {
+    return QCF_WHEN_MODE_DEFAULT;
+  } else if(optarg ==  "std") {
+    return QCF_WHEN_MODE_STD;
+  } else if(optarg ==  "std-h") {
+    return QCF_WHEN_MODE_STD_H;
+  } else if(optarg ==  "help") {
+    puts(qcfWhenModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --quant-cf-when: `") +
+                          optarg + "'.  Try --quant-cf-when help.");
+  }
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 58840989d365e69e7e977105e57727d8172696fc..1bf53db9149ce65ac32598b0008c199e78a13762 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -306,18 +306,20 @@ EqRegistry * QuantConflictFind::getEqRegistry( bool polarity, Node lit, bool doC
 void QuantConflictFind::getEqRegistryApps( Node lit, std::vector< Node >& terms ) {\r
   Assert( quantifiers::TermDb::hasBoundVarAttr( lit ) );\r
   if( lit.getKind()==EQUAL ){\r
+    bool allUf = false;\r
     for( unsigned i=0; i<2; i++ ){\r
       if( quantifiers::TermDb::hasBoundVarAttr( lit[i] ) ){\r
-        if( lit[i].getKind()==APPLY_UF ){\r
-          terms.push_back( lit[i] );\r
-        }else if( lit[i].getKind()==BOUND_VARIABLE ){\r
+        if( lit[i].getKind()==BOUND_VARIABLE ){\r
           //do not handle variable equalities\r
           terms.clear();\r
           return;\r
+        }else{\r
+          allUf = allUf && lit[i].getKind()==APPLY_UF;\r
+          terms.push_back( lit[i] );\r
         }\r
       }\r
     }\r
-    if( terms.size()==2 && isLessThan( terms[1], terms[0] ) ){\r
+    if( terms.size()==2 && allUf && isLessThan( terms[1], terms[0] ) ){\r
       Node t = terms[0];\r
       terms[0] = terms[1];\r
       terms[1] = t;\r
@@ -544,7 +546,8 @@ void QuantConflictFind::check( Theory::Effort level ) {
     Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;\r
   }else{\r
     bool addedLemma = false;\r
-    if( level==Theory::EFFORT_FULL ){\r
+    if( d_performCheck ){\r
+      ++(d_statistics.d_inst_rounds);\r
       double clSet = 0;\r
       if( Trace.isOn("qcf-engine") ){\r
         clSet = double(clock())/double(CLOCKS_PER_SEC);\r
@@ -648,6 +651,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
                   d_quantEngine->flushLemmas();\r
                   d_conflict.set( true );\r
                   addedLemma = true;\r
+                  ++(d_statistics.d_conflict_inst);\r
                   break;\r
                 }else{\r
                   Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;\r
@@ -678,7 +682,11 @@ void QuantConflictFind::check( Theory::Effort level ) {
 }\r
 \r
 bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
-  return !d_conflict && level==Theory::EFFORT_FULL;\r
+  d_performCheck = false;\r
+  if( !d_conflict && level==Theory::EFFORT_FULL ){\r
+    d_performCheck = true;\r
+  }\r
+  return d_performCheck;\r
 }\r
 \r
 void QuantConflictFind::computeRelevantEqr() {\r
@@ -1091,7 +1099,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
       d_n = n;\r
       qni_apps.push_back( n );\r
     }else{\r
-      //unknown term\r
+      //for now, unknown term\r
       d_type = typ_invalid;\r
     }\r
   }else{\r
@@ -1143,10 +1151,20 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
         if( d_n.getKind()==APPLY_UF || d_n.getKind()==EQUAL ){\r
           //get the applications (in order) that will be matching\r
           p->getEqRegistryApps( d_n, qni_apps );\r
+          bool isValid = true;\r
           if( qni_apps.size()>0 ){\r
-            d_type =typ_valid_lit;\r
+            for( unsigned i=0; i<qni_apps.size(); i++ ){\r
+              if( qni_apps[i].getKind()!=APPLY_UF ){\r
+                //for now, cannot handle anything besides uf\r
+                isValid = false;\r
+                qni_apps.clear();\r
+                break;\r
+              }\r
+            }\r
+            if( isValid ){\r
+              d_type = typ_valid_lit;\r
+            }\r
           }else if( d_n.getKind()==EQUAL ){\r
-            bool isValid = true;\r
             for( unsigned i=0; i<2; i++ ){\r
               if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) && !p->d_qinfo[q].isVar( d_n[i] ) ){\r
                 isValid = false;\r
@@ -1172,13 +1190,12 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
         for( unsigned i=0; i<d_children.size(); i++ ){\r
           d_children_order.push_back( i );\r
         }\r
-        if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){\r
+        //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){\r
           //sort based on the type of the constraint : ground comes first, then literals, then others\r
           //MatchGenSort mgs;\r
           //mgs.d_mg = this;\r
-          //std::sort( d_children_order.begin(), d_children_order.end(), mbas );\r
-\r
-        }\r
+          //std::sort( d_children_order.begin(), d_children_order.end(), mgs );\r
+        //}\r
       }\r
       if( isTop ){\r
         int base = d_children.size();\r
@@ -1709,4 +1726,17 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
   }\r
 }\r
 \r
+QuantConflictFind::Statistics::Statistics():\r
+  d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),\r
+  d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 )\r
+{\r
+  StatisticsRegistry::registerStat(&d_inst_rounds);\r
+  StatisticsRegistry::registerStat(&d_conflict_inst);\r
+}\r
+\r
+QuantConflictFind::Statistics::~Statistics(){\r
+  StatisticsRegistry::unregisterStat(&d_inst_rounds);\r
+  StatisticsRegistry::unregisterStat(&d_conflict_inst);\r
+}\r
+\r
 }
\ No newline at end of file

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index a43e2f70d088a57fed7c026bb5c5a866eef7d781..930b6ea52dc1809665df79a0be404c3cf904c5e6 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -76,6 +76,7 @@ class QuantConflictFind : public QuantifiersModule
 private:\r
   context::Context* d_c;\r
   context::CDO< bool > d_conflict;\r
+  bool d_performCheck;\r
   //void registerAssertion( Node n );\r
   void registerQuant( Node q, Node n, bool hasPol, bool pol );\r
   void flatten( Node q, Node n );\r
@@ -226,6 +227,16 @@ private:
   std::map< Node, int > d_quant_id;\r
   void debugPrintQuant( const char * c, Node q );\r
   void debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum = true );\r
+public:\r
+  /** statistics class */\r
+  class Statistics {\r
+  public:\r
+    IntStat d_inst_rounds;\r
+    IntStat d_conflict_inst;\r
+    Statistics();\r
+    ~Statistics();\r
+  };\r
+  Statistics d_statistics;\r
 };\r
 \r
 }\r