4 files changed, 26 insertions, 57 deletions

diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index cb001415..54f6b0af 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -90,7 +90,7 @@ namespace klee {
     AssignmentEvaluator v(*this);
     for (; begin!=end; ++begin) {
       ref<Expr> res = v.visit(*begin);
-      if (!res.isConstant() || !res.getConstantValue())
+      if (!res.isConstant() || !res->getConstantValue())
         return false;
     }
     return true;
diff --git a/include/klee/util/ExprHashMap.h b/include/klee/util/ExprHashMap.h
index d9f95bff..d2e6cb1a 100644
--- a/include/klee/util/ExprHashMap.h
+++ b/include/klee/util/ExprHashMap.h
@@ -19,7 +19,7 @@ namespace klee {
   namespace util {
     struct ExprHash  {
       unsigned operator()(const ref<Expr> e) const {
-        return e.hash();
+        return e->hash();
       }
     };
     
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h
index 3729b5c2..b40b9e02 100644
--- a/include/klee/util/ExprRangeEvaluator.h
+++ b/include/klee/util/ExprRangeEvaluator.h
@@ -89,9 +89,9 @@ T ExprRangeEvaluator<T>::evalRead(const UpdateList &ul,
 
 template<class T>
 T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
-  switch (e.getKind()) {
+  switch (e->getKind()) {
   case Expr::Constant:
-    return T(e.getConstantValue());
+    return T(e->getConstantValue());
 
   case Expr::NotOptimized: 
     break;
@@ -131,37 +131,37 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
 
   case Expr::Add: {
     const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
-    unsigned width = be->left.getWidth();
+    unsigned width = be->left->getWidth();
     return evaluate(be->left).add(evaluate(be->right), width);
   }
   case Expr::Sub: {
     const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
-    unsigned width = be->left.getWidth();
+    unsigned width = be->left->getWidth();
     return evaluate(be->left).sub(evaluate(be->right), width);
   }
   case Expr::Mul: {
     const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
-    unsigned width = be->left.getWidth();
+    unsigned width = be->left->getWidth();
     return evaluate(be->left).mul(evaluate(be->right), width);
   }
   case Expr::UDiv: {
     const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
-    unsigned width = be->left.getWidth();
+    unsigned width = be->left->getWidth();
     return evaluate(be->left).udiv(evaluate(be->right), width);
   }
   case Expr::SDiv: {
     const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
-    unsigned width = be->left.getWidth();
+    unsigned width = be->left->getWidth();
     return evaluate(be->left).sdiv(evaluate(be->right), width);
   }
   case Expr::URem: {
     const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
-    unsigned width = be->left.getWidth();
+    unsigned width = be->left->getWidth();
     return evaluate(be->left).urem(evaluate(be->right), width);
   }
   case Expr::SRem: {
     const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
-    unsigned width = be->left.getWidth();
+    unsigned width = be->left->getWidth();
     return evaluate(be->left).srem(evaluate(be->right), width);
   }
 
@@ -181,19 +181,19 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
   }
   case Expr::Shl: {
     //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
-    //    unsigned width = be->left.getWidth();
+    //    unsigned width = be->left->getWidth();
     //    return evaluate(be->left).shl(evaluate(be->right), width);
     break;
   }
   case Expr::LShr: {
     //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
-    //    unsigned width = be->left.getWidth();
+    //    unsigned width = be->left->getWidth();
     //    return evaluate(be->left).lshr(evaluate(be->right), width);
     break;
   }
   case Expr::AShr: {
     //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
-    //    unsigned width = be->left.getWidth();
+    //    unsigned width = be->left->getWidth();
     //    return evaluate(be->left).ashr(evaluate(be->right), width);
     break;
   }
@@ -241,7 +241,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
     T left = evaluate(be->left);
     T right = evaluate(be->right);
-    unsigned bits = be->left.getWidth();
+    unsigned bits = be->left->getWidth();
 
     if (left.maxSigned(bits) < right.minSigned(bits)) {
       return T(1);
@@ -254,7 +254,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
     T left = evaluate(be->left);
     T right = evaluate(be->right);
-    unsigned bits = be->left.getWidth();
+    unsigned bits = be->left->getWidth();
       
     if (left.maxSigned(bits) <= right.minSigned(bits)) {
       return T(1);
@@ -275,7 +275,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     break;
   }
 
-  return T(0, bits64::maxValueOfNBits(e.getWidth()));
+  return T(0, bits64::maxValueOfNBits(e->getWidth()));
 }
 
 }
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index 5e6aab4b..e2421bb0 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -15,10 +15,6 @@
 class Expr;
 class ConstantExpr;
 
-class ExprVisitor;
-class StackFrame;
-class ObjectState;
-
 template<class T>
 class ref {
   T *ptr;
@@ -77,37 +73,6 @@ public:
     return ptr && ptr->getKind() == Expr::Constant;
   }
 
-  uint64_t getConstantValue() const {
-    assert(isConstant() && "Invalid call to getConstantValue()");
-    return ptr->getConstantValue();
-  }
-
-  unsigned hash() const {
-    assert(!isNull() && "Invalid call to hash()");
-    return ptr->hash();
-  }
-
-  unsigned computeHash() const {
-    assert(!isNull() && "Invalid call to computeHash()");
-    return ptr->computeHash();
-  }
-  
-  Expr::Width getWidth() const {
-    return ptr->getWidth();
-  }
-
-  Expr::Kind getKind() const {
-    return ptr->getKind();
-  }
-
-  unsigned getNumKids() const {
-    return ptr->getNumKids();
-  }
-
-  ref<Expr> getKid(unsigned k) {
-    return ptr->getKid(k);
-  }
-
   /* The copy assignment operator must also explicitly be defined,
    * despite a redundant template. */
   ref<T> &operator= (const ref<T> &r) {
@@ -126,6 +91,14 @@ public:
     return *this;
   }
 
+  T& operator*() const {
+    return *ptr;
+  }
+
+  T* operator->() const {
+    return ptr;
+  }
+
   bool isNull() const { return ptr == 0; }
 
   // assumes non-null arguments
@@ -143,11 +116,7 @@ public:
 
 template<class T>
 inline std::ostream &operator<<(std::ostream &os, const ref<T> &e) {
-  if (e.isConstant()) {
-    os << e.getConstantValue();
-  } else {
-    os << *e.get();
-  }
+  os << *e.get();
   return os;
 }