From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 9 Apr 2014 20:43:37 +0000 (-0500)
Subject: Handle fmf.card as input from user, add support in SMT2 parser, as requested by Marti... 
X-Git-Tag: cvc5-1.0.0~6980
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=40fbc4aa1961cbeea2451251e54909285d2f4292;p=cvc5.git

Handle fmf.card as input from user, add support in SMT2 parser, as requested by Martin Brain.  Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f030d6de0..659fc97d9 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1351,6 +1351,8 @@ builtinOp[CVC4::Kind& kind]
   | REOPT_TOK      { $kind = CVC4::kind::REGEXP_OPT; }
   | RERANGE_TOK    { $kind = CVC4::kind::REGEXP_RANGE; }
   | RELOOP_TOK    { $kind = CVC4::kind::REGEXP_LOOP; }
+  
+  | FMFCARD_TOK    { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
 
   // NOTE: Theory operators go here
   ;
@@ -1734,6 +1736,8 @@ RELOOP_TOK : 're.loop';
 RENOSTR_TOK : 're.nostr';
 REALLCHAR_TOK : 're.allchar';
 
+FMFCARD_TOK : 'fmf.card';
+
 EMPTYSET_TOK: 'emptyset'; // Other set theory operators are not
                           // tokenized and handled directly when
                           // processing a term
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 4a23f1c97..a74c51a9a 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -210,7 +210,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
     }
   }
   if( index==(int)f[0].getNumChildren() ){
-    return false;
+    return reset;
   }else{
     Node n = m[ index ];
     std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 738cfed60..8b62fc39b 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -83,14 +83,17 @@ void ModelEngine::check( Theory::Effort e ){
           Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
           //let the strong solver verify that the model is minimal
           //for debugging, this will if there are terms in the model that the strong solver was not notified of
-          ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm );
-          Trace("model-engine-debug") << "Check model..." << std::endl;
-          d_incomplete_check = false;
-          //print debug
-          Debug("fmf-model-complete") << std::endl;
-          debugPrint("fmf-model-complete");
-          //successfully built an acceptable model, now check it
-          addedLemmas += checkModel();
+          if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){
+            Trace("model-engine-debug") << "Check model..." << std::endl;
+            d_incomplete_check = false;
+            //print debug
+            Debug("fmf-model-complete") << std::endl;
+            debugPrint("fmf-model-complete");
+            //successfully built an acceptable model, now check it
+            addedLemmas += checkModel();
+          }else{
+            addedLemmas++;
+          }
         }
       }
       if( addedLemmas==0 ){
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index ea1231e7a..c1b3b307d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -81,7 +81,7 @@ Node TermDb::getOperator( Node n ) {
     }
     d_par_op_map[op][tn1][tn2] = n;
     return n;
-  }else if( n.getKind()==APPLY_UF ){
+  }else if( n.hasOperator() ){
     return n.getOperator();
   }else{
     return Node::null();
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 7fa61477f..eaf5e8228 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -508,7 +508,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
   ///*
   bool alreadyExists = false;
   if( options::incrementalSolving() ){
-    Trace("inst-add-debug") << "Adding into context-dependent inst trie" << std::endl;
+    Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
     inst::CDInstMatchTrie* imt;
     std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( f );
     if( it!=d_c_inst_match_trie.end() ){
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 54a3075a1..6ea3bbd21 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -417,6 +417,12 @@ StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context
           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_maxNegCard( c, 0 ){
   d_cardinality_term = n;
+  //if( d_type.isSort() ){
+  //  TypeEnumerator te(tn);
+  //  d_cardinality_term = *te;
+  //}else{
+  //  d_cardinality_term = tn.mkGroundTerm();
+  //}
 }
 
 /** initialize */
@@ -829,14 +835,19 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
   if( !d_conflict ){
     Trace("uf-ss-assert") << "Assert cardinality " << d_type << " " << c << " " << val << " level = ";
     Trace("uf-ss-assert") << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl;
-    Assert( d_cardinality_literal.find( c )!=d_cardinality_literal.end() );
-    d_cardinality_assertions[ d_cardinality_literal[c] ] = val;
+    Node cl = getCardinalityLiteral( c );
+    d_cardinality_assertions[ cl ] = val;
     if( val ){
       bool doCheckRegions = !d_hasCard;
-      if( !d_hasCard || c<d_cardinality ){
+      bool prevHasCard = d_hasCard;
+      d_hasCard = true;
+      if( !prevHasCard || c<d_cardinality ){
         d_cardinality = c;
+        simpleCheckCardinality();
+        if( d_thss->d_conflict.get() ){
+          return;
+        }
       }
-      d_hasCard = true;
       //should check all regions now
       if( doCheckRegions ){
         for( int i=0; i<(int)d_regions_index; i++ ){
@@ -869,6 +880,7 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
         bool needsCard = true;
         for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){
           if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){
+            Debug("fmf-card-debug") << "..does not need allocate because of " << it->second << std::endl;
             needsCard = false;
             break;
           }
@@ -876,10 +888,13 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int
         if( needsCard ){
           allocateCardinality( out );
         }
+      }else{
+        Debug("fmf-card-debug") << "..already has card = " << d_cardinality << std::endl;
       }
       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 );
+        simpleCheckCardinality();
       }
     }
   }
@@ -997,22 +1012,17 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
       Trace("uf-ss-cliques") << std::endl;
     }
   }
