From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 27 Nov 2018 21:19:32 +0000 (-0600)
Subject: Fix coverity warnings in datatypes (#2553)
X-Git-Tag: cvc5-1.0.0~4350
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=711234e01a17289d1fa4af3574ddf5d6de2405a1;p=cvc5.git

Fix coverity warnings in datatypes (#2553)

This caches some information regarding tester applications and changes int -> size_t in a few places.
---

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 2fee4f48d..526ca2d4a 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -538,9 +538,10 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
     // enumerator is only specific to variable agnostic symmetry breaking
     e = Node::null();
   }
-  std::map<unsigned, Node>::iterator it =
-      d_simple_sb_pred[e][tn][tindex][optHashVal].find(depth);
-  if (it != d_simple_sb_pred[e][tn][tindex][optHashVal].end())
+  std::map<unsigned, Node>& ssbCache =
+      d_simple_sb_pred[e][tn][tindex][optHashVal];
+  std::map<unsigned, Node>::iterator it = ssbCache.find(depth);
+  if (it != ssbCache.end())
   {
     return it->second;
   }
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 6aed1514c..77579489a 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -488,7 +488,8 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
   //add to tester if applicable
   Node t_arg;
   int tindex = DatatypesRewriter::isTester( atom, t_arg );
-  if( tindex!=-1 ){
+  if (tindex >= 0)
+  {
     Trace("dt-tester") << "Assert tester : " << atom << " for " << t_arg << std::endl;
     Node rep = getRepresentative( t_arg );
     EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
@@ -863,17 +864,16 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
 
 
       //merge labels
-      NodeIntMap::iterator lbl_i = d_labels.find( t2 );
+      NodeUIntMap::iterator lbl_i = d_labels.find(t2);
       if( lbl_i != d_labels.end() ){
         Trace("datatypes-debug") << "  merge labels from " << eqc2 << " " << t2 << std::endl;
-        int n_label = (*lbl_i).second;
-        for( int i=0; i<n_label; i++ ){
-          Assert( i<(int)d_labels_data[ t2 ].size() );
+        size_t n_label = (*lbl_i).second;
+        for (size_t i = 0; i < n_label; i++)
+        {
+          Assert(i < d_labels_data[t2].size());
           Node t = d_labels_data[ t2 ][i];
-          Node tt = t.getKind()==kind::NOT ? t[0] : t;
-          Node t_arg;
-          int tindex = DatatypesRewriter::isTester( tt, t_arg );
-          Assert( tindex!=-1 );
+          Node t_arg = d_labels_args[t2][i];
+          unsigned tindex = d_labels_tindex[t2][i];
           addTester( tindex, t, eqc1, t1, t_arg );
           if( d_conflict ){
             Trace("datatypes-debug") << "  conflict!" << std::endl;
@@ -887,11 +887,12 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         eqc1->d_selectors = true;
         checkInst = true;
       }
-      NodeIntMap::iterator sel_i = d_selector_apps.find( t2 );
+      NodeUIntMap::iterator sel_i = d_selector_apps.find(t2);
       if( sel_i != d_selector_apps.end() ){
         Trace("datatypes-debug") << "  merge selectors from " << eqc2 << " " << t2 << std::endl;
-        int n_sel = (*sel_i).second;
-        for( int j=0; j<n_sel; j++ ){
+        size_t n_sel = (*sel_i).second;
+        for (size_t j = 0; j < n_sel; j++)
+        {
           addSelector( d_selector_apps_data[t2][j], eqc1, t1, eqc2->d_constructor.get().isNull() );
         }
       }
@@ -923,9 +924,9 @@ bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){
 }
 
 Node TheoryDatatypes::getLabel( Node n ) {
-  NodeIntMap::iterator lbl_i = d_labels.find( n );
+  NodeUIntMap::iterator lbl_i = d_labels.find(n);
   if( lbl_i != d_labels.end() ){
-    unsigned n_lbl = (*lbl_i).second;
+    size_t n_lbl = (*lbl_i).second;
     if( n_lbl>0 && d_labels_data[n][ n_lbl-1 ].getKind()!=kind::NOT ){
       return d_labels_data[n][ n_lbl-1 ];
     }
@@ -949,7 +950,7 @@ int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
 }
 
 bool TheoryDatatypes::hasTester( Node n ) {
-  NodeIntMap::iterator lbl_i = d_labels.find( n );
+  NodeUIntMap::iterator lbl_i = d_labels.find(n);
   if( lbl_i != d_labels.end() ){
     return (*lbl_i).second>0;
   }else{
@@ -965,14 +966,13 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
   if( lindex!=-1 ){
     pcons[ lindex ] = true;
   }else{
-    NodeIntMap::iterator lbl_i = d_labels.find( n );
+    NodeUIntMap::iterator lbl_i = d_labels.find(n);
     if( lbl_i != d_labels.end() ){
-      int n_lbl = (*lbl_i).second;
-      for( int i=0; i<n_lbl; i++ ){
-        Node t = d_labels_data[n][i];
-        Assert( t.getKind()==NOT );
-        int tindex = DatatypesRewriter::isTester( t[0] );
-        Assert( tindex!=-1 );
+      size_t n_lbl = (*lbl_i).second;
+      for (size_t i = 0; i < n_lbl; i++)
+      {
+        Assert(d_labels_data[n][i].getKind() == NOT);
+        unsigned tindex = d_labels_tindex[n][i];
         pcons[ tindex ] = false;
       }
     }
@@ -1009,16 +1009,21 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) {
   }
 }
 
-void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg ){
+void TheoryDatatypes::addTester(
+    unsigned ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg)
+{
   Trace("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl;
   Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
   bool tpolarity = t.getKind()!=NOT;
   Node j, jt;
   bool makeConflict = false;
-  int jtindex0 = getLabelIndex( eqc, n );
-  if( jtindex0!=-1 ){
+  int prevTIndex = getLabelIndex(eqc, n);
+  if (prevTIndex >= 0)
+  {
+    unsigned ptu = static_cast<unsigned>(prevTIndex);
     //if we already know the constructor type, check whether it is in conflict or redundant
-    if( (jtindex0==ttindex)!=tpolarity ){
+    if ((ptu == ttindex) != tpolarity)
+    {
       if( !eqc->d_constructor.get().isNull() ){
         //conflict because equivalence class contains a constructor
         std::vector< TNode > assumptions;
@@ -1040,19 +1045,18 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
     }
   }else{
     //otherwise, scan list of labels
-    NodeIntMap::iterator lbl_i = d_labels.find( n );
+    NodeUIntMap::iterator lbl_i = d_labels.find(n);
     Assert( lbl_i != d_labels.end() );
-    int n_lbl = (*lbl_i).second;
+    size_t n_lbl = (*lbl_i).second;
     std::map< int, bool > neg_testers;
-    for( int i=0; i<n_lbl; i++ ){
-      Node ti = d_labels_data[n][i];
-      Assert( ti.getKind()==NOT );
-      j = ti;
-      jt = j[0];
-      int jtindex = DatatypesRewriter::isTester( jt );
-      Assert( jtindex!=-1 );
+    for (size_t i = 0; i < n_lbl; i++)
+    {
+      Assert(d_labels_data[n][i].getKind() == NOT);
+      unsigned jtindex = d_labels_tindex[n][i];
       if( jtindex==ttindex ){
         if( tpolarity ){  //we are in conflict
+          j = d_labels_data[n][i];
+          jt = j[0];
           makeConflict = true;
           break;
         }else{            //it is redundant
@@ -1064,12 +1068,17 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
     }
     if( !makeConflict ){
       Debug("datatypes-labels") << "Add to labels " << t << std::endl;
-      //lbl->push_back( t );
       d_labels[n] = n_lbl + 1;
-      if( n_lbl<(int)d_labels_data[n].size() ){
+      if (n_lbl < d_labels_data[n].size())
+      {
+        // reuse spot in the vector
         d_labels_data[n][n_lbl] = t;
+        d_labels_args[n][n_lbl] = t_arg;
+        d_labels_tindex[n][n_lbl] = ttindex;
       }else{
-        d_labels_data[n].push_back( t );
+        d_labels_data[n].push_back(t);
+        d_labels_args[n].push_back(t_arg);
+        d_labels_tindex[n].push_back(ttindex);
       }
       n_lbl++;
       
@@ -1077,8 +1086,8 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
       Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl;
       if( tpolarity ){
         instantiate( eqc, n );
-        //TODO : and it is not the other testers FIXME
-        for( int i=0; i<(int)dt.getNumConstructors(); i++ ){
+        for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+        {
           if( i!=ttindex && neg_testers.find( i )==neg_testers.end() ){
             Assert( n.getKind()!=APPLY_CONSTRUCTOR );
             Node infer = DatatypesRewriter::mkTester( n, i, dt ).negate();
@@ -1090,8 +1099,8 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
       }else{
         //check if we have reached the maximum number of testers
         // in this case, add the positive tester
-        //this should not be done for sygus, since cases may be limited
-        if( n_lbl==(int)dt.getNumConstructors()-1 ){
+        if (n_lbl == dt.getNumConstructors() - 1)
+        {
           std::vector< bool > pcons;
           getPossibleCons( eqc, n, pcons );
           int testerIndex = -1;
@@ -1105,15 +1114,12 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
           //we must explain why each term in the set of testers for this equivalence class is equal
           std::vector< Node > eq_terms;
           NodeBuilder<> nb(kind::AND);
-          //for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-          
-          for( int i=0; i<n_lbl; i++ ){
+          for (unsigned i = 0; i < n_lbl; i++)
+          {
             Node ti = d_labels_data[n][i];
             nb << ti;
             Assert( ti.getKind()==NOT );
-            Node t_arg2;
-            DatatypesRewriter::isTester( ti[0], t_arg2 );
-            //Assert( tindex!=-1 );
+            Node t_arg2 = d_labels_args[n][i];
             if( std::find( eq_terms.begin(), eq_terms.end(), t_arg2 )==eq_terms.end() ){
               eq_terms.push_back( t_arg2 );
               if( t_arg2!=t_arg ){
@@ -1149,11 +1155,12 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node
 void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) {
   Trace("dt-collapse-sel") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl;
   //check to see if it is redundant
-  NodeIntMap::iterator sel_i = d_selector_apps.find( n );
+  NodeUIntMap::iterator sel_i = d_selector_apps.find(n);
   Assert( sel_i != d_selector_apps.end() );
   if( sel_i != d_selector_apps.end() ){
-    int n_sel = (*sel_i).second;
-    for( int j=0; j<n_sel; j++ ){
+    size_t n_sel = (*sel_i).second;
+    for (size_t j = 0; j < n_sel; j++)
+    {
       Node ss = d_selector_apps_data[n][j];
       if( s.getOperator()==ss.getOperator() && ( s.getKind()!=DT_HEIGHT_BOUND || s[1]==ss[1] ) ){
         Trace("dt-collapse-sel") << "...redundant." << std::endl;
@@ -1163,7 +1170,8 @@ void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFact
     //add it to the vector
     //sel->push_back( s );
     d_selector_apps[n] = n_sel + 1;
-    if( n_sel<(int)d_selector_apps_data[n].size() ){
+    if (n_sel < d_selector_apps_data[n].size())
+    {
       d_selector_apps_data[n][n_sel] = s;
     }else{
       d_selector_apps_data[n].push_back( s );
@@ -1181,16 +1189,18 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
   Trace("datatypes-debug") << "Add constructor : " << c << " to eqc(" << n << ")" << std::endl;
   Assert( eqc->d_constructor.get().isNull() );
   //check labels
-  NodeIntMap::iterator lbl_i = d_labels.find( n );
+  NodeUIntMap::iterator lbl_i = d_labels.find(n);
   if( lbl_i != d_labels.end() ){
     size_t constructorIndex = DatatypesRewriter::indexOf(c.getOperator());
-    int n_lbl = (*lbl_i).second;
-    for( int i=0; i<n_lbl; i++ ){
+    size_t n_lbl = (*lbl_i).second;
+    for (size_t i = 0; i < n_lbl; i++)
+    {
       Node t = d_labels_data[n][i];
-      if( t.getKind()==NOT ){
-        int tindex = DatatypesRewriter::isTester( t[0] );
-        Assert( tindex!=-1 );
-        if( tindex==(int)constructorIndex ){
+      if (d_labels_data[n][i].getKind() == NOT)
+      {
+        unsigned tindex = d_labels_tindex[n][i];
+        if (tindex == constructorIndex)
+        {
           std::vector< TNode > assumptions;
           explain( t, assumptions );
           explainEquality( c, t[0][0], true, assumptions );
@@ -1204,10 +1214,11 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
     }
   }
   //check selectors
-  NodeIntMap::iterator sel_i = d_selector_apps.find( n );
+  NodeUIntMap::iterator sel_i = d_selector_apps.find(n);
   if( sel_i != d_selector_apps.end() ){
-    int n_sel = (*sel_i).second;
-    for( int j=0; j<n_sel; j++ ){
+    size_t n_sel = (*sel_i).second;
+    for (size_t j = 0; j < n_sel; j++)
+    {
       Node s = d_selector_apps_data[n][j];
       //collapse the selector
       collapseSelector( s, c );
@@ -2121,18 +2132,20 @@ void TheoryDatatypes::printModelDebug( const char* c ){
           if( hasLabel( ei, eqc ) ){
             Trace( c ) << getLabel( eqc );
           }else{
-            NodeIntMap::iterator lbl_i = d_labels.find( eqc );
+            NodeUIntMap::iterator lbl_i = d_labels.find(eqc);
             if( lbl_i != d_labels.end() ){
-              for( int j=0; j<(*lbl_i).second; j++ ){
+              for (size_t j = 0; j < (*lbl_i).second; j++)
+              {
                 Trace( c ) << d_labels_data[eqc][j] << " ";
               }
             }
           }
           Trace( c ) << std::endl;
           Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes, " : "no " );
-          NodeIntMap::iterator sel_i = d_selector_apps.find( eqc );
+          NodeUIntMap::iterator sel_i = d_selector_apps.find(eqc);
           if( sel_i != d_selector_apps.end() ){
-            for( int j=0; j<(*sel_i).second; j++ ){
+            for (size_t j = 0; j < (*sel_i).second; j++)
+            {
               Trace( c ) << d_selector_apps_data[eqc][j] << " ";
             }
           }
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index de2863718..0a3017058 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -42,7 +42,8 @@ namespace datatypes {
 class TheoryDatatypes : public Theory {
  private:
   typedef context::CDList<Node> NodeList;
-  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+  /** maps nodes to an index in a vector */
+  typedef context::CDHashMap<Node, size_t, NodeHashFunction> NodeUIntMap;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
 
@@ -159,21 +160,38 @@ private:
   std::map< Node, EqcInfo* > d_eqc_info;
   /** map from nodes to their instantiated equivalent for each constructor type */
   std::map< Node, std::map< int, Node > > d_inst_map;
-  /** which instantiation lemmas we have sent */
-  //std::map< Node, std::vector< Node > > d_inst_lemmas;
+  //---------------------------------labels
   /** labels for each equivalence class
-   * for each eqc n, d_labels[n] is testers that hold for this equivalence class, either:
+   *
+   * For each eqc r, d_labels[r] is testers that hold for this equivalence
+   * class, either:
    * a list of equations of the form
-   *   NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers
-   *   and n is less than the number of possible constructors for t minus one,
+   *   NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ), each of
+   *   which are unique testers, n is less than the number of possible
+   *   constructors for t minus one,
    * or a list of equations of the form
-   *   NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t )  followed by
-   *   is_[constructor_(n+1)]( t ), each of which is a unique tester.
-  */
-  NodeIntMap d_labels;
+   *   NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ) followed by
+   *   is_[constructor_(n+1)]( t{n+1} ), each of which is a unique tester.
+   * In both cases, t1, ..., tn, t{n+1} are terms in the equivalence class of r.
+   *
+   * We store this list in a context-dependent way, using the four data
+   * structures below. The three vectors d_labels_data, d_labels_args, and
+   * d_labels_tindex store the tester applications, their arguments and the
+   * tester index of the application. The map d_labels stores the number of
+   * values in these vectors that is valid in the current context (this is an
+   * optimization that ensures we don't need to pop data when changing SAT
+   * contexts).
+   */
+  NodeUIntMap d_labels;
+  /** the tester applications */
   std::map< Node, std::vector< Node > > d_labels_data;
+  /** the argument of each node in d_labels_data */
+  std::map<Node, std::vector<Node> > d_labels_args;
+  /** the tester index of each node in d_labels_data */
+  std::map<Node, std::vector<unsigned> > d_labels_tindex;
+  //---------------------------------end labels
   /** selector apps for eqch equivalence class */
-  NodeIntMap d_selector_apps;
+  NodeUIntMap d_selector_apps;
   std::map< Node, std::vector< Node > > d_selector_apps_data;
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
@@ -300,7 +318,7 @@ private:
 
  private:
   /** add tester to equivalence class info */
-  void addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg );
+  void addTester(unsigned ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg);
   /** add selector to equivalence class info */
   void addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts = true );
   /** add constructor */