Add fair strategy for finite model finding multiple sorts --uf-ss-fair.

8 files changed, 155 insertions, 19 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index e0375e6e1..7667acdd0 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -270,6 +270,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       toStream(op, n.getOperator(), depth, types, false);
       break;
     case kind::CARDINALITY_CONSTRAINT:
+    case kind::COMBINED_CARDINALITY_CONSTRAINT:
       out << "CARDINALITY_CONSTRAINT";
       break;
 
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 393f3883c..b6ef924d7 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -162,6 +162,10 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
       if(val.getKind() == kind::CARDINALITY_CONSTRAINT) {
         val = NodeManager::currentNM()->mkConst(getCardinality(val[0].getType().toType()).getFiniteCardinality() <= val[1].getConst<Rational>().getNumerator());
       }
+      if(val.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){
+        //FIXME
+        val = NodeManager::currentNM()->mkConst(false);
+      }
       return val;
     }
 
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index fa24df717..e99c3366c 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -18,4 +18,7 @@ typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule
 operator CARDINALITY_CONSTRAINT 2 "cardinality constraint"
 typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule
 
+operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint"
+typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule
+
 endtheory
diff --git a/src/theory/uf/options b/src/theory/uf/options
index b9f60b83d..cfa6e6c04 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -42,5 +42,7 @@ option ufssCliqueSplits --uf-ss-clique-splits bool :default false
 
 option ufssSymBreak --uf-ss-sym-break bool :default false
  finite model finding symmetry breaking techniques
+option ufssFairness --uf-ss-fair bool :default false
+ use fair strategy for finite model finding multiple sorts
 
 endmodule
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 41935984f..0ee7a2bdd 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -72,7 +72,6 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) {
 }/* mkAnd() */
 
 void TheoryUF::check(Effort level) {
-
   while (!done() && !d_conflict)
   {
     // Get all the assertions
@@ -94,7 +93,7 @@ void TheoryUF::check(Effort level) {
     TNode atom = polarity ? fact : fact[0];
     if (atom.getKind() == kind::EQUAL) {
       d_equalityEngine.assertEquality(atom, polarity, fact);
-    } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT) {
+    } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) {
       // do nothing
     } else {
       d_equalityEngine.assertPredicate(atom, polarity, fact);
@@ -136,6 +135,7 @@ void TheoryUF::preRegisterTerm(TNode node) {
     d_functionsTerms.push_back(node);
     break;
   case kind::CARDINALITY_CONSTRAINT:
+  case kind::COMBINED_CARDINALITY_CONSTRAINT:
     //do nothing
     break;
   default:
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 4ef11c042..5f63fa8df 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -416,7 +416,7 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in
 StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
           d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ),
           d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ),
-          d_cardinality_assertions( c ), d_hasCard( c, false ){
+          d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ){
   d_cardinality_term = n;
 }
 
@@ -894,6 +894,10 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
           allocateCardinality( out );
         }
       }
+      if( c>d_maxNegCard.get() ){
+        Trace("uf-ss-com-card-debug") << "Maximum negative cardinality for " << d_type << " is now " << c << std::endl;
+        d_maxNegCard.set( c );
+      }
     }
   }
 }
@@ -1449,13 +1453,12 @@ void StrongSolverTheoryUF::SortModel::getRepresentatives( std::vector< Node >& r
   }
 }
 
+Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) {
+  return d_cardinality_literal.find( c )!=d_cardinality_literal.end() ? d_cardinality_literal[c] : Node::null();
+}
+
 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_conf_types(),
