Do not enforce dt fairness when single invocation sygus.

diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015
index c66ee11c63f71739d003d507d8a5fbd7da73d346..4cfe5acd94fab35f128fc1fd3b75f9fef0857399 100644 (file)
--- a/contrib/run-script-smtcomp2015
+++ b/contrib/run-script-smtcomp2015
@@ -55,7 +55,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
   trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality
   trywith 30 --inst-when=full --full-saturate-quant
   trywith 30 --fmf-bound-int --macros-quant
-  trywith 30 --no-inst-no-entail --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+  trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
   trywith 30 --decision=justification-stoponly --full-saturate-quant
   # large runs 3min
   trywith 60 --term-db-mode=relevant --full-saturate-quant

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 5e6bcf0b4dd0f5f6f71da142a6c65404df639d15..aaab8f3f915ed94ab550b83d8215103233d21240 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -112,7 +112,7 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
       qe->getOutputChannel().lemma( lem );
       qe->getOutputChannel().requirePhase( lit, true );
 
-      if( options::ceGuidedInstFair()==CEGQI_FAIR_DT_HEIGHT_PRED ){
+      if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){
         //implies height bounds on each candidate variable
         std::vector< Node > lem_c;
         for( unsigned j=0; j<d_candidates.size(); j++ ){
@@ -129,6 +129,14 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
   }
 }
 
+CegqiFairMode CegConjecture::getCegqiFairMode() {
+  return isSingleInvocation() ? CEGQI_FAIR_NONE : options::ceGuidedInstFair();
+}
+
+bool CegConjecture::isSingleInvocation() {
+  return d_ceg_si->isSingleInvocation();
+}
+
 CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
   d_conj = new CegConjecture( qe->getSatContext() );
   d_last_inst_si = false;
@@ -139,7 +147,7 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
 }
 
 unsigned CegInstantiation::needsModel( Theory::Effort e ) {
-  return QuantifiersEngine::QEFFORT_MODEL;  
+  return QuantifiersEngine::QEFFORT_MODEL;
 }
 
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
@@ -161,21 +169,21 @@ void CegInstantiation::registerQuantifier( Node q ) {
       d_conj->assign( d_quantEngine, q );
 
       //fairness
-      if( options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){
+      if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
         std::vector< Node > mc;
         for( unsigned j=0; j<d_conj->d_candidates.size(); j++ ){
           TypeNode tn = d_conj->d_candidates[j].getType();
-          if( options::ceGuidedInstFair()==CEGQI_FAIR_DT_SIZE ){
+          if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE ){
             if( tn.isDatatype() ){
               mc.push_back( NodeManager::currentNM()->mkNode( DT_SIZE, d_conj->d_candidates[j] ) );
             }
-          }else if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){
+          }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){
             registerMeasuredType( tn );
             std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn );
             if( it!=d_uf_measure.end() ){
               mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) );
             }
-          }else if( options::ceGuidedInstFair()==CEGQI_FAIR_DT_HEIGHT_PRED ){
+          }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){
             //measure term is a fresh constant
             mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) );
           }
@@ -208,15 +216,15 @@ Node CegInstantiation::getNextDecisionRequest() {
   d_conj->initializeGuard( d_quantEngine );
   bool value;
   if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
-    if( d_conj->d_guard_split.isNull() ){
-      Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
-      d_quantEngine->getOutputChannel().lemma( lem );
-    }
+    //if( d_conj->d_guard_split.isNull() ){
+    //  Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
+    //  d_quantEngine->getOutputChannel().lemma( lem );
+    //}
     Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
     return d_conj->d_guard;
   }
   //enforce fairness
-  if( d_conj->isAssigned() && options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){
+  if( d_conj->isAssigned() && d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
     Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
     if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
       if( !value ){
@@ -242,7 +250,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
     Trace("cegqi-engine-debug") << conj->d_candidates[i] << " ";
   }
   Trace("cegqi-engine-debug") << std::endl;
-  if( options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){
+  if( conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
     Trace("cegqi-engine") << "  * Current term size : " << conj->d_curr_lit.get() << std::endl;
   }
 
@@ -266,7 +274,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       std::vector< Node > model_values;
       if( getModelValues( conj, conj->d_candidates, model_values ) ){
         //check if we must apply fairness lemmas
-        if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){
+        if( conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){
           std::vector< Node > lems;
           for( unsigned j=0; j<conj->d_candidates.size(); j++ ){
             getMeasureLemmas( conj->d_candidates[j], model_values[j], lems );

diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 52e1107207b47a56731179527e6e3123bb20cd95..09e449b356d8ab27cb51ab454ef6a4ff4ea14687 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -21,6 +21,7 @@
 #include "context/cdchunk_list.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/ce_guided_single_inv.h"
+#include "theory/quantifiers/modes.h"
 
 namespace CVC4 {
 namespace theory {
@@ -49,7 +50,7 @@ public:
   /** list of constants for quantified formula */
   std::vector< Node > d_candidates;
   /** list of variables on inner quantification */
-  std::vector< Node > d_inner_vars;    
+  std::vector< Node > d_inner_vars;
   std::vector< std::vector< Node > > d_inner_vars_disj;
   /** list of terms we have instantiated candidates with */
   std::map< int, std::vector< Node > > d_candidate_inst;
@@ -78,9 +79,13 @@ public:  //for fairness
   Node getLiteral( QuantifiersEngine * qe, int i );
   /** is ground */
   bool isGround() { return d_inner_vars.empty(); }
+  /** fairness */
+  CegqiFairMode getCegqiFairMode();
+  /** is single invocation */
+  bool isSingleInvocation();
 };
-  
-  
+
+
 class CegInstantiation : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
@@ -128,7 +133,7 @@ public:
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const { return "CegInstantiation"; }
   /** print solution for synthesis conjectures */
-  void printSynthSolution( std::ostream& out );  
+  void printSynthSolution( std::ostream& out );
   /** collect disjuncts */
   static void collectDisjuncts( Node n, std::vector< Node >& ex );
 public:
@@ -139,7 +144,7 @@ public:
     IntStat d_cegqi_si_lemmas;
     Statistics();
     ~Statistics();
-  };/* class CegInstantiation::Statistics */  
+  };/* class CegInstantiation::Statistics */
   Statistics d_statistics;
 };
 

diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index fc748173998fc345337d4fb837860a9c9b3dc353..54f762720b8ea2fd9dca4c0ef231e69ccacf2d4f 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -158,6 +158,8 @@ public:
   void check( std::vector< Node >& lems );
   //get solution
   Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed );
+  // is single invocation
+  bool isSingleInvocation() { return !d_single_inv.isNull(); }
 };
 
 }

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2177ebc32e091556d99c77e8354de20c2e323352..6a49980166cd43ee2288269b00dcc22d4c196c09 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -888,12 +888,14 @@ void QuantifiersEngine::flushLemmas(){
     //take default output channel if none is provided
     d_hasAddedLemma = true;
     for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){
+      Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
       getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
     }
     d_lemmas_waiting.clear();
   }
   if( !d_phase_req_waiting.empty() ){
     for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
+      Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl;
       getOutputChannel().requirePhase( it->first, it->second );
     }
     d_phase_req_waiting.clear();