-  /*
-  if( options::ufssSymBreak() ){
-    std::vector< Node > reps;
-    getRepresentatives( reps );
-    if( d_aloc_cardinality>0 ){
-      d_thss->getSymmetryBreaker()->allocateCardinality( out, d_type, d_aloc_cardinality+1, d_cliques[ d_aloc_cardinality ], reps );
-    }else{
-      std::vector< Node > clique;
-      clique.push_back( d_cardinality_term );
-      std::vector< std::vector< Node > > cliques;
-      cliques.push_back( clique );
-      d_thss->getSymmetryBreaker()->allocateCardinality( out, d_type, 1, cliques, reps );
-    }
+
+  //allocate the lowest such that it is not asserted
+  Node cl;
+  do {
+    d_aloc_cardinality = d_aloc_cardinality + 1;
+    cl = getCardinalityLiteral( d_aloc_cardinality );
+  }while( d_cardinality_assertions.find( cl )!=d_cardinality_assertions.end() && !d_cardinality_assertions[cl] );
+  //if one is already asserted postively, abort
+  if( d_cardinality_assertions.find( cl )!=d_cardinality_assertions.end() ){
+    return;
   }
-  */
-  d_aloc_cardinality = d_aloc_cardinality + 1;
 
   //check for abort case
   if( options::ufssAbortCardinality()==d_aloc_cardinality ){
@@ -1042,10 +1052,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
 
     //add splitting lemma for cardinality constraint
     Assert( !d_cardinality_term.isNull() );
-    Node lem = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_term,
-                                                 NodeManager::currentNM()->mkConst( Rational( d_aloc_cardinality ) ) );
-    lem = Rewriter::rewrite(lem);
-    d_cardinality_literal[ d_aloc_cardinality ] = lem;
+    Node lem = getCardinalityLiteral( d_aloc_cardinality );
     lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
     d_cardinality_lemma[ d_aloc_cardinality ] = lem;
     //add as lemma to output channel
@@ -1360,6 +1367,16 @@ Node StrongSolverTheoryUF::SortModel::getTotalityLemmaTerm( int cardinality, int
   //}
 }
 
+void StrongSolverTheoryUF::SortModel::simpleCheckCardinality() {
+  if( d_maxNegCard.get()!=0 && d_hasCard.get() && d_cardinality.get()<d_maxNegCard.get() ){
+    Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ),
+                                                      getCardinalityLiteral( d_maxNegCard.get() ).negate() );
+    Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl;
+    d_thss->getOutputChannel().conflict( lem );
+    d_thss->d_conflict.set( true );
+  }
+}
+
 void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){
   Debug( c ) << "--  Conflict Find:" << std::endl;
   Debug( c ) << "Number of reps = " << d_reps << std::endl;
@@ -1385,7 +1402,7 @@ void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){
   }
 }
 
-void StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){
+bool StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){
   if( Trace.isOn("uf-ss-warn") ){
     std::vector< Node > eqcs;
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( m->d_equalityEngine );
@@ -1404,12 +1421,53 @@ void StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){
       }
       ++eqcs_i;
     }
