CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly applied selectors.

9 files changed, 157 insertions, 42 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 90703774b..29a95b38f 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -169,22 +169,46 @@ public:
         }
       }
     }
-    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] ) );
+    if(in.getKind() == kind::DT_SIZE ){
+      if( 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 size " << in << " to " << res << std::endl;
+        return RewriteResponse(REWRITE_AGAIN_FULL, res );
       }
-      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) );
+    }else if(in.getKind() == kind::DT_HEIGHT_BOUND ){
+      if( in[0].getKind()==kind::APPLY_CONSTRUCTOR ){
+        std::vector< Node > children;
+        Node res;
+        Rational r = in[1].getConst<Rational>();
+        Rational rmo = Rational( r-Rational(1) );
+        for( unsigned i=0; i<in[0].getNumChildren(); i++ ){
+          if( in[0][i].getType().isDatatype() ){
+            if( r.isZero() ){
+              res = NodeManager::currentNM()->mkConst(false);
+              break;
+            }else{
+              children.push_back( NodeManager::currentNM()->mkNode( kind::DT_HEIGHT_BOUND, in[0][i], NodeManager::currentNM()->mkConst(rmo) ) );
+            }
+          }
+        }
+        if( res.isNull() ){
+          res = children.size()==0 ? NodeManager::currentNM()->mkConst(true) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) );
+        }
+        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite height " << in << " to " << res << std::endl;
+        return RewriteResponse(REWRITE_AGAIN_FULL, res );
       }
-      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) {
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 84bcb5814..b68206b48 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -136,7 +136,11 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
           }
         }
       }
-
+      
+      // we are splitting on a term that may later have no semantics : guard this case
+      Node ptest = DatatypesRewriter::mkTester( n[0], csIndex, pdt ).negate();
+      Trace("sygus-split-debug") << "Parent guard : " << ptest << std::endl;
+      d_splits[n].push_back( ptest );
     }
 
     for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
@@ -272,6 +276,7 @@ void SygusSplit::registerSygusType( TypeNode tn, const Datatype& dt ) {
             }
           }
         }
+        //NAND,NOR
       }
       d_sygus_nred[tn].push_back( nred );
     }
@@ -447,24 +452,28 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
     Kind nk = UNDEFINED_KIND;
     Kind reqk = UNDEFINED_KIND;
     std::map< int, Kind > reqk_arg; //TODO
-    if( k==AND ) { 
-      nk = OR;reqk = NOT;
-    }else if( k==OR ){ 
-      nk = AND;reqk = NOT;
-    }else if( k==IFF ) { 
-      nk = XOR;
-    }else if( k==XOR ) { 
-      nk = IFF;
-    }else if( k==BITVECTOR_AND ) { 
-      nk = BITVECTOR_OR;reqk = BITVECTOR_NOT;
-    }else if( k==BITVECTOR_OR ){ 
-      nk = BITVECTOR_AND;reqk = BITVECTOR_NOT;
-    }else if( k==BITVECTOR_XNOR ) { 
-      nk = BITVECTOR_XOR;
-    }else if( k==BITVECTOR_XOR ) { 
-      nk = BITVECTOR_XNOR;
+    if( parent==NOT ){
+      if( k==AND ) { 
+        nk = OR;reqk = NOT;
+      }else if( k==OR ){ 
+        nk = AND;reqk = NOT;
+      }else if( k==IFF ) { 
+        nk = XOR;
+      }else if( k==XOR ) { 
+        nk = IFF;
+      }
+    }
+    if( parent==BITVECTOR_NOT ){
+      if( k==BITVECTOR_AND ) { 
+        nk = BITVECTOR_OR;reqk = BITVECTOR_NOT;
+      }else if( k==BITVECTOR_OR ){ 
+        nk = BITVECTOR_AND;reqk = BITVECTOR_NOT;
+      }else if( k==BITVECTOR_XNOR ) { 
+        nk = BITVECTOR_XOR;
+      }else if( k==BITVECTOR_XOR ) { 
+        nk = BITVECTOR_XNOR;
+      }
     }
-    //NAND,NOR
     if( nk!=UNDEFINED_KIND ){
       Trace("sygus-split-debug") << "Push " << parent << " over " << k << " to " << nk;
       if( reqk!=UNDEFINED_KIND ){
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 8c25e2a86..55db44c29 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -167,4 +167,7 @@ typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule
 operator DT_SIZE 1 "datatypes size"
 typerule DT_SIZE ::CVC4::theory::datatypes::DtSizeTypeRule
 
+operator DT_HEIGHT_BOUND 1 "datatypes height bound"
+typerule DT_HEIGHT_BOUND ::CVC4::theory::datatypes::DtHeightBoundTypeRule
+
 endtheory
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 82804e565..501b3d86e 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -60,6 +60,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
   d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine.addFunctionKind(kind::DT_SIZE);
+  d_equalityEngine.addFunctionKind(kind::DT_HEIGHT_BOUND);
   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
   //d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 
@@ -134,7 +135,7 @@ void TheoryDatatypes::check(Effort e) {
 
   TimerStat::CodeTimer checkTimer(d_checkTime);
 
-  Trace("datatypes-debug") << "Check effort " << e << std::endl;
+  Trace("datatypes-check") << "Check effort " << e << std::endl;
   while(!done() && !d_conflict) {
     // Get all the assertions
     Assertion assertion = get();
@@ -994,7 +995,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
 }
 
 void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) {
-  Debug("datatypes-debug") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl;
+  Trace("dt-collapse-sel") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl;
   //check to see if it is redundant
   NodeListMap::iterator sel_i = d_selector_apps.find( n );
   Assert( sel_i != d_selector_apps.end() );
@@ -1002,7 +1003,8 @@ void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFact
     NodeList* sel = (*sel_i).second;
     for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
       Node ss = *j;
-      if( s.getOperator()==ss.getOperator() ){
+      if( s.getOperator()==ss.getOperator() && ( s.getKind()!=DT_HEIGHT_BOUND || s[1]==ss[1] ) ){
+        Trace("dt-collapse-sel") << "...redundant." << std::endl;
         return;
       }
     }
@@ -1056,21 +1058,33 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
   Assert( c.getKind()==APPLY_CONSTRUCTOR );
   Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl;
   Node r;
+  bool wrong = false;
   if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
     //Trace("dt-collapse-sel") << "Indices : " << Datatype::indexOf(c.getOperator().toExpr()) << " " << Datatype::cindexOf(s.getOperator().toExpr()) << std::endl;
+    wrong = Datatype::indexOf(c.getOperator().toExpr())!=Datatype::cindexOf(s.getOperator().toExpr());
+    //if( wrong ){
+    //  return;
+    //}
     //if( Datatype::indexOf(c.getOperator().toExpr())!=Datatype::cindexOf(s.getOperator().toExpr()) ){
     //  mkExpDefSkolem( s.getOperator(), s[0].getType(), s.getType() );
     //  r = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[s.getOperator().toExpr()], s[0] );
     //}else{
     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 );
+  }else if( s.getKind()==DT_SIZE ){
+    r = NodeManager::currentNM()->mkNode( DT_SIZE, c );
+  }else if( s.getKind()==DT_HEIGHT_BOUND ){
+    r = NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, c, s[1] );
+    if( r==d_true ){
+      return;
+    }
   }
   Node rr = Rewriter::rewrite( r );
   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;
+    Trace("datatypes-infer") << "DtInfer : collapse sel";
+    Trace("datatypes-infer") << ( wrong ? " wrong" : "");
+    Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl;
 
     d_pending.push_back( eq );
     d_pending_exp[ eq ] = eq_exp;
@@ -1102,7 +1116,9 @@ void TheoryDatatypes::computeCareGraph(){
       for( unsigned j=i+1; j<functionTerms; j++ ){
         TNode f2 = r==0 ? d_consTerms[j] : d_selTerms[j];
         Trace("dt-cg-debug") << "dt-cg: " << f1 << " and " << f2 << " " << (f1.getOperator()==f2.getOperator()) << " " << areEqual( f1, f2 ) << std::endl;
-        if( f1.getOperator()==f2.getOperator() && ( f1.getKind()!=DT_SIZE || f1[0].getType()==f2[0].getType() ) && !areEqual( f1, f2 ) ){
+        if( f1.getOperator()==f2.getOperator() && 
+            ( ( f1.getKind()!=DT_SIZE && f1.getKind()!=DT_HEIGHT_BOUND ) || f1[0].getType()==f2[0].getType() ) && 
+            !areEqual( f1, f2 ) ){
           Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
           bool somePairIsDisequal = false;
           currentPairs.clear();
@@ -1357,10 +1373,10 @@ void TheoryDatatypes::collectTerms( Node n ) {
     if( n.getKind() == APPLY_CONSTRUCTOR ){
       Debug("datatypes") << "  Found constructor " << n << endl;
       d_consTerms.push_back( n );
-    }else if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE ){
+    }else if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){
       d_selTerms.push_back( n );
       //we must also record which selectors exist
-      Debug("datatypes") << "  Found selector " << n << endl;
+      Trace("dt-collapse-sel") << "  Found selector " << n << endl;
       //if (n.getType().isBoolean()) {
       //  d_equalityEngine.addTriggerPredicate( n );
       //}else{
@@ -1396,6 +1412,27 @@ void TheoryDatatypes::collectTerms( Node n ) {
         d_pending.push_back( conc );
         d_pending_exp[ conc ] = d_true;
         d_infer.push_back( conc );
+      }else if( n.getKind() == DT_HEIGHT_BOUND ){
+        if( n[1].getConst<Rational>().isZero() ){
+          std::vector< Node > children;
+          const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
+          for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+            if( DatatypesRewriter::isNullaryConstructor( dt[i] ) ){
+              Node test = DatatypesRewriter::mkTester( n[0], i, dt );
+              children.push_back( test );
+            }
+          }
+          Node lem;
+          if( children.empty() ){
+            lem = n.negate();
+          }else{
+            lem = NodeManager::currentNM()->mkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) );
+          }
+          Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl;
+          d_pending.push_back( lem );
+          d_pending_exp[ lem ] = d_true;
+          d_infer.push_back( lem );
+        }
       }
     }
   }
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 3044a2bf1..b97645ecb 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -567,6 +567,26 @@ public:
   }
 };/* class DtSizeTypeRule */
 
+class DtHeightBoundTypeRule {
+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 height bound term to have datatype argument.");
+      }
+      if( n[1].getKind()!=kind::CONST_RATIONAL ){
+        throw TypeCheckingExceptionPrivate(n, "datatype height bound must be a constant");
+      }
+      if( n[1].getConst<Rational>().getNumerator().sgn()==-1 ){
+        throw TypeCheckingExceptionPrivate(n, "datatype height bound must be non-negative");
+      }
+    }
+    return nodeManager->integerType();
+  }
+};/* class DtHeightBoundTypeRule */
+
 
 }/* CVC4::theory::datatypes namespace */
 }/* CVC4::theory namespace */
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") {