Do not enforce dt fairness when single invocation sygus.

3 files changed, 33 insertions, 18 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 5e6bcf0b4..aaab8f3f9 100644
--- 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 52e110720..09e449b35 100644
--- 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 fc7481739..54f762720 100644
--- 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(); }
 };
 
 }