Add dt.size to datatypes theory. Add option for fairness strategy used by CEGQI. Improve care graph/equality status for datatypes. Only do FULL effort check in datatypes if no other theories used output channel.

13 files changed, 182 insertions, 74 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6fce26484..3d57eebff 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1459,6 +1459,8 @@ builtinOp[CVC4::Kind& kind]
   | RERANGE_TOK    { $kind = CVC4::kind::REGEXP_RANGE; }
   | RELOOP_TOK    { $kind = CVC4::kind::REGEXP_LOOP; }
   
+  | DTSIZE_TOK     { $kind = CVC4::kind::DT_SIZE; }
+  
   | FMFCARD_TOK    { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
 
   // NOTE: Theory operators go here
@@ -1858,6 +1860,8 @@ RELOOP_TOK : 're.loop';
 RENOSTR_TOK : 're.nostr';
 REALLCHAR_TOK : 're.allchar';
 
+DTSIZE_TOK : 'dt.size';
+
 FMFCARD_TOK : 'fmf.card';
 
 EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 37e64ca88..3a41510dd 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -159,6 +159,23 @@ public:
         return RewriteResponse(REWRITE_DONE,gt );
       }
     }
+    if(in.getKind() == kind::DT_SIZE && in[0].getKind()==kind::APPLY_CONSTRUCTOR ){
+      std::vector< Node > children;
+      for( unsigned i=0; i<in[0].getNumChildren(); i++ ){
+        if( in[0][i].getType().isDatatype() ){
+          children.push_back( NodeManager::currentNM()->mkNode( kind::DT_SIZE, in[0][i] ) );
+        }
+      }
+      Node res;
+      if( !children.empty() ){
+        children.push_back( NodeManager::currentNM()->mkConst( Rational(1) ) );
+        res = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::PLUS, children );
+      }else{
+        res = NodeManager::currentNM()->mkConst( Rational(0) );
+      }
+      Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite " << in << " to " << res << std::endl;
+      return RewriteResponse(REWRITE_AGAIN_FULL, res );
+    }
     if(in.getKind() == kind::TUPLE_SELECT &&
        in[0].getKind() == kind::TUPLE) {
       return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]);
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index faaf78fe4..8c25e2a86 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -163,4 +163,8 @@ constant RECORD_UPDATE_OP \
 parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field"
 typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule
 
+
+operator DT_SIZE 1 "datatypes size"
+typerule DT_SIZE ::CVC4::theory::datatypes::DtSizeTypeRule
+
 endtheory
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 145cd32dd..4c37e8889 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -58,6 +58,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
   d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
+  d_equalityEngine.addFunctionKind(kind::DT_SIZE);
   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 
@@ -147,7 +148,7 @@ void TheoryDatatypes::check(Effort e) {
     flushPendingFacts();
   }
 
-  if( e == EFFORT_FULL && !d_conflict ) {
+  if( e == EFFORT_FULL && !d_conflict && !d_valuation.needCheck() ) {
     //check for cycles
     bool addedFact;
     do {
@@ -286,7 +287,7 @@ void TheoryDatatypes::flushPendingFacts(){
           Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
           Node ee_exp = explain( exp );
           Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl;
-          lem = NodeManager::currentNM()->mkNode( IMPLIES, ee_exp, fact );
+          lem = NodeManager::currentNM()->mkNode( OR, ee_exp.negate(), fact );
           lem = Rewriter::rewrite( lem );
         }
         Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
@@ -1027,19 +1028,20 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
 }
 
 void TheoryDatatypes::collapseSelector( Node s, Node c ) {
-  Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
+  Node r;
+  if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
+    r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
+  }else if( s.getKind()==kind::DT_SIZE ){
+    r = NodeManager::currentNM()->mkNode( kind::DT_SIZE, c );
+  }
   Node rr = Rewriter::rewrite( r );
-  //if( r!=rr ){
-    //Node eq_exp = NodeManager::currentNM()->mkConst(true);
-    //Node eq = r.getType().isBoolean() ? r.iffNode( rr ) : r.eqNode( rr );
-  if( s!=rr ){::
+  if( s!=rr ){
     Node eq_exp = c.eqNode( s[0] );
     Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr );
-
-
+    Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq << " by " << eq_exp << std::endl;
+    
     d_pending.push_back( eq );
     d_pending_exp[ eq ] = eq_exp;
-    Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq << " by " << eq_exp << std::endl;
     d_infer.push_back( eq );
     d_infer_exp.push_back( eq_exp );
   }
@@ -1056,7 +1058,7 @@ EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){
       return EQUALITY_FALSE;
     }
   }
