Add option uf-ss-fair-monotone. Minor cleanup and improvement of sort inference.

7 files changed, 321 insertions, 187 deletions

diff --git a/src/options/uf_options b/src/options/uf_options
index baea1cb41..e7df9a2db 100644
--- a/src/options/uf_options
+++ b/src/options/uf_options
@@ -38,5 +38,7 @@ option ufssSymBreak --uf-ss-sym-break bool :default false
  finite model finding symmetry breaking techniques
 option ufssFairness --uf-ss-fair bool :default true
  use fair strategy for finite model finding multiple sorts
+option ufssFairnessMonotone --uf-ss-fair-monotone bool :read-write :default false
+ group monotone sorts when enforcing fairness for finite model finding
 
 endmodule
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 21d190d0e..f3724b432 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1337,9 +1337,13 @@ void SmtEngine::setDefaults() {
     options::decisionMode.set(decMode);
     options::decisionStopOnly.set(stoponly);
   }
+  if( options::incrementalSolving() ){
+    //disable modes not supported by incremental
+    options::sortInference.set( false );
+    options::ufssFairnessMonotone.set( false );
+  }
   //local theory extensions
   if( options::localTheoryExt() ){
-    //no E-matching?
     if( !options::instMaxLevel.wasSetByUser() ){
       options::instMaxLevel.set( 0 );
     }
@@ -3392,10 +3396,10 @@ void SmtEnginePrivate::processAssertions() {
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl;
   }
 
-  if( options::sortInference() ){
+  if( options::sortInference() || options::ufssFairnessMonotone() ){
     //sort inference technique
     SortInference * si = d_smt.d_theoryEngine->getSortInference();
-    si->simplify( d_assertions.ref() );
+    si->simplify( d_assertions.ref(), options::sortInference(), options::ufssFairnessMonotone() );
     for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){
       d_smt.setPrintFuncInModel( it->first.toExpr(), false );
       d_smt.setPrintFuncInModel( it->second.toExpr(), true );
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index a26c0e9d7..c4c24612d 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -26,7 +26,9 @@
 #include "options/uf_options.h"
 #include "proof/proof_manager.h"
 #include "theory/rewriter.h"
+#include "theory/quantifiers/quant_util.h"
 
+using namespace CVC4;
 using namespace std;
 
 namespace CVC4 {
@@ -40,7 +42,6 @@ void SortInference::UnionFind::print(const char * c){
   }
   Trace(c) << std::endl;
 }
-
 void SortInference::UnionFind::set( UnionFind& c ) {
   clear();
   for( std::map< int, int >::iterator it = c.d_eqc.begin(); it != c.d_eqc.end(); ++it ){
@@ -48,7 +49,6 @@ void SortInference::UnionFind::set( UnionFind& c ) {
   }
   d_deq.insert( d_deq.end(), c.d_deq.begin(), c.d_deq.end() );
 }
-
 int SortInference::UnionFind::getRepresentative( int t ){
   std::map< int, int >::iterator it = d_eqc.find( t );
   if( it==d_eqc.end() || it->second==t ){
@@ -59,7 +59,6 @@ int SortInference::UnionFind::getRepresentative( int t ){
     return rt;
   }
 }
-
 void SortInference::UnionFind::setEqual( int t1, int t2 ){
   if( t1!=t2 ){
     int rt1 = getRepresentative( t1 );
@@ -71,7 +70,6 @@ void SortInference::UnionFind::setEqual( int t1, int t2 ){
     }
   }
 }
-
 bool SortInference::UnionFind::isValid() {
   for( unsigned i=0; i<d_deq.size(); i++ ){
     if( areEqual( d_deq[i].first, d_deq[i].second ) ){
@@ -116,157 +114,166 @@ void SortInference::reset() {
   d_const_map.clear();
 }
 
-bool SortInference::simplify( std::vector< Node >& assertions ){
-  Trace("sort-inference") << "Calculating sort inference..." << std::endl;
-  //process all assertions
-  for( unsigned i=0; i<assertions.size(); i++ ){
-    Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;
-    std::map< Node, Node > var_bound;
-    process( assertions[i], var_bound );
-  }
-  for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
-    Trace("sort-inference") << it->first << " : ";
-    TypeNode retTn = it->first.getType();
-    if( !d_op_arg_types[ it->first ].empty() ){
-      Trace("sort-inference") << "( ";
-      for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){
-        recordSubsort( retTn[i], d_op_arg_types[ it->first ][i] );
-        printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
-        Trace("sort-inference") << " ";
-      }
-      Trace("sort-inference") << ") -> ";
-      retTn = retTn[(int)retTn.getNumChildren()-1];
-    }
-    recordSubsort( retTn, it->second );
-    printSort( "sort-inference", it->second );
-    Trace("sort-inference") << std::endl;
-  }
-  for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
-    Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl;
-    for( unsigned i=0; i<it->first[0].getNumChildren(); i++ ){
-      recordSubsort( it->first[0][i].getType(), it->second[it->first[0][i]] );
-      printSort( "sort-inference", it->second[it->first[0][i]] );
-      Trace("sort-inference") << std::endl;
-    }
-    Trace("sort-inference") << std::endl;
-  }
-
-  if( !options::ufssSymBreak() ){
-    bool rewritten = false;
-    //determine monotonicity of sorts
+void SortInference::simplify( std::vector< Node >& assertions, bool doSortInference, bool doMonotonicyInference ){
+  if( doSortInference ){
+    Trace("sort-inference") << "Calculating sort inference..." << std::endl;
+    //process all assertions
     for( unsigned i=0; i<assertions.size(); i++ ){
-      Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
+      Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;
       std::map< Node, Node > var_bound;
-      processMonotonic( assertions[i], true, true, var_bound );
+      process( assertions[i], var_bound );
     }
-
-    Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl;
-    for( unsigned i=0; i<d_sub_sorts.size(); i++ ){
-      printSort( "sort-inference", d_sub_sorts[i] );
-      if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
-        Trace("sort-inference") << " is interpreted." << std::endl;
-      }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
-        Trace("sort-inference") << " is monotonic." << std::endl;
-      }else{
-        Trace("sort-inference") << " is not monotonic." << std::endl;
+    for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
+      Trace("sort-inference") << it->first << " : ";
+      TypeNode retTn = it->first.getType();
+      if( !d_op_arg_types[ it->first ].empty() ){
+        Trace("sort-inference") << "( ";
+        for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){
+          recordSubsort( retTn[i], d_op_arg_types[ it->first ][i] );
+          printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
+          Trace("sort-inference") << " ";
+        }
+        Trace("sort-inference") << ") -> ";
+        retTn = retTn[(int)retTn.getNumChildren()-1];
       }
+      recordSubsort( retTn, it->second );
+      printSort( "sort-inference", it->second );
+      Trace("sort-inference") << std::endl;
     }
-
-    //simplify all assertions by introducing new symbols wherever necessary
-    for( unsigned i=0; i<assertions.size(); i++ ){
-      Node prev = assertions[i];
-      std::map< Node, Node > var_bound;
-      Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl;
-      Node curr = simplify( assertions[i], var_bound );
-      Trace("sort-inference-debug") << "Done." << std::endl;
-      if( curr!=assertions[i] ){
-        curr = theory::Rewriter::rewrite( curr );
-        rewritten = true;
-        Trace("sort-inference-rewrite") << assertions << std::endl;
-        Trace("sort-inference-rewrite") << " --> " << curr << std::endl;
-        PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
-        assertions[i] = curr;
+    for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
+      Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl;
+      for( unsigned i=0; i<it->first[0].getNumChildren(); i++ ){
+        recordSubsort( it->first[0][i].getType(), it->second[it->first[0][i]] );
+        printSort( "sort-inference", it->second[it->first[0][i]] );
+        Trace("sort-inference") << std::endl;
       }
+      Trace("sort-inference") << std::endl;
     }
-    //now, ensure constants are distinct
-    for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){
-      std::vector< Node > consts;
-      for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-        consts.push_back( it2->second );
+
+    if( !options::ufssSymBreak() ){
+      bool rewritten = false;
+      //determine monotonicity of sorts
+      for( unsigned i=0; i<assertions.size(); i++ ){
+        Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
+        std::map< Node, Node > var_bound;
+        processMonotonic( assertions[i], true, true, var_bound );
+      }
+      //doMonotonicyInference = false;
+
+      Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl;
+      for( unsigned i=0; i<d_sub_sorts.size(); i++ ){
+        printSort( "sort-inference", d_sub_sorts[i] );
+        if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
+          Trace("sort-inference") << " is interpreted." << std::endl;
+        }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
+          Trace("sort-inference") << " is monotonic." << std::endl;
+        }else{
+          Trace("sort-inference") << " is not monotonic." << std::endl;
+        }
       }
-      //TODO: add lemma enforcing introduced constants to be distinct
-    }
 
-    //enforce constraints based on monotonicity
-    for( std::map< TypeNode, std::vector< int > >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){
-      int nmonSort = -1;
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
-          nmonSort = it->second[i];
-          break;
+      //simplify all assertions by introducing new symbols wherever necessary
+      for( unsigned i=0; i<assertions.size(); i++ ){
+        Node prev = assertions[i];
+        std::map< Node, Node > var_bound;
+        Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl;
+        Node curr = simplify( assertions[i], var_bound );
+        Trace("sort-inference-debug") << "Done." << std::endl;
+        if( curr!=assertions[i] ){
+          curr = theory::Rewriter::rewrite( curr );
+          rewritten = true;
+          Trace("sort-inference-rewrite") << assertions << std::endl;
+          Trace("sort-inference-rewrite") << " --> " << curr << std::endl;
+          PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
+          assertions[i] = curr;
         }
       }
-      if( nmonSort!=-1 ){
-        std::vector< Node > injections;
-        TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first );
+      //now, ensure constants are distinct
+      for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){
+        std::vector< Node > consts;
+        for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+          consts.push_back( it2->second );
+        }
+        //TODO: add lemma enforcing introduced constants to be distinct
+      }
+
+      //enforce constraints based on monotonicity
+      for( std::map< TypeNode, std::vector< int > >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){
+        int nmonSort = -1;
         for( unsigned i=0; i<it->second.size(); i++ ){
-          if( it->second[i]!=nmonSort ){
-            TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first );
-            //make injection to nmonSort
-            Node a1 = mkInjection( new_tn, base_tn );
-            injections.push_back( a1 );
-            if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
-              //also must make injection from nmonSort to this
-              Node a2 = mkInjection( base_tn, new_tn );
-              injections.push_back( a2 );
-            }
+          if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
+            nmonSort = it->second[i];
+            break;
           }
         }
-        Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl;
-        for( unsigned j=0; j<injections.size(); j++ ){
-          Trace("sort-inference-rewrite") << "   " << injections[j] << std::endl;
-        }
-        assertions.insert( assertions.end(), injections.begin(), injections.end() );
-        if( !injections.empty() ){
-          rewritten = true;
+        if( nmonSort!=-1 ){
+          std::vector< Node > injections;
+          TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first );
+          for( unsigned i=0; i<it->second.size(); i++ ){
+            if( it->second[i]!=nmonSort ){
+              TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first );
+              //make injection to nmonSort
+              Node a1 = mkInjection( new_tn, base_tn );
+              injections.push_back( a1 );
+              if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
+                //also must make injection from nmonSort to this
+                Node a2 = mkInjection( base_tn, new_tn );
+                injections.push_back( a2 );
+              }
+            }
+          }
+          Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl;
+          for( unsigned j=0; j<injections.size(); j++ ){
+            Trace("sort-inference-rewrite") << "   " << injections[j] << std::endl;
+          }
+          assertions.insert( assertions.end(), injections.begin(), injections.end() );
+          if( !injections.empty() ){
+            rewritten = true;
+          }
         }
       }
-    }
-    //no sub-sort information is stored
-    reset();
-    return rewritten;
-  }
-  /*
-  else if( !options::ufssSymBreak() ){
-    //just add the unit lemmas between constants
-    std::map< TypeNode, std::map< int, Node > > constants;
-    for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
-      int rt = d_type_union_find.getRepresentative( it->second );
-      if( d_op_arg_types[ it->first ].empty() ){
-        TypeNode tn = it->first.getType();
-        if( constants[ tn ].find( rt )==constants[ tn ].end() ){
-          constants[ tn ][ rt ] = it->first;
+      //no sub-sort information is stored
+      reset();
+      Trace("sort-inference-debug") << "Finished sort inference, rewritten = " << rewritten << std::endl;
+    }
+    /*
+    else if( !options::ufssSymBreak() ){
+      //just add the unit lemmas between constants
+      std::map< TypeNode, std::map< int, Node > > constants;
+      for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
+        int rt = d_type_union_find.getRepresentative( it->second );
+        if( d_op_arg_types[ it->first ].empty() ){
+          TypeNode tn = it->first.getType();
+          if( constants[ tn ].find( rt )==constants[ tn ].end() ){
+            constants[ tn ][ rt ] = it->first;
+          }
         }
       }
-    }
-    //add unit lemmas for each constant
-    for( std::map< TypeNode, std::map< int, Node > >::iterator it = constants.begin(); it != constants.end(); ++it ){
-      Node first_const;
-      for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-        if( first_const.isNull() ){
-          first_const = it2->second;
-        }else{
-          Node eq = first_const.eqNode( it2->second );
-          //eq = Rewriter::rewrite( eq );
-          Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl;
-          assertions.push_back( eq );
+      //add unit lemmas for each constant
+      for( std::map< TypeNode, std::map< int, Node > >::iterator it = constants.begin(); it != constants.end(); ++it ){
+        Node first_const;
+        for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+          if( first_const.isNull() ){
+            first_const = it2->second;
+          }else{
+            Node eq = first_const.eqNode( it2->second );
+            //eq = Rewriter::rewrite( eq );
+            Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl;
+            assertions.push_back( eq );
+          }
         }
       }
     }
+    */
+    initialSortCount = sortCount;
+  }
+  if( doMonotonicyInference ){
+    for( unsigned i=0; i<assertions.size(); i++ ){
+      Trace("sort-inference-debug") << "Process type monotonicity for " << assertions[i] << std::endl;
+      std::map< Node, Node > var_bound;
+      processMonotonic( assertions[i], true, true, var_bound, true );
+    }
   }
