more progress, compiles

SRI-CSL · Apr 11, 2016 · 4de7be0 · 4de7be0
1 parent e42225d
commit 4de7be0
Show file tree

Hide file tree

Showing 5 changed files with 221 additions and 30 deletions.
diff --git a/src/expr/bitvector.cpp b/src/expr/bitvector.cpp
@@ -29,6 +29,11 @@ bitvector::bitvector(size_t size)
 : d_size(size)
 {}
 
+bitvector::bitvector(const bitvector& other)
+: integer(other)
+, d_size(other.d_size)
+{}
+
 /** Construct from integer */
 bitvector::bitvector(size_t size, const integer& z)
 : integer(z)
@@ -114,6 +119,7 @@ std::ostream& operator << (std::ostream& out, const bitvector& bv) {
 }
 
 bitvector& bitvector::set_bit(size_t i, bool value) {
+  assert(i < d_size);
   if (value) {
     mpz_setbit(d_gmp_int.get_mpz_t(), i);
   } else {
@@ -138,42 +144,138 @@ bitvector bitvector::concat(const bitvector& rhs) const {
 }
 
 bitvector bitvector::extract(size_t low, size_t high) const {
+  assert(low < high);
+  assert(high < d_size);
   size_t size = high-low+1;
   integer value(d_gmp_int >> low);
   return bitvector(size, value);
 }
 
 bool bitvector::uleq(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
   return *this <= rhs;
 }
 
 bool bitvector::sleq(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
   return get_signed() <= rhs.get_signed();
 }
 
 bool bitvector::ult(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
   return *this < rhs;
 }
 
 bool bitvector::slt(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
   return get_signed() < rhs.get_signed();
 }
 
 bool bitvector::ugeq(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
   return *this >= rhs;
 }
 
 bool bitvector::sgeq(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
   return get_signed() >= rhs.get_signed();
 }
 
 bool bitvector::ugt(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
   return *this > rhs;
 }
 
 bool bitvector::sgt(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
   return get_signed() > rhs.get_signed();
 }
 
+bitvector bitvector::add(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  return bitvector(d_size, *this + rhs);
+}
+
+bitvector bitvector::sub(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  assert(false);
+  return bitvector();
+}
+
+bitvector bitvector::mul(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  return bitvector(d_size, *this * rhs);
+}
+
+bitvector bitvector::udiv(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  // unsigned division, truncating towards 0. x/0 = 1...1
+  if (rhs.sgn() == 0) {
+    return bitvector(d_size, true);
+  } else {
+    return bitvector(d_size, integer(this->d_gmp_int / rhs.d_gmp_int));
+  }
+}
+
+bitvector bitvector::sdiv(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  return bitvector();
+}
+
+bitvector bitvector::urem(const bitvector& rhs) const {
+  // unsigned remainder from truncating division
+  assert(d_size == rhs.d_size);
+  return bitvector();
+}
+
+bitvector bitvector::srem(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  return bitvector();
+}
+
+bitvector bitvector::smod(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  return bitvector();
+}
+
+bitvector bitvector::shl(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  return bitvector();
+}
+
+bitvector bitvector::lshr(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  if (d_size < rhs.d_gmp_int) {
+    return bitvector(d_size);
+  } else {
+    assert(false);
+    return bitvector();
+  }
+}
+
+bitvector bitvector::ashr(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  return bitvector();
+}
+
+bitvector bitvector::bvxor(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  return bitvector();
+}
+
+bitvector bitvector::bvand(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  return bitvector();
+}
+
+bitvector bitvector::bvor(const bitvector& rhs) const {
+  assert(d_size == rhs.d_size);
+  return bitvector();
+}
+
+bitvector bitvector::bvnot() const {
+  return bitvector();
+}
+
 }
 }
