Lemmas instead of conflicts in sygus sym break (do not expand explanations). Minor improvements to sygus splitting.

4 files changed, 171 insertions, 61 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 3063e85bb..353bd1392 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -56,11 +56,13 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
       //register the constructors that are redundant children of argument sIndex of constructor index csIndex of dt
       registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, sIndex );
 
-      if( options::sygusNormalFormArg() && sIndex==1 && pdt[csIndex].getNumArgs()==2 ){
-        arg1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] );
-        tn1 = arg1.getType();
-        if( !DatatypesRewriter::isTypeDatatype( tn1 ) ){
-          arg1 = Node::null();
+      if( options::sygusNormalFormArg() ){
+        if( sIndex==1 && pdt[csIndex].getNumArgs()==2 ){
+          arg1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] );
+          tn1 = arg1.getType();
+          if( !DatatypesRewriter::isTypeDatatype( tn1 ) ){
+            arg1 = Node::null();
+          }
         }
       }
       // we are splitting on a term that may later have no semantics : guard this case
@@ -99,6 +101,21 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
               narrow = true;
             }
           }
+          //other constraints on arguments
+          Kind curr = d_util->getArgKind( tnn, i );
+          if( curr!=UNDEFINED_KIND ){
+            //ITE children must be distinct when properly typed
+            if( curr==ITE ){
+              if( getArgType( dt[i], 1 )==tnn && getArgType( dt[i], 2 )==tnn ){
+                Node arg_ite1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[i][1].getSelector() ), n );
+                Node arg_ite2 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[i][2].getSelector() ), n );
+                Node deq = arg_ite1.eqNode( arg_ite2 ).negate();
+                Trace("sygus-str") << "...ite strengthen " << deq << std::endl;
+                test_c.push_back( deq );
+                narrow = true;
+              }
+            }
+          }
           //add fairness constraint
           if( options::ceGuidedInstFair()==quantifiers::CEGQI_FAIR_DT_SIZE ){
             Node szl = NodeManager::currentNM()->mkNode( DT_SIZE, n );
@@ -218,16 +235,11 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
     }else{
       // calculate which constructors we should consider based on normal form for terms
       //get parent kind
-      bool hasParentKind = false;
-      Kind parentKind;
-      if( d_util->isKindArg( tnnp, csIndex ) ){
-        hasParentKind = true;
-        parentKind = d_util->d_arg_kind[tnnp][csIndex];
-      }
+      Kind parentKind = d_util->getArgKind( tnnp, csIndex );
       for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
         Assert( d_sygus_nred.find( tnn )!=d_sygus_nred.end() );
         bool addSplit = d_sygus_nred[tnn][i];
-        if( addSplit && hasParentKind ){
+        if( addSplit && parentKind!=UNDEFINED_KIND ){
           if( d_util->d_arg_kind.find( tnn )!=d_util->d_arg_kind.end() && d_util->d_arg_kind[tnn].find( i )!=d_util->d_arg_kind[tnn].end() ){
             addSplit = considerSygusSplitKind( dt, pdt, tnn, tnnp, d_util->d_arg_kind[tnn][i], parentKind, sIndex );
             if( !addSplit ){
@@ -257,7 +269,7 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
         d_sygus_pc_nred[tnn][csIndex][sIndex].push_back( addSplit );
       }
       //compute argument relationships for 2-arg constructors
-      if( d_util->isKindArg( tnnp, csIndex ) && pdt[csIndex].getNumArgs()==2 ){
+      if( parentKind!=UNDEFINED_KIND && pdt[csIndex].getNumArgs()==2 ){
         int osIndex = sIndex==0 ? 1 : 0;
         TypeNode tnno = getArgType( pdt[csIndex], osIndex );
         if( DatatypesRewriter::isTypeDatatype( tnno ) ){
@@ -268,7 +280,6 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
             Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() );
             Assert( d_sygus_pc_nred[tnno][csIndex].find( osIndex )!=d_sygus_pc_nred[tnno][csIndex].end() );
 
-            Kind parentKind = d_util->d_arg_kind[tnnp][csIndex];
             bool isPComm = d_util->isComm( parentKind );
             std::map< int, bool > larg_consider;
             for( unsigned i=0; i<dto.getNumConstructors(); i++ ){
@@ -479,6 +490,32 @@ bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pd
       return false;
     }
   }
+  if( pdt[pc].getNumArgs()==2 ){
+    Kind ok;
+    int offset;
+    if( d_util->hasOffsetArg( parent, arg, offset, ok ) ){
+      Trace("sygus-split-debug") << parent << " has offset arg " << ok << " " << offset << std::endl;
+      int ok_arg = d_util->getKindArg( tnp, ok );
+      if( ok_arg!=-1 ){
+        Trace("sygus-split-debug") << "...at argument " << ok_arg << std::endl;
+        //other operator be the same type
+        if( isTypeMatch( pdt[ok_arg], pdt[arg] ) ){
+          Node co = d_util->getTypeValueOffset( c.getType(), c, offset );
+          Trace("sygus-split-debug") << c << " with offset " << offset << " is " << co << std::endl;
+          if( !co.isNull() ){
+            if( d_util->hasConst( tn, co ) ){
+              Trace("sygus-split-debug") << "arg " << arg << " " << c << " in " << parent << " can be treated as " << co << " in " << ok << "..." << std::endl;
+              return false;
+            }else{
+              Trace("sygus-split-debug") << "Type does not have constant." << std::endl;
+            }
+          }
+        }else{
+          Trace("sygus-split-debug") << "Type mismatch." << std::endl;
+        }
+      }
+    }
+  }
   return true;
 }
 
@@ -507,6 +544,19 @@ TypeNode SygusSplit::getArgType( const DatatypeConstructor& c, int i ) {
   return TypeNode::fromType( ((SelectorType)c[i].getType()).getRangeType() );
 }
 
+bool SygusSplit::isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ){
+  if( c1.getNumArgs()!=c2.getNumArgs() ){
+    return false;
+  }else{
+    for( unsigned i=0; i<c1.getNumArgs(); i++ ){
+      if( getArgType( c1, i )!=getArgType( c2, i ) ){
+        return false;
+      }
+    }
+    return true;
+  }
+}
+
 bool SygusSplit::isGenericRedundant( TypeNode tn, Node g ) {
   //everything added to this cache should be mutually exclusive cases
   std::map< Node, bool >::iterator it = d_gen_redundant[tn].find( g );
@@ -707,6 +757,7 @@ Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog
 bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node prog,
                                            std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) {
   Assert( a.getType()==at );
+  //Assert( !d_util->d_conflict );
   std::map< Node, bool >::iterator it = d_redundant[at].find( prog );
   bool red;
   if( it==d_redundant[at].end() ){
@@ -799,14 +850,14 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node
             for( unsigned i=0; i<testers.size(); i++ ){
               bool rl = std::find( rlv_testers.begin(), rlv_testers.end(), testers[i] )!=rlv_testers.end();
               Trace("sygus-nf-gen-debug") << "* " << testers[i] << " -> " << rl << std::endl;
-              d_conflict_gen[at][prog].push_back( rl );
+              d_lemma_gen[at][prog].push_back( rl );
             }
           }
         }
       }
       if( !conflict_gen_set ){
         for( unsigned i=0; i<testers.size(); i++ ){
-          d_conflict_gen[at][prog].push_back( true );
+          d_lemma_gen[at][prog].push_back( true );
         }
       }
     }
@@ -814,16 +865,21 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node
     red = it->second;
   }
   if( red ){
-    Assert( d_conflict_gen[at][prog].size()==testers.size() );
-    std::vector< Node > gtesters;
-    for( unsigned i=0; i<testers.size(); i++ ){
-      if( d_conflict_gen[at][prog][i] ){
-        gtesters.push_back( testers[i] );
+    if( std::find( d_lemmas_reported[at][prog].begin(), d_lemmas_reported[at][prog].end(), a )==d_lemmas_reported[at][prog].end() ){
+      d_lemmas_reported[at][prog].push_back( a );
+      Assert( d_lemma_gen[at][prog].size()==testers.size() );
+      std::vector< Node > gtesters;
+      for( unsigned i=0; i<testers.size(); i++ ){
+        if( d_lemma_gen[at][prog][i] ){
+          gtesters.push_back( testers[i].negate() );
+        }
       }
+      Node lem = gtesters.size()==1 ? gtesters[0] : NodeManager::currentNM()->mkNode( OR, gtesters );
+      d_util->d_lemmas.push_back( lem );
+      Trace("sygus-sym-break2") << "Sym break lemma : " << lem << std::endl;
+    }else{
+      Trace("sygus-sym-break2") << "repeated lemma for " << prog << " from " << a << std::endl;
     }
-    d_util->d_conflictNode = gtesters.size()==1 ? gtesters[0] : NodeManager::currentNM()->mkNode( AND, gtesters );
-    Trace("sygus-sym-break2") << "Conflict : " << d_util->d_conflictNode << std::endl;
-    d_util->d_conflict = true;
     return false;
   }else{
     return true;
@@ -862,7 +918,7 @@ void SygusSymBreak::collectTesters( Node tst, std::map< Node, std::vector< Node
   }
 }
 
-SygusUtil::SygusUtil( Context* c ) : d_conflict( c, false ) {
+SygusUtil::SygusUtil( Context* c ) {
   d_split = new SygusSplit( this );
   d_sym_break = new SygusSymBreak( this, c );
 }
@@ -1075,6 +1131,26 @@ bool SygusUtil::isSingularArg( Node n, Kind ik, int arg ) {
   return false;
 }
 
+bool SygusUtil::hasOffsetArg( Kind ik, int arg, int& offset, Kind& ok ) {
+  if( ik==LT ){
+    Assert( arg==0 || arg==1 );
+    offset = arg==0 ? 1 : -1;
+    ok = LEQ;
+    return true;
+  }else if( ik==BITVECTOR_ULT ){
+    Assert( arg==0 || arg==1 );
+    offset = arg==0 ? 1 : -1;
+    ok = BITVECTOR_ULE;
+    return true;
+  }else if( ik==BITVECTOR_SLT ){
+    Assert( arg==0 || arg==1 );
+    offset = arg==0 ? 1 : -1;
+    ok = BITVECTOR_SLE;
+    return true;
+  }
+  return false;
+}
+
 
 Node SygusUtil::getTypeValue( TypeNode tn, int val ) {
   std::map< int, Node >::iterator it = d_type_value[tn].find( val );
@@ -1115,6 +1191,25 @@ Node SygusUtil::getTypeMaxValue( TypeNode tn ) {
   }
 }
 
+Node SygusUtil::getTypeValueOffset( TypeNode tn, Node val, int offset ) {
+  std::map< int, Node >::iterator it = d_type_value_offset[tn][val].find( offset );
+  if( it==d_type_value_offset[tn][val].end() ){
+    Node val_o;
+    Node offset_val = getTypeValue( tn, offset );
+    if( !offset_val.isNull() ){
+      if( tn.isInteger() || tn.isReal() ){
+        val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, val, offset_val ) );
+      }else if( tn.isBitVector() ){
+        val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode( BITVECTOR_PLUS, val, offset_val ) );
+      }
+    }
+    d_type_value_offset[tn][val][offset] = val_o;
+    return val_o;
+  }else{
+    return it->second;
+  }
+}
+
 void SygusUtil::registerSygusType( TypeNode tn ){
   if( d_register.find( tn )==d_register.end() ){
     if( !DatatypesRewriter::isTypeDatatype( tn ) ){
@@ -1196,14 +1291,20 @@ bool SygusUtil::hasOp( TypeNode tn, Node n ) {
   return getOpArg( tn, n )!=-1;
 }
 
-bool SygusUtil::isKindArg( TypeNode tn, int i ) {
+Kind SygusUtil::getArgKind( TypeNode tn, int i ) {
   Assert( isRegistered( tn ) );
   std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn );
   if( itt!=d_arg_kind.end() ){
-    return itt->second.find( i )!=itt->second.end();
-  }else{
-    return false;
+    std::map< int, Kind >::iterator itk = itt->second.find( i );
+    if( itk!=itt->second.end() ){
+      return itk->second;
+    }
   }
+  return UNDEFINED_KIND;
+}
+
+bool SygusUtil::isKindArg( TypeNode tn, int i ) {
+  return getArgKind( tn, i )!=UNDEFINED_KIND;
 }
 
 bool SygusUtil::isConstArg( TypeNode tn, int i ) {
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index f30a0fd0a..33e9fc54a 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -47,19 +47,6 @@ private:
   std::map< TypeNode, std::map< Node, Node > > d_gen_terms;
   std::map< TypeNode, std::map< Node, bool > > d_gen_redundant;
 private:
-  bool isRegistered( TypeNode tn );
-  int getKindArg( TypeNode tn, Kind k );
-  int getConstArg( TypeNode tn, Node n );
-  int getOpArg( TypeNode tn, Node n );
-  bool hasKind( TypeNode tn, Kind k );
-  bool hasConst( TypeNode tn, Node n );
-  bool hasOp( TypeNode tn, Node n );
-  bool isKindArg( TypeNode tn, int i );
-  bool isConstArg( TypeNode tn, int i );
-private:
-  Node getVar( TypeNode tn, int i );
-  Node getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count );
-private:
   /** register sygus type */
   void registerSygusType( TypeNode tn );
   /** register sygus operator */
@@ -73,6 +60,8 @@ private:
   bool isArgDatatype( const DatatypeConstructor& c, int i, const Datatype& dt );
   /** get arg type */
   TypeNode getArgType( const DatatypeConstructor& c, int i );
+  /** is type match */
+  bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
 private:
   // generic cache
   bool isGenericRedundant( TypeNode tn, Node g );
@@ -117,7 +106,8 @@ private:
   std::map< Node, ProgSearch * > d_prog_search;
   std::map< TypeNode, std::map< Node, Node > > d_normalized_to_orig;
   std::map< TypeNode, std::map< Node, bool > > d_redundant;
-  std::map< TypeNode, std::map< Node, std::vector< bool > > > d_conflict_gen;
+  std::map< TypeNode, std::map< Node, std::vector< Node > > > d_lemmas_reported;
+  std::map< TypeNode, std::map< Node, std::vector< bool > > > d_lemma_gen;
   Node getAnchor( Node n );
   bool processCurrentProgram( Node a, TypeNode at, int depth, Node prog,
                               std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u );
@@ -155,6 +145,7 @@ private:
   bool hasKind( TypeNode tn, Kind k );
   bool hasConst( TypeNode tn, Node n );
   bool hasOp( TypeNode tn, Node n );
+  Kind getArgKind( TypeNode tn, int i );
   bool isKindArg( TypeNode tn, int i );
   bool isConstArg( TypeNode tn, int i );
   void registerSygusType( TypeNode tn );
@@ -162,6 +153,7 @@ private:
   //information for builtin types
   std::map< TypeNode, std::map< int, Node > > d_type_value;
   std::map< TypeNode, Node > d_type_max_value;
+  std::map< TypeNode, std::map< Node, std::map< int, Node > > > d_type_value_offset;
   /** is assoc */
   bool isAssoc( Kind k );
   /** is comm */
@@ -172,9 +164,13 @@ private:
   bool isIdempotentArg( Node n, Kind ik, int arg );
   /** is singular arg */
   bool isSingularArg( Node n, Kind ik, int arg );
+  /** get offset arg */
+  bool hasOffsetArg( Kind ik, int arg, int& offset, Kind& ok );
   /** get value */
   Node getTypeValue( TypeNode tn, int val );
   /** get value */
+  Node getTypeValueOffset( TypeNode tn, Node val, int offset );
+  /** get value */
   Node getTypeMaxValue( TypeNode tn );
 private:
   Node getVar( TypeNode tn, int i );
@@ -187,8 +183,9 @@ public:
   SygusUtil( context::Context* c );
   SygusSplit * getSplit() { return d_split; }
   SygusSymBreak * getSymBreak() { return d_sym_break; }
-  context::CDO<bool> d_conflict;
-  Node d_conflictNode;
+  //context::CDO<bool> d_conflict;
+  //Node d_conflictNode;
+  std::vector< Node > d_lemmas;
 };
 
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 42d06cdb5..063b76102 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -368,17 +368,26 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
     if( !d_conflict && polarity ){
       Trace("dt-tester") << "Assert tester : " << atom << std::endl;
       if( d_sygus_util ){
-        Assert( !d_sygus_util->d_conflict );
+        //Assert( !d_sygus_util->d_conflict );
         d_sygus_util->getSymBreak()->addTester( atom );
+        for( unsigned i=0; i<d_sygus_util->d_lemmas.size(); i++ ){
+          Trace("dt-lemma-sygus") << "Sygus symmetry breaking lemma : " << d_sygus_util->d_lemmas[i] << std::endl;
+          d_out->lemma( d_sygus_util->d_lemmas[i] );
+        }
+        d_sygus_util->d_lemmas.clear();
+        /*
         if( d_sygus_util->d_conflict ){
-          d_conflict = true;
-          std::vector< TNode > assumptions;
-          explain( d_sygus_util->d_conflictNode, assumptions );
-          d_conflictNode = mkAnd( assumptions );
-          Trace("dt-conflict") << "CONFLICT: sygus symmetry breaking conflict : " << d_conflictNode << std::endl;
-          d_out->conflict( d_conflictNode );
+          //d_conflict = true;
+          if( !d_sygus_util->d_conflictNode.isNull() ){
+            std::vector< TNode > assumptions;
+            explain( d_sygus_util->d_conflictNode, assumptions );
+            d_conflictNode = mkAnd( assumptions );
+            Trace("dt-conflict") << "CONFLICT: sygus symmetry breaking conflict : " << d_conflictNode << std::endl;
+            d_out->conflict( d_conflictNode );
+          }
           return;
         }
+        */
       }
     }
   }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index f9b7c4fdc..6d604a345 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -191,7 +191,7 @@ void CegInstantiation::CegConjecture::analyzeSygusConjecture() {
           std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( c );
           if( itp!=prog_invoke.end() ){
             std::vector< Node > terms;
-            std::vector< Node > subs;        
+            std::vector< Node > subs;
             for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
               if( !it2->second.empty() ){
                 Node prog = it2->first;
@@ -235,7 +235,7 @@ void CegInstantiation::CegConjecture::analyzeSygusConjecture() {
             d_single_inv_arg_sk.push_back( v );
           }
           bd = bd.substitute( vars.begin(), vars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() );
-          
+
           Trace("cegqi-analyze-debug") << "    -> " << bd << std::endl;
         }
         d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
@@ -263,18 +263,21 @@ void CegInstantiation::CegConjecture::analyzeSygusConjecture() {
 }
 
 bool CegInstantiation::CegConjecture::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) {
+  Trace("ajr-temp") << "Process single inv lit " << lit << " " << pol << std::endl;
   if( lit.getKind()==NOT ){
     return processSingleInvLiteral( lit[0], !pol, case_vals );
   }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){
     bool exh = true;
     for( unsigned k=0; k<lit.getNumChildren(); k++ ){
-      exh = exh && processSingleInvLiteral( lit[k], pol, case_vals );
+      bool curr = processSingleInvLiteral( lit[k], pol, case_vals );
+      exh = exh && curr;
     }
     return exh;
   }else if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
     if( pol ){
       for( unsigned r=0; r<2; r++ ){
-        std::map< Node, Node >::iterator it = d_single_inv_map_to_prog.find( lit[0] );
+        Trace("ajr-temp") << "Check literal " << lit[r] << " at " << r << std::endl;
+        std::map< Node, Node >::iterator it = d_single_inv_map_to_prog.find( lit[r] );
         if( it!=d_single_inv_map_to_prog.end() ){
           if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){
             case_vals[it->second].push_back( lit[ r==0 ? 1 : 0 ] );
@@ -286,9 +289,9 @@ bool CegInstantiation::CegConjecture::processSingleInvLiteral( Node lit, bool po
   }
   return false;
 }
-  
+
 bool CegInstantiation::CegConjecture::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
-                                                            std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, 
+                                                            std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
                                                             std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
   if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
@@ -345,7 +348,7 @@ bool CegInstantiation::CegConjecture::analyzeSygusTerm( Node n, std::map< Node,
     }
   }else{
     //record this conjunct contains n
-    contains[n] = true;    
+    contains[n] = true;
   }
   return true;
 }
@@ -403,7 +406,7 @@ 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;
@@ -470,7 +473,7 @@ void CegInstantiation::registerQuantifier( Node q ) {
               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 
+            //measure term is a fresh constant
             mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) );
           }
         }