-d_rep_model_init( 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 )
 {
   if( options::ufssColoringSat() ){
     d_term_amb = new TermDisambiguator( th->getQuantifiersEngine(), c );
@@ -1539,6 +1542,25 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
     Assert( d_rep_model[tn] );
     long nCard = lit[1].getConst<Rational>().getNumerator().getLong();
     d_rep_model[tn]->assertCardinality( d_out, nCard, polarity );
+
+    //check if combined cardinality is violated
+    checkCombinedCardinality();
+  }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
+    d_com_card_assertions[lit] = polarity;
+    if( polarity ){
+      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( needsCard ){
+        allocateCombinedCardinality();
+      }
+    }
   }else{
     if( Trace.isOn("uf-ss-warn") ){
       ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but
@@ -1625,6 +1647,18 @@ void StrongSolverTheoryUF::propagate( Theory::Effort level ){
 
 /** get next decision request */
 Node StrongSolverTheoryUF::getNextDecisionRequest(){
+  //request the combined cardinality as a decision literal, if not already asserted
+  int comCard = 0;
+  Node com_lit;
+  do {
+    com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null();
+    if( d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){
+      Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl;
+      return com_lit;
+    }
+    comCard++;
+  }while( !com_lit.isNull() );
+  //otherwise, check each individual sort
   for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
     Node n = it->second->getNextDecisionRequest();
     if( !n.isNull() ){
@@ -1635,6 +1669,9 @@ Node StrongSolverTheoryUF::getNextDecisionRequest(){
 }
 
 void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
+  //initialize combined cardinality
+  initializeCombinedCardinality();
+
   Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
   //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
   TypeNode tn = n.getType();
@@ -1661,7 +1698,7 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
     if( rm ){
       rm->initialize( d_out );
       d_rep_model[tn] = rm;
-      d_rep_model_init[tn] = true;
+      //d_rep_model_init[tn] = true;
     }
   }else{
     Trace("uf-ss-register") << "Already preregistered sort " << tn << "." << std::endl;
@@ -1769,6 +1806,70 @@ void 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 ){
+      allocateCombinedCardinality();
+    }
+  }
+}
+
+/** check */
+void StrongSolverTheoryUF::checkCombinedCardinality() {
+  if( options::ufssFairness() ){
+    int totalCombinedCard = 0;
+    for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+      totalCombinedCard += it->second->getMaximumNegativeCardinality();
+    }
+    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;
+            }
+          }
+          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 );
+        }
+      }
+    }
+  }
+}
+
+void StrongSolverTheoryUF::allocateCombinedCardinality() {
+  Trace("uf-ss-com-card") << "Allocate combined cardinality (" << d_aloc_com_card.get() << ")" << std::endl;
+  //make node
+  Node lem = NodeManager::currentNM()->mkNode( COMBINED_CARDINALITY_CONSTRAINT,
+                                               NodeManager::currentNM()->mkConst( Rational( d_aloc_com_card.get() ) ) );
+  Trace("uf-ss-com-card") << "Split on " << lem << std::endl;
+  lem = Rewriter::rewrite(lem);
+  d_com_card_literal[ d_aloc_com_card.get() ] = lem;
+  lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
+  //add as lemma to output channel
+  getOutputChannel().lemma( lem );
+  //require phase
+  getOutputChannel().requirePhase( d_com_card_literal[ d_aloc_com_card.get() ], true );
+  //increment cardinality
+  d_aloc_com_card.set( d_aloc_com_card.get() + 1 );
+}
+
 StrongSolverTheoryUF::Statistics::Statistics():
   d_clique_conflicts("StrongSolverTheoryUF::Clique_Conflicts", 0),
   d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0),
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 079a03c36..4f41ebf2e 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -245,6 +245,8 @@ public:
     context::CDO< bool > d_hasCard;
     /** clique lemmas that have been asserted */
     std::map< int, std::vector< std::vector< Node > > > d_cliques;
+    /** maximum negatively asserted cardinality */
+    context::CDO< int > d_maxNegCard;
   private:
     /** apply totality */
     bool applyTotality( int cardinality );
@@ -281,6 +283,10 @@ public:
     void getRepresentatives( std::vector< Node >& reps );
     /** has cardinality */
     bool hasCardinalityAsserted() { return d_hasCard; }
+    /** get cardinality literal */
+    Node getCardinalityLiteral( int c );
+    /** get maximum negative cardinality */
+    int getMaximumNegativeCardinality() { return d_maxNegCard.get(); }
     //print debug
     void debugPrint( const char* c );
     /** debug a model */
@@ -298,13 +304,22 @@ private:
   context::CDO<bool> d_conflict;
   /** rep model structure, one for each type */
   std::map< TypeNode, SortModel* > d_rep_model;
-  /** all types */
-  std::vector< TypeNode > d_conf_types;
-  /** whether conflict find data structures have been initialized */
-  TypeNodeBoolMap d_rep_model_init;
-  /** get conflict find */
+  /** get sort model */
   SortModel* getSortModel( Node n );
 private:
+  /** allocated combined cardinality */
+  context::CDO< int > d_aloc_com_card;
+  /** combined cardinality constraints */
+  std::map< int, Node > d_com_card_literal;
+  /** combined cardinality assertions (indexed by cardinality literals ) */
+  NodeBoolMap d_com_card_assertions;
+  /** initialize */
+  void initializeCombinedCardinality();
+  /** allocateCombinedCardinality */
+  void allocateCombinedCardinality();
+  /** check */
+  void checkCombinedCardinality();
+private:
   /** term disambiguator */
   TermDisambiguator* d_term_amb;
   /** disequality propagator */
@@ -359,10 +374,6 @@ public:
   /** debug a model */
   void debugModel( TheoryModel* m );
 public:
-  /** get number of types */
-  int getNumCardinalityTypes() { return (int)d_conf_types.size(); }
-  /** get type */
-  TypeNode getCardinalityType( int i ) { return d_conf_types[i]; }
   /** get is in conflict */
   bool isConflict() { return d_conflict; }
   /** get cardinality for node */
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index b9a8ed12e..50a746205 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -70,6 +70,20 @@ public:
   }
 };/* class CardinalityConstraintTypeRule */
 
+class CombinedCardinalityConstraintTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw(TypeCheckingExceptionPrivate) {
+    if( check ) {
+      TypeNode valType = n[0].getType(check);
+      if( valType != nodeManager->integerType() ) {
+        throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be integer");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* class CardinalityConstraintTypeRule */
+
 }/* CVC4::theory::uf namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */