Minor improvement to partial qe. Add options for representative selection in FMF.

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index f214b032c67d7b2fdc5919e97b174c95a3af0a01..152e22f14af2316383bf749f5fd446d9abcba3bc 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -428,7 +428,7 @@ post \n\
 ";
 
 const std::string OptionsHandler::s_macrosQuantHelp = "\
-Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
+Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
 \n\
 all \n\
 + Infer definitions for functions, including those containing quantified formulas.\n\
@@ -442,7 +442,7 @@ ground-uf \n\
 ";
 
 const std::string OptionsHandler::s_quantDSplitHelp = "\
-Template modes for quantifiers splitting, supported by --quant-split:\n\
+Modes for quantifiers splitting, supported by --quant-dsplit-mode:\n\
 \n\
 none \n\
 + Never split quantified formulas.\n\
@@ -455,6 +455,20 @@ agg \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_quantRepHelp = "\
+Modes for quantifiers representative selection, supported by --quant-rep-mode:\n\
+\n\
+ee \n\
++ Let equality engine choose representatives.\n\
+\n\
+first (default) \n\
++ Choose terms that appear first.\n\
+\n\
+depth \n\
++ Choose terms that are of minimal depth.\n\
+\n\
+";
+
 theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg == "pre-full") {
     return theory::quantifiers::INST_WHEN_PRE_FULL;
@@ -716,6 +730,22 @@ theory::quantifiers::QuantDSplitMode OptionsHandler::stringToQuantDSplitMode(std
   }
 }
 
+theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "none" ) {
+    return theory::quantifiers::QUANT_REP_MODE_EE;
+  } else if(optarg == "first" || optarg == "default") {
+    return theory::quantifiers::QUANT_REP_MODE_FIRST;
+  } else if(optarg == "depth") {
+    return theory::quantifiers::QUANT_REP_MODE_DEPTH;
+  } else if(optarg ==  "help") {
+    puts(s_quantRepHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --quant-rep-mode: `") +
+                          optarg + "'.  Try --quant-rep-mode help.");
+  }
+}
+
 // theory/bv/options_handlers.h
 void OptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) {
 #ifndef CVC4_USE_ABC

diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index a2d67be60e3120683684755e7e461468c3055473..720889ca2ad25f028d54bfa77e8e545df1e32578 100644 (file)
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -101,6 +101,7 @@ public:
   theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException);
+  theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, std::string optarg) throw(OptionException);
 
   // theory/bv/options_handlers.h
   void abcEnabledBuild(std::string option, bool value) throw(OptionException);
@@ -201,6 +202,7 @@ public:
   static const std::string s_literalMatchHelp;
   static const std::string s_macrosQuantHelp;
   static const std::string s_quantDSplitHelp;
+  static const std::string s_quantRepHelp;
   static const std::string s_mbqiModeHelp;
   static const std::string s_modelFormatHelp;
   static const std::string s_prenexQuantModeHelp;

diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 7395a9a30843d68b519399b80d9d81a31da293d4..8aa3756cccfc6fc849d9ebd187eba3057bac71c4 100644 (file)
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -172,6 +172,14 @@ enum QuantDSplitMode {
   QUANT_DSPLIT_MODE_AGG,
 };
 
+enum QuantRepMode {
+  /** let equality engine choose representatives */
+  QUANT_REP_MODE_EE,
+  /** default, choose representatives that appear first */
+  QUANT_REP_MODE_FIRST,
+  /** choose representatives that have minimal depth */
+  QUANT_REP_MODE_DEPTH,
+};
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index cba1423a030e53ab91c045da5a944913a7bc6d8b..58367f2e205326eea8359d75fd3d50a4aeef156b 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -100,8 +100,8 @@ option instMaxLevel --inst-max-level=N int :read-write :default -1
  maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
 option instLevelInputOnly --inst-level-input-only bool :default true
  only input terms are assigned instantiation level zero
-option internalReps --quant-internal-reps bool :default true
- instantiate with representatives chosen by quantifiers engine
+option quantRepMode --quant-rep-mode=MODE  CVC4::theory::quantifiers::QuantRepMode :default CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST :read-write :include "options/quantifiers_modes.h" :handler stringToQuantRepMode
+ selection mode for representatives in quantifiers engine
  
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index e6c9b9e6be578bfc5b07524d1986535f4123edcf..faad18c281c1d74a91c0c403a38e2968a47079c7 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -34,7 +34,9 @@ using namespace CVC4::theory::arith;
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 
 InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
-  : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), d_added_inst( qe->getUserContext() ) {
+  : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() )
+//, d_added_inst( qe->getUserContext() ) 
+{
 }
 
 InstStrategyCbqi::~InstStrategyCbqi() throw(){}
@@ -97,14 +99,6 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
         }else{
           Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
         }
-        //if doing partial quantifier elimination, do not process this if already processed once
-        if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) ){
-          if( d_added_inst.find( q )!=d_added_inst.end() ){
-            d_quantEngine->getModel()->setQuantifierActive( q, false );
-            d_cbqi_set_quant_inactive = true;
-            d_incomplete_check = true;
-          }
-        }
       }
     }
   }
@@ -597,21 +591,23 @@ InstStrategyCegqi::~InstStrategyCegqi() throw () {
 }
 
 void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
-  d_check_vts_lemma_lc = true;
+  d_check_vts_lemma_lc = false;
 }
 
-void InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
+void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
   if( e==0 ){
-    CegInstantiator * cinst = getInstantiator( f );
-    Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
-    d_curr_quant = f;
+    CegInstantiator * cinst = getInstantiator( q );
+    Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
+    d_curr_quant = q;
     if( !cinst->check() ){
       d_incomplete_check = true;
+      d_check_vts_lemma_lc = true;
     }
     d_curr_quant = Node::null();
   }else if( e==1 ){
     //minimize the free delta heuristically on demand
     if( d_check_vts_lemma_lc ){
+      Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
       d_check_vts_lemma_lc = false;
       d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
       d_small_const = Rewriter::rewrite( d_small_const );
@@ -635,13 +631,21 @@ void InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
 
 bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) {
   Assert( !d_curr_quant.isNull() );
-  //check if we need virtual term substitution (if used delta or infinity)
-  bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
-  if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){
-    d_added_inst.insert( d_curr_quant );
+  //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
+  if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){
+    d_cbqi_set_quant_inactive = true;
+    d_incomplete_check = true;
+    d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
     return true;
   }else{
-    return false;
+    //check if we need virtual term substitution (if used delta or infinity)
+    bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
+    if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){
+      //d_added_inst.insert( d_curr_quant );
+      return true;
+    }else{
+      return false;
+    }
   }
 }
 

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 8de844eb822ee296abae0b8e1018280dcd5b94b5..fd8afb1496836d35a561f15782e300c589a3164d 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -40,7 +40,7 @@ protected:
   /** whether we have added cbqi lemma */
   NodeSet d_added_cbqi_lemma;
   /** whether we have instantiated quantified formulas */
-  NodeSet d_added_inst;
+  //NodeSet d_added_inst;
   /** whether to do cbqi for this quantified formula */
   std::map< Node, bool > d_do_cbqi;
   /** register ce lemma */

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cb23b8bb7afce1df39d75a9c395dc7abec81eff0..be0f60654719cd8259a3f2e56113c4fb6fd49ed0 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1680,6 +1680,21 @@ bool TermDb::containsTerms( Node n, std::vector< Node >& t ) {
   }
 }
 
+int TermDb::getTermDepth( Node n ) {
+  if (!n.hasAttribute(TermDepthAttribute()) ){
+    int maxDepth = -1;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      int depth = getTermDepth( n[i] );
+      if( depth>maxDepth ){
+        maxDepth = depth;
+      }
+    }
+    TermDepthAttribute tda;
+    n.setAttribute(tda,1+maxDepth);
+  }
+  return n.getAttribute(TermDepthAttribute());
+}
+
 bool TermDb::containsUninterpretedConstant( Node n ) {
   std::map< Node, bool > visited;
   return containsUninterpretedConstant2( n, visited );

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 5560098c9ab7ebc59205f85f07f3f817efef5543..b1cfcf2aef3af8375df51a2494aa63b16d14eb56 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -68,6 +68,9 @@ typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
 struct InstVarNumAttributeId {};
 typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
 
+struct TermDepthAttributeId {};
+typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute;
+
 struct ModelBasisAttributeId {};
 typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
 //for APPLY_UF terms, 1 : term has direct child with model basis attribute,
@@ -436,6 +439,8 @@ public:
   static bool containsTerms( Node n, std::vector< Node >& t );
   /** contains uninterpreted constant */
   static bool containsUninterpretedConstant( Node n );
+  /** get the term depth of n */
+  static int getTermDepth( Node n );
   /** simple negate */
   static Node simpleNegate( Node n );
   /** is assoc */

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index bbc41278e4d8fe8ab1e68490538dd52abf0a177c..9568966d617c48aaca599a946e74e6a37c87db5c 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -741,6 +741,24 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v
   }
 }
 
+bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst ) {
+  if( options::incrementalSolving() ){
+    Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
+    inst::CDInstMatchTrie* imt;
+    std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
+    if( it!=d_c_inst_match_trie.end() ){
+      imt = it->second;
+    }else{
+      imt = new CDInstMatchTrie( getUserContext() );
+      d_c_inst_match_trie[q] = imt;
+    }
+    return imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst );
+  }else{
+    Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+    return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst );
+  }
+}
+
 void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){
   Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level << std::endl;
   //if not from the vector of terms we instantiatied
@@ -956,22 +974,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
   }
 
   //check for duplication
-  bool alreadyExists = false;
-  if( options::incrementalSolving() ){
-    Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
-    inst::CDInstMatchTrie* imt;
-    std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
-    if( it!=d_c_inst_match_trie.end() ){
-      imt = it->second;
-    }else{
-      imt = new CDInstMatchTrie( getUserContext() );
-      d_c_inst_match_trie[q] = imt;
-    }
-    alreadyExists = !imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst );
-  }else{
-    Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
-    alreadyExists = !d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst );
-  }
+  bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst );
   if( alreadyExists ){
     Trace("inst-add-debug") << " -> Already exists." << std::endl;
     ++(d_statistics.d_inst_duplicate_eq);
@@ -1260,27 +1263,27 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
 Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
   Assert( f.isNull() || f.getKind()==FORALL );
   Node r = getRepresentative( a );
-  if( !options::internalReps() ){
-    return r;
-  }else{
-    if( options::finiteModelFind() ){
-      if( r.isConst() ){
-        //map back from values assigned by model, if any
-        if( d_qe->getModel() ){
-          std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
-          if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
-            r = it->second;
-            r = getRepresentative( r );
-          }else{
-            if( r.getType().isSort() ){
-              Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
-              //should never happen : UF constants should never escape model
-              Assert( false );
-            }
+  if( options::finiteModelFind() ){
+    if( r.isConst() ){
+      //map back from values assigned by model, if any
+      if( d_qe->getModel() ){
+        std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
+        if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
+          r = it->second;
+          r = getRepresentative( r );
+        }else{
+          if( r.getType().isSort() ){
+            Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
+            //should never happen : UF constants should never escape model
+            Assert( false );
           }
         }
       }
     }
+  }
+  if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){
+    return r;
+  }else{
     TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
     std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
     if( itir==d_int_rep[v_tn].end() ){
@@ -1320,7 +1323,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
       if( d_rep_score.find( r_best )==d_rep_score.end() ){
         d_rep_score[ r_best ] = d_reset_count;
       }
-      Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
+      Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl;
       Assert( r_best.getType().isSubtypeOf( v_tn ) );
       d_int_rep[v_tn][r] = r_best;
       if( r_best!=a ){
@@ -1446,23 +1449,6 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod
   }
 }
 
-/*
-int getDepth( Node n ){
-  if( n.getNumChildren()==0 ){
-    return 0;
-  }else{
-    int maxDepth = -1;
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      int depth = getDepth( n[i] );
-      if( depth>maxDepth ){
-        maxDepth = depth;
-      }
-    }
-    return maxDepth;
-  }
-}
-*/
-
 //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
 int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
   if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){  //reject
@@ -1479,8 +1465,12 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, Type
       return options::instLevelInputOnly() ? -1 : 0;
     }
   }else{
-    //score prefers earliest use of this term as a representative
-    return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
+    if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){
+      //score prefers earliest use of this term as a representative
+      return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
+    }else{
+      Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH );
+      return quantifiers::TermDb::getTermDepth( n );
+    }
   }
-  //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n );    //term depth
 }

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index c5c88487bfc7f69c2958528401042addcef4b6e7..b9ce2063a831fbc8d57ac1911103fc7d2ea5b898 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -99,6 +99,7 @@ namespace quantifiers {
   class QuantEqualityEngine;
   class FullSaturation;
   class InstStrategyCbqi;
+  class InstStrategyCegqi;
   class QuantDSplit;
 }/* CVC4::theory::quantifiers */
 
@@ -111,6 +112,7 @@ class EqualityQueryQuantifiersEngine;
 
 class QuantifiersEngine {
   friend class quantifiers::InstantiationEngine;
+  friend class quantifiers::InstStrategyCegqi;
   friend class quantifiers::ModelEngine;
   friend class quantifiers::RewriteEngine;
   friend class quantifiers::QuantConflictFind;
@@ -292,6 +294,8 @@ private:
   void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
   /** instantiate f with arguments terms */
   bool addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
+  /** record instantiation, return true if it was non-duplicate */
+  bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false );
   /** set instantiation level attr */
   static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
   /** flush lemmas */

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a4ebe5e978e503320c98f58f4f5414c1d261ba4c..175bd2c2ad9818279102a1cc4bbe19ad39cd30e4 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2027,6 +2027,7 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
                         Trace("strings-entail") << "  explanation was : " << et.second << std::endl;
                         conc = e==0 ? eq1 : eq2;
                         antec_new_lits.push_back( et.second );
+                        break;
                       }
                     }
                   }