Fix type of bddVar argument

The function bdd_variable takes a size_t for miniBdd while cudd.bddVar
takes an int.
We make this type dependent of the implementation by defining an indext,
which will avoid having to do conversions.

Author: romainbrenguier

src/solvers/bdd/bdd_cudd.h

@@ -15,7 +15,9 @@ Author: Romain Brenguier, [email protected]
 #ifndef CPROVER_SOLVERS_BDD_BDD_CUDD_H
 #define CPROVER_SOLVERS_BDD_BDD_CUDD_H
 
-#include <cplusplus/cuddObj.hh>
+#include <cplusplus/cuddObj.hh>s
+
+#include <util/arith_tools.h>
 
 class bdd_managert;
 class bddt;
@@ -35,8 +37,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 +152,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())