Add stats to quantifiers conflict find. Added option for qcf. Working on handling non-APPLY_UF terms.

7 files changed, 102 insertions, 17 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index bc717bbbc..9e3e77c8e 100644
--- 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 fcbba7aee..ba54d7ba4 100644
--- 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 d5c755ad2..7a7ce9b54 100644
--- 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 652526cc9..dc016be3f 100644
--- 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 4929fa60b..e0b1e30e8 100644
--- 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 58840989d..1bf53db91 100755
--- 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 ) {

   Assert( quantifiers::TermDb::hasBoundVarAttr( lit ) );

   if( lit.getKind()==EQUAL ){

+    bool allUf = false;

     for( unsigned i=0; i<2; i++ ){

       if( quantifiers::TermDb::hasBoundVarAttr( lit[i] ) ){

-        if( lit[i].getKind()==APPLY_UF ){

-          terms.push_back( lit[i] );

-        }else if( lit[i].getKind()==BOUND_VARIABLE ){

+        if( lit[i].getKind()==BOUND_VARIABLE ){

           //do not handle variable equalities

           terms.clear();

           return;

+        }else{

+          allUf = allUf && lit[i].getKind()==APPLY_UF;

+          terms.push_back( lit[i] );

         }

       }

     }

-    if( terms.size()==2 && isLessThan( terms[1], terms[0] ) ){

+    if( terms.size()==2 && allUf && isLessThan( terms[1], terms[0] ) ){

       Node t = terms[0];

       terms[0] = terms[1];

       terms[1] = t;

@@ -544,7 +546,8 @@ void QuantConflictFind::check( Theory::Effort level ) {
     Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;

   }else{

     bool addedLemma = false;

-    if( level==Theory::EFFORT_FULL ){

+    if( d_performCheck ){

+      ++(d_statistics.d_inst_rounds);

       double clSet = 0;

       if( Trace.isOn("qcf-engine") ){

         clSet = double(clock())/double(CLOCKS_PER_SEC);

@@ -648,6 +651,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
                   d_quantEngine->flushLemmas();

                   d_conflict.set( true );

                   addedLemma = true;

+                  ++(d_statistics.d_conflict_inst);

                   break;

                 }else{

                   Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;

@@ -678,7 +682,11 @@ void QuantConflictFind::check( Theory::Effort level ) {
 }

 

 bool QuantConflictFind::needsCheck( Theory::Effort level ) {

-  return !d_conflict && level==Theory::EFFORT_FULL;

+  d_performCheck = false;

+  if( !d_conflict && level==Theory::EFFORT_FULL ){

+    d_performCheck = true;

+  }

+  return d_performCheck;

 }

 

 void QuantConflictFind::computeRelevantEqr() {

@@ -1091,7 +1099,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
       d_n = n;

       qni_apps.push_back( n );

     }else{

-      //unknown term

+      //for now, unknown term

       d_type = typ_invalid;

     }

   }else{

@@ -1143,10 +1151,20 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
         if( d_n.getKind()==APPLY_UF || d_n.getKind()==EQUAL ){

           //get the applications (in order) that will be matching

           p->getEqRegistryApps( d_n, qni_apps );

+          bool isValid = true;

           if( qni_apps.size()>0 ){

-            d_type =typ_valid_lit;

+            for( unsigned i=0; i<qni_apps.size(); i++ ){

+              if( qni_apps[i].getKind()!=APPLY_UF ){

+                //for now, cannot handle anything besides uf

+                isValid = false;

+                qni_apps.clear();

+                break;

+              }

+            }

+            if( isValid ){

+              d_type = typ_valid_lit;

+            }

           }else if( d_n.getKind()==EQUAL ){

-            bool isValid = true;

             for( unsigned i=0; i<2; i++ ){

               if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) && !p->d_qinfo[q].isVar( d_n[i] ) ){

                 isValid = false;

@@ -1172,13 +1190,12 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
         for( unsigned i=0; i<d_children.size(); i++ ){

           d_children_order.push_back( i );

         }

-        if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){

+        //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){

           //sort based on the type of the constraint : ground comes first, then literals, then others

           //MatchGenSort mgs;

           //mgs.d_mg = this;

-          //std::sort( d_children_order.begin(), d_children_order.end(), mbas );

-

-        }

+          //std::sort( d_children_order.begin(), d_children_order.end(), mgs );

+        //}

       }

       if( isTop ){

         int base = d_children.size();

@@ -1709,4 +1726,17 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
   }

 }

 

+QuantConflictFind::Statistics::Statistics():

+  d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),

+  d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 )

+{

+  StatisticsRegistry::registerStat(&d_inst_rounds);

+  StatisticsRegistry::registerStat(&d_conflict_inst);

+}

+

+QuantConflictFind::Statistics::~Statistics(){

+  StatisticsRegistry::unregisterStat(&d_inst_rounds);

+  StatisticsRegistry::unregisterStat(&d_conflict_inst);

+}

+

 }
\ 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 a43e2f70d..930b6ea52 100755
--- 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:

   context::Context* d_c;

   context::CDO< bool > d_conflict;

+  bool d_performCheck;

   //void registerAssertion( Node n );

   void registerQuant( Node q, Node n, bool hasPol, bool pol );

   void flatten( Node q, Node n );

@@ -226,6 +227,16 @@ private:
   std::map< Node, int > d_quant_id;

   void debugPrintQuant( const char * c, Node q );

   void debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum = true );

+public:

+  /** statistics class */

+  class Statistics {

+  public:

+    IntStat d_inst_rounds;

+    IntStat d_conflict_inst;

+    Statistics();

+    ~Statistics();

+  };

+  Statistics d_statistics;

 };

 

 }