-  */
-  initialSortCount = sortCount;
-  return false;
 }
 
 void SortInference::setEqual( int t1, int t2 ){
@@ -455,37 +462,42 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
   return retType;
 }
 
-void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ) {
+void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound, bool typeMode ) {
   Trace("sort-inference-debug") << "...Process monotonic " << pol << " " << hasPol << " " << n << std::endl;
   if( n.getKind()==kind::FORALL ){
-    for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
-      var_bound[n[0][i]] = n;
+    //only consider variables universally if it is possible this quantified formula is asserted positively
+    if( !hasPol || pol ){
+      for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+        var_bound[n[0][i]] = n;
+      }
     }
-    processMonotonic( n[1], pol, hasPol, var_bound );
-    for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
-      var_bound.erase( n[0][i] );
+    processMonotonic( n[1], pol, hasPol, var_bound, typeMode );
+    if( !hasPol || pol ){
+      for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+        var_bound.erase( n[0][i] );
+      }
     }
+    return;
   }else if( n.getKind()==kind::EQUAL ){
     if( !hasPol || pol ){
       for( unsigned i=0; i<2; i++ ){
         if( var_bound.find( n[i] )!=var_bound.end() ){
-          int sid = getSortId( var_bound[n[i]], n[i] );
-          d_non_monotonic_sorts[sid] = true;
+          if( !typeMode ){
+            int sid = getSortId( var_bound[n[i]], n[i] );
+            d_non_monotonic_sorts[sid] = true;
+          }else{
+            d_non_monotonic_sorts_orig[n[i].getType()] = true;
+          }
           break;
         }
       }
     }
   }
   for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    bool npol = pol;
