uint is non-standard (#339)

This prevents compilation of smt-switch with alternative libc implementations like musl.

include/generic_solver.h

@@ -38,8 +38,8 @@ class GenericSolver : public AbsSmtSolver
  public:
   GenericSolver(std::string path,
                 std::vector<std::string> cmd_line_args,
-                uint write_buf_size = 256,
-                uint read_buf_size = 256);
+                unsigned int write_buf_size = 256,
+                unsigned int read_buf_size = 256);
   ~GenericSolver();
 
   /***************************************************************/
@@ -168,28 +168,28 @@ class GenericSolver : public AbsSmtSolver
    * desired bv value. width is the bit-width returns a bv term of width `width`
    * whose value is (-1) * abs_decimal.
    * */
-  Term make_non_negative_bv_const(std::string abs_decimal, uint width) const;
+  Term make_non_negative_bv_const(std::string abs_decimal, unsigned int width) const;
 
   /** helper function for bv constant
    * abs_decimal is the absolute value of the desired bit-vector.
    * width is the bit-width
    * returns a bv term of width `width` whose value is abs_value.
    * */
-  Term make_non_negative_bv_const(int64_t abs_value, uint width) const;
+  Term make_non_negative_bv_const(int64_t abs_value, unsigned int width) const;
 
   /** helper function for bv constant
    * abs_decimal is the string represnentation of the absolute value of the
    * desired bv value. width is the bit-width returns a bv term of width `width`
    * whose value is abs_decimal.
    * */
-  Term make_negative_bv_const(std::string abs_decimal, uint width) const;
+  Term make_negative_bv_const(std::string abs_decimal, unsigned int width) const;
 
   /** helper function for bv constant
    * abs_decimal is the absolute value of the desired bit-vector.
    * width is the bit-width
    * returns a bv term of width `width` whose value is (-1) * abs_value.
    * */
-  Term make_negative_bv_const(int64_t abs_value, uint width) const;
+  Term make_negative_bv_const(int64_t abs_value, unsigned int width) const;
 
   // open a connection to the binary via a pipe
   void start_solver();
@@ -241,8 +241,8 @@ class GenericSolver : public AbsSmtSolver
   char * read_buf;
 
   // buffer sizes
-  uint write_buf_size;
-  uint read_buf_size;
+  unsigned int write_buf_size;
+  unsigned int read_buf_size;
 
   // tracks the context level of the solver
   // (e.g., number of pushes - number of pops)
@@ -253,7 +253,7 @@ class GenericSolver : public AbsSmtSolver
   std::unique_ptr<std::unordered_map<Sort, std::string>> sort_name_map;
 
   // internal counter for naming terms
-  uint * term_counter;
+  unsigned int * term_counter;
 
   // maps between Term name and actual Term and vice versa
   std::unique_ptr<std::unordered_map<std::string, Term>> name_term_map;

src/generic_solver.cpp

@@ -67,8 +67,8 @@ std::string & trim(std::string & str)
 // class methods implementation
 GenericSolver::GenericSolver(string path,
                              vector<string> cmd_line_args,
-                             uint write_buf_size,
-                             uint read_buf_size)
+                             unsigned int write_buf_size,
+                             unsigned int read_buf_size)
     : AbsSmtSolver(SolverEnum::GENERIC_SOLVER),
       path(path),
       cmd_line_args(cmd_line_args),
@@ -95,7 +95,7 @@ GenericSolver::GenericSolver(string path,
         "Generic Solvers require a buffer size of at least 2 and at most 256.");
     throw IncorrectUsageException(msg);
   }
-  term_counter = new uint;
+  term_counter = new unsigned int;
   //allocate memory for the buffers
   write_buf = new char[write_buf_size];
   read_buf = new char[read_buf_size];
@@ -170,14 +170,14 @@ void GenericSolver::start_solver() {
 void GenericSolver::write_internal(string str) const
 {
   // track how many charas were written so far
-  uint written_chars = 0;
+  unsigned int written_chars = 0;
   // continue writing  until entire str was written
   while (written_chars < str.size())
   {
     // how many characters are there left to write
-    uint remaining = str.size() - written_chars;
+    unsigned int remaining = str.size() - written_chars;
     // how many characters are we writing in this iteration
-    uint substr_size;
+    unsigned int substr_size;
     if (remaining < write_buf_size)
     {
       substr_size = remaining;
@@ -775,29 +775,29 @@ Term GenericSolver::store_term(Term term) const
 }
 
 Term GenericSolver::make_non_negative_bv_const(string abs_decimal,
-                                               uint width) const
+                                               unsigned int width) const
 {
   Sort bvsort = make_sort(BV, width);
   string repr = "(_ bv" + abs_decimal + " " + std::to_string(width) + ")";
   Term term = std::make_shared<GenericTerm>(bvsort, Op(), TermVec{}, repr);
   return term;
 }
 
-Term GenericSolver::make_non_negative_bv_const(int64_t i, uint width) const
+Term GenericSolver::make_non_negative_bv_const(int64_t i, unsigned int width) const
 {
   assert(i >= 0);
   return make_non_negative_bv_const(std::to_string(i), width);
 }
 
-Term GenericSolver::make_negative_bv_const(string abs_decimal, uint width) const
+Term GenericSolver::make_negative_bv_const(string abs_decimal, unsigned int width) const
 {
   Term zero = make_non_negative_bv_const("0", width);
   Term abs = make_non_negative_bv_const(abs_decimal, width);
   Term result = make_term(BVSub, zero, abs);
   return result;
 }
 
-Term GenericSolver::make_negative_bv_const(int64_t abs_value, uint width) const
+Term GenericSolver::make_negative_bv_const(int64_t abs_value, unsigned int width) const
 {
   assert(abs_value >= 0);
   return make_negative_bv_const(std::to_string(abs_value), width);