diff --git a/src/expr/bitvector.h b/src/expr/bitvector.h
@@ -35,6 +35,9 @@ class bitvector : protected integer {
   /** Construct 0 of size 1 */
   bitvector(): d_size(1) {}
 
+  /** Copy constructor */
+  bitvector(const bitvector& other);
+
   /** Construct 0 */
   explicit bitvector(size_t size);
 
@@ -75,9 +78,28 @@ class bitvector : protected integer {
   /** Set the bit to value (returns self-reference) */
   bitvector& set_bit(size_t i, bool value);
 
-  /** Operations */
   bitvector concat(const bitvector& rhs) const;
   bitvector extract(size_t low, size_t high) const;
+
+  bitvector add(const bitvector& rhs) const;
+  bitvector sub(const bitvector& rhs) const;
+  bitvector mul(const bitvector& rhs) const;
+
+  bitvector udiv(const bitvector& rhs) const;
+  bitvector sdiv(const bitvector& rhs) const;
+  bitvector urem(const bitvector& rhs) const;
+  bitvector srem(const bitvector& rhs) const;
+  bitvector smod(const bitvector& rhs) const;
+
+  bitvector shl(const bitvector& rhs) const;
+  bitvector lshr(const bitvector& rhs) const;
+  bitvector ashr(const bitvector& rhs) const;
+
+  bitvector bvxor(const bitvector& rhs) const;
+  bitvector bvand(const bitvector& rhs) const;
+  bitvector bvor(const bitvector& rhs) const;
+  bitvector bvnot() const;
+
   bool uleq(const bitvector& rhs) const;
   bool sleq(const bitvector& rhs) const;
   bool ult(const bitvector& rhs) const;

diff --git a/src/expr/integer.cpp b/src/expr/integer.cpp
@@ -63,6 +63,14 @@ int integer::sgn() const {
   return mpz_sgn(d_gmp_int.get_mpz_t());
 }
 
+unsigned long integer::get_unsigned() const {
+  return d_gmp_int.get_ui();
+}
+
+signed long integer::get_signed() const {
+  return d_gmp_int.get_si();
+}
+
 integer integer::operator + (const integer& other) const {
   return integer(d_gmp_int + other.d_gmp_int);
 }

diff --git a/src/expr/integer.h b/src/expr/integer.h
@@ -70,8 +70,15 @@ class integer {
   bool operator > (const integer& other) const;
   bool operator >= (const integer& other) const;
 
+  /** Get the sign */
   int sgn() const;
 
+  /** Get unsigned value */
+  unsigned long get_unsigned() const;
+
+  /** Get signed value */
+  signed long get_signed() const;
+
   /** Returns the hash of the integer */
   size_t hash() const { return d_gmp_int.get_si(); }
 

diff --git a/src/expr/model.cpp b/src/expr/model.cpp
@@ -350,51 +350,103 @@ class evaluation_visitor {
     case CONST_BITVECTOR:
       v = d_tm.get_bitvector_constant(t_term);
       break;
-    case TERM_BV_ADD:
-      assert(false);
+    case TERM_BV_ADD: {
+      bitvector bv = children_values[0].get_bitvector();
+      for (size_t i = 0; i < children_values.size(); ++ i) {
+        bv = bv.add(children_values[i].get_bitvector());
+      }
+      v = bv;
       break;
-    case TERM_BV_SUB:
-      assert(false);
+    }
+    case TERM_BV_SUB: {
+      const bitvector& lhs = children_values[0].get_bitvector();
+      const bitvector& rhs = children_values[0].get_bitvector();
+      v = lhs.sub(rhs);
       break;
-    case TERM_BV_MUL:
-      assert(false);
+    }
+    case TERM_BV_MUL: {
+      bitvector bv = children_values[0].get_bitvector();
+      for (size_t i = 0; i < children_values.size(); ++ i) {
+        bv = bv.mul(children_values[i].get_bitvector());
+      }
+      v = bv;
       break;
-    case TERM_BV_UDIV: // NOTE: semantics of division is x/0 = 111...111
-      assert(false);
+    }
+    case TERM_BV_UDIV: { // NOTE: semantics of division is x/0 = 111...111
+      const bitvector& lhs = children_values[0].get_bitvector();
+      const bitvector& rhs = children_values[0].get_bitvector();
+      v = lhs.udiv(rhs);
       break;
-    case TERM_BV_SDIV:
-      assert(false);
+    }
+    case TERM_BV_SDIV: {
+      const bitvector& lhs = children_values[0].get_bitvector();
+      const bitvector& rhs = children_values[0].get_bitvector();
+      v = lhs.sdiv(rhs);
       break;
-    case TERM_BV_UREM:
-      assert(false);
+    }
+    case TERM_BV_UREM: {
+      const bitvector& lhs = children_values[0].get_bitvector();
+      const bitvector& rhs = children_values[0].get_bitvector();
+      v = lhs.urem(rhs);
       break;
-    case TERM_BV_SREM:
-      assert(false);
+    }
+    case TERM_BV_SREM: {
+      const bitvector& lhs = children_values[0].get_bitvector();
+      const bitvector& rhs = children_values[0].get_bitvector();
+      v = lhs.srem(rhs);
       break;
-    case TERM_BV_SMOD:
-      assert(false);
+    }
+    case TERM_BV_SMOD: {
+      const bitvector& lhs = children_values[0].get_bitvector();
+      const bitvector& rhs = children_values[0].get_bitvector();
+      v = lhs.smod(rhs);
       break;
-    case TERM_BV_XOR:
-      assert(false);
+    }
+    case TERM_BV_XOR: {
+      bitvector bv = children_values[0].get_bitvector();
+      for (size_t i = 0; i < children_values.size(); ++ i) {
+        bv = bv.bvxor(children_values[i].get_bitvector());
+      }
+      v = bv;
       break;
-    case TERM_BV_SHL:
-      assert(false);
+    }
+    case TERM_BV_SHL: {
+      const bitvector& lhs = children_values[0].get_bitvector();
+      const bitvector& rhs = children_values[0].get_bitvector();
+      v = lhs.shl(rhs);
       break;
-    case TERM_BV_LSHR:
-      assert(false);
+    }
+    case TERM_BV_LSHR: {
+      const bitvector& lhs = children_values[0].get_bitvector();
+      const bitvector& rhs = children_values[0].get_bitvector();
+      v = lhs.lshr(rhs);
       break;
-    case TERM_BV_ASHR:
-      assert(false);
+    }
+    case TERM_BV_ASHR: {
+      const bitvector& lhs = children_values[0].get_bitvector();
+      const bitvector& rhs = children_values[0].get_bitvector();
+      v = lhs.ashr(rhs);
       break;
+    }
     case TERM_BV_NOT:
-      assert(false);
+      v = children_values[0].get_bitvector().bvnot();
       break;
-    case TERM_BV_AND:
-      assert(false);
+    case TERM_BV_AND: {
+      bitvector bv = children_values[0].get_bitvector();
+      for (size_t i = 0; i < children_values.size(); ++ i) {
+        bv = bv.bvand(children_values[i].get_bitvector());
+      }
+      v = bv;
       break;
-    case TERM_BV_OR:
-      assert(false);
+    }
+    case TERM_BV_OR: {
+      bitvector bv = children_values[0].get_bitvector();
+      for (size_t i = 0; i < children_values.size(); ++ i) {
+        bv = bv.bvor(children_values[i].get_bitvector());
+      }
+      v = bv;
       break;
+    }
     case TERM_BV_NAND:
       assert(false);
       break;