-    bool nhasPol = hasPol;
-    if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){
-      npol = !npol;
-    }
-    if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){
-      nhasPol = false;
-    }
-    processMonotonic( n[i], npol, nhasPol, var_bound );
+    bool npol;
+    bool nhasPol;
+    theory::QuantPhaseReq::getPolarity( n, i, hasPol, pol, nhasPol, npol );
+    processMonotonic( n[i], npol, nhasPol, var_bound, typeMode );
   }
 }
 
@@ -756,4 +768,9 @@ void SortInference::getSortConstraints( Node n, UnionFind& uf ) {
   }
 }
 
+bool SortInference::isMonotonic( TypeNode tn ) {
+  Assert( tn.isSort() );
+  return d_non_monotonic_sorts_orig.find( tn )==d_non_monotonic_sorts_orig.end();
+}
+
 }/* CVC4 namespace */
diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h
index 4bb1a072e..f926776de 100644
--- a/src/theory/sort_inference.h
+++ b/src/theory/sort_inference.h
@@ -71,7 +71,7 @@ private:
   int process( Node n, std::map< Node, Node >& var_bound );
 //for monotonicity inference
 private:
-  void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound );
+  void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound, bool typeMode = false );
 
 //for rewriting
 private:
@@ -93,7 +93,7 @@ public:
   SortInference() : sortCount( 1 ){}
   ~SortInference(){}
 
