Merge pull request #4350 from romainbrenguier/bugfix/bdd-var-type

Fix type of bddVar argument

Author: tautschnig

src/solvers/bdd/bdd_cudd.h

@@ -35,8 +35,11 @@ class bdd_nodet
     return Cudd_IsComplement(node) != 0;
   }
 
+  /// Type of indexes of Boolean variables
+  using indext = int;
+
   /// Label on the node, corresponds to the index of a Boolean variable
-  std::size_t index() const
+  indext index() const
   {
     return Cudd_NodeReadIndex(node);
   }
@@ -147,7 +150,7 @@ class bdd_managert
     return bddt(cudd.bddZero());
   }
 
-  bddt bdd_variable(std::size_t index)
+  bddt bdd_variable(bdd_nodet::indext index)
   {
     return bddt(cudd.bddVar(index));
   }

src/solvers/bdd/bdd_miniBDD.h

@@ -39,8 +39,11 @@ class bdd_nodet
     return node->node_number == 0;
   }
 
+  /// Type of indexes of Boolean variables
+  using indext = std::size_t;
+
   /// Label on the node, corresponds to the index of a Boolean variable
-  std::size_t index() const
+  indext index() const
   {
     return bdd_var_to_index.at(node->var);
   }
@@ -158,7 +161,7 @@ class bdd_managert : private mini_bdd_mgrt
     return bddt(False());
   }
 
-  bddt bdd_variable(std::size_t index)
+  bddt bdd_variable(bdd_nodet::indext index)
   {
     auto it = index_to_bdd.find(index);
     if(it != index_to_bdd.end())

src/solvers/prop/bdd_expr.cpp

@@ -11,6 +11,7 @@ Author: Michael Tautschnig, [email protected]
 
 #include "bdd_expr.h"
 
+#include <util/arith_tools.h>
 #include <util/expr_util.h>
 #include <util/format_expr.h>
 #include <util/invariant.h>
@@ -111,8 +112,9 @@ exprt bdd_exprt::as_expr(
       return true_exprt();
   }
 
-  INVARIANT(r.index() < node_map.size(), "Index should be in node_map");
-  const exprt &n_expr = node_map[r.index()];
+  auto index = numeric_cast_v<std::size_t>(r.index());
+  INVARIANT(index < node_map.size(), "Index should be in node_map");
+  const exprt &n_expr = node_map[index];
 
   // Look-up cache for already computed value
   auto insert_result = cache.emplace(r.id(), nil_exprt());