-  return EQUALITY_UNKNOWN;
+  return EQUALITY_FALSE_IN_MODEL;
 }
 
 void TheoryDatatypes::computeCareGraph(){
@@ -1386,7 +1388,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
         //eqc->d_selectors = true;
       }
       */
-    }else if( n.getKind() == APPLY_SELECTOR_TOTAL ){
+    }else if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE ){
       d_selTerms.push_back( n );
       //we must also record which selectors exist
       Debug("datatypes") << "  Found selector " << n << endl;
@@ -1400,6 +1402,15 @@ void TheoryDatatypes::collectTerms( Node n ) {
       EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
       //add it to the eqc info
       addSelector( n, eqc, rep );
+      
+      if( n.getKind() == DT_SIZE ){
+        Node conc = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), n );
+        //must be non-negative
+        Trace("datatypes-infer") << "DtInfer : non-negative size : " << conc << std::endl;
+        d_pending.push_back( conc );
+        d_pending_exp[ conc ] = d_true;
+        d_infer.push_back( conc );
+      }
     }
   }
 }
@@ -1731,35 +1742,39 @@ bool TheoryDatatypes::mustSpecifyAssignment(){
 }
 
 bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
-  //the datatypes decision procedure makes 3 "internal" inferences apart from the equality engine :
+  //the datatypes decision procedure makes 5 "internal" inferences apart from the equality engine :
   //  (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
   //  (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t )
   //  (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
-  //We may need to communicate (3) outwards if the conclusions involve other theories
+  //  (4) collapse selector : S( C( t1...tn ) ) = t'
+  //  (5) collapse term size : size( C( t1...tn ) ) = 1 + size( t1 ) + ... + size( tn )
+  //  (6) non-negative size : 0 <= size( t )
+  //We may need to communicate (3) outwards if the conclusions involve other theories.  Also communicate (5) and (6).
   Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
   bool addLemma = false;
   if( ( n.getKind()==EQUAL || n.getKind()==IFF) && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL  ){
-#if 1
     const Datatype& dt = ((DatatypeType)(n[1].getType()).toType()).getDatatype();
     addLemma = dt.involvesExternalType();
-#else
-    for( int j=0; j<(int)n[1].getNumChildren(); j++ ){
-      if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){
-        addLemma = true;
-        break;
-      }
-    }
-#endif
-    if( addLemma ){
-      //check if we have already added this lemma
-      if( std::find( d_inst_lemmas[ n[0] ].begin(), d_inst_lemmas[ n[0] ].end(), n[1] )==d_inst_lemmas[ n[0] ].end() ){
-        d_inst_lemmas[ n[0] ].push_back( n[1] );
-        Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
-        return true;
-      }else{
-        Trace("dt-lemma-debug") << "Already communicated " << n << std::endl;
-        return false;
-      }
+    //for( int j=0; j<(int)n[1].getNumChildren(); j++ ){
+    //  if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){
+    //    addLemma = true;
+    //    break;
+    //  }
+    //}
+  }else if( n.getKind()==EQUAL && ( n[0].getKind()==DT_SIZE || n[1].getKind()==DT_SIZE ) ){
+    addLemma = true;
+  }else if( n.getKind()==LEQ ){
+    addLemma = true;
+  }
+  if( addLemma ){
+    //check if we have already added this lemma
+    if( std::find( d_inst_lemmas[ n[0] ].begin(), d_inst_lemmas[ n[0] ].end(), n[1] )==d_inst_lemmas[ n[0] ].end() ){
+      d_inst_lemmas[ n[0] ].push_back( n[1] );
+      Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
+      return true;
+    }else{
+      Trace("dt-lemma-debug") << "Already communicated " << n << std::endl;
+      return false;
     }
   }
   //else if( exp.getKind()==APPLY_TESTER ){
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 74d10e754..d698e80c9 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -138,8 +138,6 @@ private:
   eq::EqualityEngine d_equalityEngine;
   /** information necessary for equivalence classes */
   std::map< Node, EqcInfo* > d_eqc_info;
-  /** selector applications */
-  //BoolMap d_selector_apps;
   /** map from nodes to their instantiated equivalent for each constructor type */
   std::map< Node, std::map< int, Node > > d_inst_map;
   /** which instantiation lemmas we have sent */
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 8ce8ee7df..84be5238d 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -551,6 +551,21 @@ struct RecordProperties {
   }
 };/* struct RecordProperties */
 
+class DtSizeTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ) {
+      TypeNode t = n[0].getType(check);
+      if (!t.isDatatype()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting datatype size term to have datatype argument.");
+      }
+    }
+    return nodeManager->integerType();
+  }
+};/* class DtSizeTypeRule */
+
+
 }/* CVC4::theory::datatypes namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 90e7a274a..dddbee73b 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -50,19 +50,23 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
 }
 
 Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
-  std::map< int, Node >::iterator it = d_lits.find( i );
-  if( it==d_lits.end() ){
-    Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i ) ) );
-    lit = Rewriter::rewrite( lit );
-    d_lits[i] = lit;
-
-    Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
-    Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl;
-    qe->getOutputChannel().lemma( lem );
-    qe->getOutputChannel().requirePhase( lit, true );
-    return lit;
+  if( d_measure_term.isNull() ){
+    return Node::null();
   }else{
-    return it->second;
+    std::map< int, Node >::iterator it = d_lits.find( i );
+    if( it==d_lits.end() ){
+      Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i ) ) );
+      lit = Rewriter::rewrite( lit );
+      d_lits[i] = lit;
+
+      Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
+      Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl;
+      qe->getOutputChannel().lemma( lem );
+      qe->getOutputChannel().requirePhase( lit, true );
+      return lit;
+    }else{
+      return it->second;
+    }
   }
 }
 
@@ -110,18 +114,26 @@ void CegInstantiation::registerQuantifier( Node q ) {
         d_quantEngine->getOutputChannel().lemma( lem );
       }
       //fairness
-      std::vector< Node > mc;
-      for( unsigned j=0; j<d_conj->d_candidates.size(); j++ ){
-        TypeNode tn = d_conj->d_candidates[j].getType();
-        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] ) );
+      if( options::ceGuidedInstFair()!=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( tn.isDatatype() ){
+              mc.push_back( NodeManager::currentNM()->mkNode( DT_SIZE, d_conj->d_candidates[j] ) );
+            }
+          }else if( options::ceGuidedInstFair()==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] ) );
+            }
+          }
+        }
+        if( !mc.empty() ){
+          d_conj->d_measure_term = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc );
+          Trace("cegqi") << "Measure term is : " << d_conj->d_measure_term << std::endl;
         }
-      }
-      if( !mc.empty() ){
-        d_conj->d_measure_term = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc );
-        Trace("cegqi") << "Measure term is : " << d_conj->d_measure_term << std::endl;
       }
     }else{
       Assert( d_conj->d_quant==q );
@@ -154,7 +166,7 @@ Node CegInstantiation::getNextDecisionRequest() {
     return d_conj->d_guard;
   }
   //enforce fairness
-  if( d_conj->isAssigned() ){
+  if( d_conj->isAssigned() && options::ceGuidedInstFair()!=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 ){
@@ -180,7 +192,9 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
     Trace("cegqi-engine") << conj->d_candidates[i] << " ";
   }
   Trace("cegqi-engine") << std::endl;
-  Trace("cegqi-engine") << "  * Current term size : " << conj->d_curr_lit.get() << std::endl;
+  if( options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){
+    Trace("cegqi-engine") << "  * Current term size : " << conj->d_curr_lit.get() << std::endl;
+  }
 
   if( conj->d_ce_sk.empty() ){
     Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
@@ -190,14 +204,17 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       if( getModelValues( conj->d_candidates, model_values ) ){
         //check if we must apply fairness lemmas
         std::vector< Node > lems;
-        for( unsigned j=0; j<conj->d_candidates.size(); j++ ){
-          getMeasureLemmas( conj->d_candidates[j], model_values[j], lems );
+        if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){
+          for( unsigned j=0; j<conj->d_candidates.size(); j++ ){
+            getMeasureLemmas( conj->d_candidates[j], model_values[j], lems );
+          }
         }
         if( !lems.empty() ){
           for( unsigned j=0; j<lems.size(); j++ ){
             Trace("cegqi-lemma") << "Measure lemma : " << lems[j] << std::endl;
             d_quantEngine->addLemma( lems[j] );
           }
+          Trace("cegqi-engine") << "  ...refine size." << std::endl;
         }else{
           //must get a counterexample to the value of the current candidate
           Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
@@ -210,6 +227,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
           d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk.negate() ) );
           conj->d_ce_sk.push_back( inst[0] );
+          Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
         }
       }
 
@@ -233,6 +251,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
                                                                   model_values.begin(), model_values.end() );
         Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine );
         Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
+        Trace("cegqi-engine") << "  ...refine candidate." << std::endl;
         d_quantEngine->addLemma( lem );
       }
     }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index cb1825377..2502416bd 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -68,18 +68,6 @@ private:
     /** allocate literal */
     Node getLiteral( QuantifiersEngine * qe, int i );
   };
