Fix compiler warnings. (#5305)

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index df715675dd0a15a087d2494326a3077127a92094..6c2901bd3885fa78f77dbfb1334d77e08051f37d 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -41,7 +41,7 @@ bool RepSet::hasRep(TypeNode tn, Node n) const
   }
 }
 
-unsigned RepSet::getNumRepresentatives(TypeNode tn) const
+size_t RepSet::getNumRepresentatives(TypeNode tn) const
 {
   const std::vector<Node>* reps = getTypeRepsOrNull(tn);
   return (reps != nullptr) ? reps->size() : 0;

diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 6e1ed1227bb08697633bf6d0bb3203f45761989d..acf2147872db3858bbad55c52481e58518c474a7 100644 (file)
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -71,7 +71,7 @@ class RepSet {
   /** does this set have representative n of type tn? */
   bool hasRep(TypeNode tn, Node n) const;
   /** get the number of representatives for type */
-  unsigned getNumRepresentatives(TypeNode tn) const;
+  size_t getNumRepresentatives(TypeNode tn) const;
   /** get representative at index */
   Node getRepresentative(TypeNode tn, unsigned i) const;
   /**

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index f24a058a3d59e43eb44d0fd01977516e5b42f523..b51e40a6c36eadcbd2f4571dc44f00ce12060095 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -887,9 +887,11 @@ void SortModel::assertCardinality(uint32_t c, bool val)
     }
     else
     {
-      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 );
+      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();
       }
     }
@@ -1139,8 +1141,11 @@ bool SortModel::checkLastCall()
   size_t nReps = rs->getNumRepresentatives(d_type);
   if (nReps != d_maxNegCard + 1)
   {
-    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") << "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)
     {
@@ -1148,7 +1153,8 @@ bool SortModel::checkLastCall()
       {
         std::stringstream ss;
         ss << "r_" << d_type << "_";
-        Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "enumeration to meet negative card constraint" );
+        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 == 0)
@@ -1163,7 +1169,8 @@ bool SortModel::checkLastCall()
         {
           for (size_t j = (i + 1); j <= d_maxNegCard; j++)
           {
-            force_cl.push_back( d_fresh_aloc_reps[i].eqNode( d_fresh_aloc_reps[j] ).negate() );
+            force_cl.push_back(
+                d_fresh_aloc_reps[i].eqNode(d_fresh_aloc_reps[j]).negate());
           }
         }
         Node cl = getCardinalityLiteral( d_maxNegCard );