4 files changed, 24 insertions, 2 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index b1850b373..bb53c9cfb 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -73,7 +73,8 @@ Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i
     std::map< int, Node >::iterator it = d_lits.find( i );
     if( it==d_lits.end() ){
       Trace("cegqi-engine") << "******* CEGQI : allocate size literal " << i << std::endl;
-      Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i ) ) );
+      Node c = NodeManager::currentNM()->mkConst( Rational( i ) );
+      Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, c );
       lit = Rewriter::rewrite( lit );
       d_lits[i] = lit;
 
@@ -81,6 +82,17 @@ Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i
       Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl;
       qe->getOutputChannel().lemma( lem );
       qe->getOutputChannel().requirePhase( lit, true );
+      
+      if( options::ceGuidedInstFair()==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++ ){
+          lem_c.push_back( NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) );
+        }
+        Node hlem = NodeManager::currentNM()->mkNode( OR, lit.negate(), lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ) );
+        Trace("cegqi-lemma") << "Fairness expansion (dt-height-pred) : " << hlem << std::endl;
+        qe->getOutputChannel().lemma( hlem );
+      }
       return lit;
     }else{
       return it->second;
@@ -158,6 +170,9 @@ void CegInstantiation::registerQuantifier( Node q ) {
             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 ){
+            //measure term is a fresh constant 
+            mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) );
           }
         }
         if( !mc.empty() ){
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 5e692ace1..a6c52274f 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -128,6 +128,8 @@ typedef enum {
   CEGQI_FAIR_UF_DT_SIZE,
   /** enforce fairness by datatypes size */
   CEGQI_FAIR_DT_SIZE,
+  /** enforce fairness by datatypes height bound */
+  CEGQI_FAIR_DT_HEIGHT_PRED,
   /** do not use fair strategy for CEGQI */
   CEGQI_FAIR_NONE,
 } CegqiFairMode;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 009a0ada6..560e29c3b 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -198,7 +198,7 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo
   if and how to apply fairness for cegqi
 option sygusDecompose --sygus-decompose bool :default false
   decompose single invocation synthesis conjectures
-option sygusNormalForm --sygus-normal-form bool :default true
+option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form
 option sygusNormalFormArg --sygus-nf-arg bool :default true
   account for relationship between arguments of operations in sygus normal form
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index e9f85d454..fdfad21b9 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -184,6 +184,9 @@ uf-dt-size \n\
 default | dt-size \n\
 + Default, enforce fairness using size theory operator.\n\
 \n\
+dt-height-bound \n\
++ Enforce fairness by height bound predicate.\n\
+\n\
 none \n\
 + Do not enforce fairness. \n\
 \n\
@@ -379,6 +382,8 @@ inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optar
     return CEGQI_FAIR_UF_DT_SIZE;
   } else if(optarg == "default" || optarg == "dt-size") {
     return CEGQI_FAIR_DT_SIZE;
+  } else if(optarg == "dt-height-bound" ){
+    return CEGQI_FAIR_DT_HEIGHT_PRED;
   } else if(optarg == "none") {
     return CEGQI_FAIR_NONE;
   } else if(optarg ==  "help") {