-  class CegFairness {
-  public:
-    CegFairness( context::Context* c );
-    /** which conjecture we are looking at */
-    CegConjecture * d_conj;
-    /** the cardinality literals */
-    std::map< int, Node > d_lits;
-    /** current cardinality */
-    context::CDO< int > d_curr_lit;
-    /** allocate literal */
-    Node getLiteral( int i );
-  };
   /** the quantified formula stating the synthesis conjecture */
   CegConjecture * d_conj;
 private: //for enforcing fairness
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 993ac5536..53c04cfe8 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -125,6 +125,15 @@ typedef enum {
   PRENEX_NONE,
 } PrenexQuantMode;
 
+typedef enum {
+  /** enforce fairness by UF corresponding to datatypes size */
+  CEGQI_FAIR_UF_DT_SIZE,
+  /** enforce fairness by datatypes size */
+  CEGQI_FAIR_DT_SIZE,
+  /** do not use fair strategy for CEGQI */
+  CEGQI_FAIR_NONE,
+} CegqiFairMode;
+
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index d608f0820..1cab2f9d8 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -178,5 +178,7 @@ option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
  
 option ceGuidedInst --cegqi bool :default false
   counterexample guided quantifier instantiation
+option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_UF_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h"
+  if and how to apply fairness for cegqi
  
 endmodule
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 9558aa0e0..be74fffab 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -178,6 +178,20 @@ none \n\
 + Do no prenex nested quantifiers. \n\
 \n\
 ";
+static const std::string cegqiFairModeHelp = "\
+Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\
+\n\
+default \n\
++ Default, enforce fairness using an uninterpreted function for datatypes size.\n\
+\n\
+dt-size \n\
++ Enforce fairness using size theory operator.\n\
+\n\
+none \n\
++ Do not enforce fairness. \n\
+\n\
+";
+
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
     return INST_WHEN_PRE_FULL;
@@ -355,6 +369,22 @@ inline PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string o
   }
 }
 
+inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "default" || optarg == "uf-dt-size" ) {
+    return CEGQI_FAIR_UF_DT_SIZE;
+  } else if(optarg == "dt-size") {
+    return CEGQI_FAIR_DT_SIZE;
+  } else if(optarg == "none") {
+    return CEGQI_FAIR_NONE;
+  } else if(optarg ==  "help") {
+    puts(cegqiFairModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --cegqi-fair: `") +
+                          optarg + "'.  Try --cegqi-fair help.");
+  }
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index b2d7f4b21..7407086c2 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -103,5 +103,9 @@ std::pair<bool, Node> Valuation::entailmentCheck(theory::TheoryOfMode mode, TNod
   return d_engine->entailmentCheck(mode, lit, params, out);
 }
 
+bool Valuation::needCheck() const{
+  return d_engine->needCheck();
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 448d055d4..540ebd8fc 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -135,6 +135,9 @@ public:
    */
   std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL);
 
+  /** need check ? */
+  bool needCheck() const;
+  
 };/* class Valuation */
 
 }/* CVC4::theory namespace */