-    if( (int)eqcs.size()!=d_cardinality ){
-      Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
-      Trace("uf-ss-warn") << "  cardinality : " << d_cardinality << std::endl;
-      Trace("uf-ss-warn") << "  # reps : " << (int)eqcs.size() << std::endl;
+  }
+  int nReps = m->d_rep_set.d_type_reps.find( d_type )==m->d_rep_set.d_type_reps.end() ? 0 : (int)m->d_rep_set.d_type_reps[d_type].size();
+  if( nReps!=d_maxNegCard ){
+    Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
+    Trace("uf-ss-warn") << "   Max neg cardinality : " << d_maxNegCard << std::endl;
+    Trace("uf-ss-warn") << "   # Reps : " << nReps << std::endl;
+    if( d_maxNegCard>nReps ){
+      /*
+      for( unsigned i=0; i<d_fresh_aloc_reps.size(); i++ ){
+        if( add>0 && !m->d_equalityEngine->hasTerm( d_fresh_aloc_reps[i] ) ){
+          m->d_rep_set.d_type_reps[d_type].push_back( d_fresh_aloc_reps[i] );
+          add--;
+        }
+      }
+      for( int i=0; i<add; i++ ){
+        std::stringstream ss;
+        ss << "r_" << d_type << "_";
+        Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "enumeration to meet negative card constraint" );
+        d_fresh_aloc_reps.push_back( nn );
+        m->d_rep_set.d_type_reps[d_type].push_back( nn );
+      }
+      */
+      while( (int)d_fresh_aloc_reps.size()<=d_maxNegCard ){
+        std::stringstream ss;
+        ss << "r_" << d_type << "_";
+        Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "enumeration to meet negative card constraint" );
+        d_fresh_aloc_reps.push_back( nn );
+      }
+      if( d_maxNegCard==1 ){
+        m->d_rep_set.d_type_reps[d_type].push_back( d_fresh_aloc_reps[0] );
+      }else{
+        //must add lemma
+        std::vector< Node > force_cl;
+        for( int i=0; i<=d_maxNegCard; i++ ){
+          for( int j=(i+1); j<=d_maxNegCard; j++ ){
+            force_cl.push_back( d_fresh_aloc_reps[i].eqNode( d_fresh_aloc_reps[j] ).negate() );
+          }
+        }
+        Node cl = getCardinalityLiteral( d_maxNegCard );
+        Node lem = NodeManager::currentNM()->mkNode( OR, cl, NodeManager::currentNM()->mkNode( AND, force_cl ) );
+        Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
+        d_thss->getOutputChannel().lemma( lem );
+        return false;
+      }
     }
   }
+  return true;
 }
 
 int StrongSolverTheoryUF::SortModel::getNumRegions(){
@@ -1436,11 +1494,16 @@ 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();
+  if( d_cardinality_literal.find( c )==d_cardinality_literal.end() ){
+    d_cardinality_literal[c] = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_term,
+                                                                 NodeManager::currentNM()->mkConst( Rational( c ) ) );
+  }
+  return d_cardinality_literal[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_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 )
 {
   if( options::ufssDiseqPropagation() ){
     d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this );
@@ -1521,10 +1584,20 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
     Assert( tn.isSort() );
     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();
+    Node ct = d_rep_model[tn]->getCardinalityTerm();
+    if( lit[0]==ct ){
+      d_rep_model[tn]->assertCardinality( d_out, nCard, polarity );
+      //check if combined cardinality is violated
+      checkCombinedCardinality();
+    }else{
+      //otherwise, make equal via lemma
+      if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){
+        Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
+        Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << lit.iffNode( eqv_lit ) << std::endl;
+        getOutputChannel().lemma( lit.iffNode( eqv_lit ) );
+        d_card_assertions_eqv_lemma[lit] = true;
+      }
+    }
   }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
     d_com_card_assertions[lit] = polarity;
     if( polarity ){
@@ -1650,6 +1723,7 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
     if( tn.isSort() ){
       Trace("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
       rm  = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this );
+      //getOutputChannel().lemma( n.eqNode( rm->getCardinalityTerm() ) );
     }else{
       /*
       if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
@@ -1727,12 +1801,18 @@ int StrongSolverTheoryUF::getCardinality( TypeNode tn ) {
   return -1;
 }
 
+/*
 void StrongSolverTheoryUF::getRepresentatives( Node n, std::vector< Node >& reps ){
   SortModel* c = getSortModel( n );
   if( c ){
     c->getRepresentatives( reps );
+    if( (int)reps.size()!=c->getCardinality() ){
+      Trace("uf-ss-warn") << "Sort " << n.getType() << " has cardinality " << c->getCardinality();
+      Trace("uf-ss-warn") << ", but provided " << reps.size() << " representatives!!!" << std::endl;
+    }
   }
 }
+*/
 
 bool StrongSolverTheoryUF::minimize( TheoryModel* m ){
   for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
@@ -1768,12 +1848,13 @@ void StrongSolverTheoryUF::debugPrint( const char* c ){
   }
 }
 
-void StrongSolverTheoryUF::debugModel( TheoryModel* m ){
-  if( Trace.isOn("uf-ss-warn") ){
-    for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-      it->second->debugModel( m );
+bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){
+  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+    if( !it->second->debugModel( m ) ){
+      return false;
     }
   }
+  return true;
 }
 
 /** initialize */
@@ -1813,8 +1894,8 @@ void StrongSolverTheoryUF::checkCombinedCardinality() {
             }
           }
           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;
+          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 );
         }
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 51783c1e3..f59d46d36 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -171,7 +171,7 @@ public:
     NodeIntMap d_regions_map;
     /** the score for each node for splitting */
     NodeIntMap d_split_score;