-  bool simplify( std::vector< Node >& assertions );
+  void simplify( std::vector< Node >& assertions, bool doSortInference, bool doMonotonicyInference );
   //get sort id for term n
   int getSortId( Node n );
   //get sort id for variable of quantified formula f
@@ -109,6 +109,13 @@ public:
 public:
   //list of all functions and the uninterpreted symbols they were replaced with
   std::map< Node, Node > d_model_replace_f;
+
+private:
+  // store monotonicity for original sorts as well
+  std::map< TypeNode, bool > d_non_monotonic_sorts_orig;  
+public:
+  //is monotonic
+  bool isMonotonic( TypeNode tn );  
 };
 
 }
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index d617207cf..d261d0007 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1501,8 +1501,8 @@ Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) {
 }
 
 StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
-d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c ),
-d_card_assertions_eqv_lemma( u ), d_rel_eqc( c )
+d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c ), d_min_pos_com_card( c, -1 ), 
+d_card_assertions_eqv_lemma( u ), d_min_pos_tn_master_card( c, -1 ), d_rel_eqc( c )
 {
   if( options::ufssDiseqPropagation() ){
     d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this );
@@ -1618,9 +1618,45 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
     TypeNode tn = lit[0].getType();
     Assert( tn.isSort() );
     Assert( d_rep_model[tn] );
-    long nCard = lit[1].getConst<Rational>().getNumerator().getLong();
+    int nCard = lit[1].getConst<Rational>().getNumerator().getSignedInt();
     Node ct = d_rep_model[tn]->getCardinalityTerm();
+    Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
     if( lit[0]==ct ){
+      if( options::ufssFairnessMonotone() ){
+        Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
+        if( tn!=d_tn_mono_master ){
+          std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn );
+          if( it==d_tn_mono_slave.end() ){
+            bool isMonotonic;
+            if( d_th->getQuantifiersEngine() ){
+              isMonotonic = getSortInference()->isMonotonic( tn );
+            }else{
+              //if ground, everything is monotonic
+              isMonotonic = true;
+            }
+            if( isMonotonic ){
+              if( d_tn_mono_master.isNull() ){
+                Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set master : " << tn << std::endl;
+                d_tn_mono_master = tn;
+              }else{
+                Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn << std::endl;
+                d_tn_mono_slave[tn] = true;
+              }
+            }else{
+              Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn << std::endl;
+              d_tn_mono_slave[tn] = false;
+            }
+          }
+        }
+        //set the minimum positive cardinality for master if necessary
+        if( polarity && tn==d_tn_mono_master ){
+          Trace("uf-ss-com-card-debug") << "...set min positive cardinality" << std::endl;
+          if( d_min_pos_tn_master_card.get()==-1 || nCard<d_min_pos_tn_master_card.get() ){
+            d_min_pos_tn_master_card.set( nCard );
+          }
+        }
+      }
+      Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
       d_rep_model[tn]->assertCardinality( d_out, nCard, polarity );
       //check if combined cardinality is violated
       checkCombinedCardinality();
@@ -1636,14 +1672,28 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
   }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
     d_com_card_assertions[lit] = polarity;
     if( polarity ){
-      checkCombinedCardinality();
+      //safe to assume int here 
+      int nCard = lit[0].getConst<Rational>().getNumerator().getSignedInt();
+      if( d_min_pos_com_card.get()==-1 || nCard<d_min_pos_com_card.get() ){
+        d_min_pos_com_card.set( nCard );
+        checkCombinedCardinality();
+      }
     }else{
       bool needsCard = true;
-      for( std::map< int, Node >::iterator it = d_com_card_literal.begin(); it != d_com_card_literal.end(); ++it ){
-        if( d_com_card_assertions.find( it->second )==d_com_card_assertions.end() || d_com_card_assertions[it->second] ){
-          needsCard = false;
-          break;
+      if( d_min_pos_com_card.get()==-1 ){
+        //check if all current combined cardinality constraints are asserted negatively
+        for( std::map< int, Node >::iterator it = d_com_card_literal.begin(); it != d_com_card_literal.end(); ++it ){
+          if( d_com_card_assertions.find( it->second )==d_com_card_assertions.end() ){
+            Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : non-assertion : " << it->first << std::endl;
+            needsCard = false;
+            break;
+          }else{
+            Assert( !d_com_card_assertions[it->second] );
+          }
         }
+      }else{
+        Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : positive assertion : " << d_min_pos_com_card.get() << std::endl;
+        needsCard = false;
       }
       if( needsCard ){
         allocateCombinedCardinality();
@@ -1892,8 +1942,8 @@ bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){
 /** initialize */
 void StrongSolverTheoryUF::initializeCombinedCardinality() {
   if( options::ufssFairness() ){
-    Trace("uf-ss-com-card-debug") << "Initialize combined cardinality" << std::endl;
     if( d_aloc_com_card.get()==0 ){
+      Trace("uf-ss-com-card-debug") << "Initialize combined cardinality" << std::endl;
       allocateCombinedCardinality();
     }
   }
@@ -1902,36 +1952,76 @@ void StrongSolverTheoryUF::initializeCombinedCardinality() {
 /** check */
 void StrongSolverTheoryUF::checkCombinedCardinality() {
   if( options::ufssFairness() ){
+    Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
     int totalCombinedCard = 0;
+    int maxMonoSlave = 0;
+    TypeNode maxSlaveType;
     for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-      totalCombinedCard += it->second->getMaximumNegativeCardinality();
+      int max_neg = it->second->getMaximumNegativeCardinality();
+      if( !options::ufssFairnessMonotone() ){
+        totalCombinedCard += max_neg;
+      }else{
+        std::map< TypeNode, bool >::iterator its = d_tn_mono_slave.find( it->first );
+        if( its==d_tn_mono_slave.end() || !its->second ){
+          totalCombinedCard += max_neg;
+        }else{
+          if( max_neg>maxMonoSlave ){
+            maxMonoSlave = max_neg;
+            maxSlaveType = it->first;
+          }
+        }
+      }
     }
     Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard << std::endl;
-    for( int i=0; i<totalCombinedCard; i++ ){
-      if( d_com_card_literal.find( i )!=d_com_card_literal.end() ){
-        Node com_lit = d_com_card_literal[i];
-        if( d_com_card_assertions.find( com_lit )!=d_com_card_assertions.end() && d_com_card_assertions[com_lit] ){
-          //conflict
-          std::vector< Node > conf;
-          conf.push_back( com_lit );
-          int totalAdded = 0;
-          for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-            int c = it->second->getMaximumNegativeCardinality();
-            if( c>0 ){
-              conf.push_back( it->second->getCardinalityLiteral( c ).negate() );
-              totalAdded += c;
-            }
-            if( totalAdded>i ){
-              break;
-            }
+    if( options::ufssFairnessMonotone() ){
+      Trace("uf-ss-com-card-debug") << "Max slave monotonic negated cardinality : " << maxMonoSlave << std::endl;
+      if( d_min_pos_tn_master_card.get()!=-1 && maxMonoSlave>d_min_pos_tn_master_card.get() ){
+        int mc = d_min_pos_tn_master_card.get();
+        std::vector< Node > conf;
+        conf.push_back( d_rep_model[d_tn_mono_master]->getCardinalityLiteral( mc ) );
+        conf.push_back( d_rep_model[maxSlaveType]->getCardinalityLiteral( maxMonoSlave ).negate() );
+        Node cf = NodeManager::currentNM()->mkNode( AND, conf );
+        Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict : " << cf << std::endl;
+        Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict : " << cf << std::endl;
+        getOutputChannel().conflict( cf );
+        d_conflict.set( true );
+        return;
+      }
+    }
+    if( d_min_pos_com_card.get()!=-1 && totalCombinedCard>d_min_pos_com_card.get() ){
+      //conflict
+      int cc = d_min_pos_com_card.get();
+      Assert( d_com_card_literal.find( cc )!=d_com_card_literal.end() );
+      Node com_lit = d_com_card_literal[cc];
+      Assert( d_com_card_assertions.find( com_lit )!=d_com_card_assertions.end() );
+      Assert( d_com_card_assertions[com_lit] );
+      std::vector< Node > conf;
+      conf.push_back( com_lit );
+      int totalAdded = 0;
+      for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+        bool doAdd = true;
+        if( options::ufssFairnessMonotone() ){
+          std::map< TypeNode, bool >::iterator its = d_tn_mono_slave.find( it->first );
+          if( its!=d_tn_mono_slave.end() && its->second ){
+            doAdd = false;
+          }
+        }
+        if( doAdd ){
+          int c = it->second->getMaximumNegativeCardinality();
+          if( c>0 ){
+            conf.push_back( it->second->getCardinalityLiteral( c ).negate() );
+            totalAdded += c;
+          }
+          if( totalAdded>cc ){
+            break;
           }
-          Node cc = NodeManager::currentNM()->mkNode( AND, conf );
-          Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cc << std::endl;
-          Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cc << std::endl;
-          getOutputChannel().conflict( cc );
-          d_conflict.set( true );
         }
       }
+      Node cf = NodeManager::currentNM()->mkNode( AND, conf );
+      Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf << std::endl;
+      Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf << std::endl;
+      getOutputChannel().conflict( cf );
+      d_conflict.set( true );
     }
   }
 }
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index dd32154d9..45d7fc3cc 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -314,8 +314,14 @@ private:
   std::map< int, Node > d_com_card_literal;
   /** combined cardinality assertions (indexed by cardinality literals ) */
   NodeBoolMap d_com_card_assertions;
+  /** minimum positive combined cardinality */
+  context::CDO< int > d_min_pos_com_card;
   /** cardinality literals for which we have added */
   NodeBoolMap d_card_assertions_eqv_lemma;
+  /** the master monotone type (if ufssFairnessMonotone enabled) */
+  TypeNode d_tn_mono_master;
+  std::map< TypeNode, bool > d_tn_mono_slave;
+  context::CDO< int > d_min_pos_tn_master_card;  
   /** initialize */
   void initializeCombinedCardinality();
   /** allocateCombinedCardinality */
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 0040a38c3..6faab8517 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -71,6 +71,10 @@ public:
       if( n[1].getKind()!=kind::CONST_RATIONAL ){
         throw TypeCheckingExceptionPrivate(n, "cardinality constraint must be a constant");
       }
+      CVC4::Rational r(INT_MAX);
+      if( n[1].getConst<Rational>()>r ){
+        throw TypeCheckingExceptionPrivate(n, "Exceeded INT_MAX in cardinality constraint");
+      }
       if( n[1].getConst<Rational>().getNumerator().sgn()!=1 ){
         throw TypeCheckingExceptionPrivate(n, "cardinality constraint must be positive");
       }
@@ -91,6 +95,10 @@ public:
       if( n[0].getKind()!=kind::CONST_RATIONAL ){
         throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be a constant");
       }
+      CVC4::Rational r(INT_MAX);
+      if( n[0].getConst<Rational>()>r ){
+        throw TypeCheckingExceptionPrivate(n, "Exceeded INT_MAX in combined cardinality constraint");
+      }
       if( n[0].getConst<Rational>().getNumerator().sgn()==-1 ){
         throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be non-negative");
       }