-    /** regions used to d_region_index */
+    /** number of valid disequalities in d_disequalities */
     context::CDO< unsigned > d_disequalities_index;
     /** list of all disequalities */
     std::vector< Node > d_disequalities;
@@ -244,11 +244,15 @@ public:
     std::map< int, std::vector< std::vector< Node > > > d_cliques;
     /** maximum negatively asserted cardinality */
     context::CDO< int > d_maxNegCard;
+    /** list of fresh representatives allocated */
+    std::vector< Node > d_fresh_aloc_reps;
   private:
     /** apply totality */
     bool applyTotality( int cardinality );
     /** get totality lemma terms */
     Node getTotalityLemmaTerm( int cardinality, int i );
+    /** simple check cardinality */
+    void simpleCheckCardinality();
   public:
     SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss );
     virtual ~SortModel(){}
@@ -280,6 +284,8 @@ public:
     void getRepresentatives( std::vector< Node >& reps );
     /** has cardinality */
     bool hasCardinalityAsserted() { return d_hasCard; }
+    /** get cardinality term */
+    Node getCardinalityTerm() { return d_cardinality_term; }
     /** get cardinality literal */
     Node getCardinalityLiteral( int c );
     /** get maximum negative cardinality */
@@ -287,7 +293,7 @@ public:
     //print debug
     void debugPrint( const char* c );
     /** debug a model */
-    void debugModel( TheoryModel* m );
+    bool debugModel( TheoryModel* m );
   public:
     /** get number of regions (for debugging) */
     int getNumRegions();
@@ -310,6 +316,8 @@ private:
   std::map< int, Node > d_com_card_literal;
   /** combined cardinality assertions (indexed by cardinality literals ) */
   NodeBoolMap d_com_card_assertions;
+  /** cardinality literals for which we have added */
+  NodeBoolMap d_card_assertions_eqv_lemma;
   /** initialize */
   void initializeCombinedCardinality();
   /** allocateCombinedCardinality */
@@ -365,7 +373,7 @@ public:
   //print debug
   void debugPrint( const char* c );
   /** debug a model */
-  void debugModel( TheoryModel* m );
+  bool debugModel( TheoryModel* m );
 public:
   /** get is in conflict */
   bool isConflict() { return d_conflict; }
@@ -374,7 +382,7 @@ public:
   /** get cardinality for type */
   int getCardinality( TypeNode tn );
   /** get representatives */
-  void getRepresentatives( Node n, std::vector< Node >& reps );
+  //void getRepresentatives( Node n, std::vector< Node >& reps );
   /** minimize */
   bool minimize( TheoryModel* m = NULL );
 
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index b4d1b6d48..128b8ceda 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -65,6 +65,12 @@ public:
       if( valType != nodeManager->integerType() ) {
         throw TypeCheckingExceptionPrivate(n, "cardinality constraint must be integer");
       }
+      if( n[1].getKind()!=kind::CONST_RATIONAL ){
+        throw TypeCheckingExceptionPrivate(n, "cardinality constraint must be a constant");
+      }
+      if( n[1].getConst<Rational>().getNumerator().sgn()!=1 ){
+        throw TypeCheckingExceptionPrivate(n, "cardinality constraint must be positive");
+      }
     }
     return nodeManager->booleanType();
   }