2 files changed, 29 insertions, 10 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 192be985..9851d122 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -354,6 +354,28 @@ public:
   }
   static bool classof(const ConstantExpr *) { return true; }
 
+  /* Utility Functions */
+
+  /// isZero - Is this a constant zero.
+  bool isZero() const { return getConstantValue() == 0; }
+  
+  /// isTrue - Is this the true expression.
+  bool isTrue() const { 
+    assert(getWidth() == Expr::Bool && "Invalid isTrue() call!");
+    return getConstantValue() == 1;
+  }
+
+  /// isFalse - Is this the false expression.
+  bool isFalse() const {
+    assert(getWidth() == Expr::Bool && "Invalid isTrue() call!");
+    return getConstantValue() == 0;
+  }
+
+  /// isAllOnes - Is this constant all ones.
+  bool isAllOnes() const {
+    return getConstantValue() == bits64::maxValueOfNBits(getWidth());
+  }
+
   /* Constant Operations */
 
   ref<ConstantExpr> Concat(const ref<ConstantExpr> &RHS);
@@ -936,21 +958,21 @@ COMPARISON_EXPR_CLASS(Sge)
 
 inline bool Expr::isZero() const {
   if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))
-    return CE->getConstantValue() == 0;
+    return CE->isZero();
   return false;
 }
   
 inline bool Expr::isTrue() const {
+  assert(getWidth() == Expr::Bool && "Invalid isTrue() call!");
   if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))
-    return (CE->getWidth() == Expr::Bool &&
-            CE->getConstantValue() == 1);
+    return CE->isTrue();
   return false;
 }
   
 inline bool Expr::isFalse() const {
+  assert(getWidth() == Expr::Bool && "Invalid isFalse() call!");
   if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))
-    return (CE->getWidth() == Expr::Bool &&
-            CE->getConstantValue() == 0);
+    return CE->isFalse();
   return false;
 }
 
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 458b8d8d..838d03bd 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -88,12 +88,9 @@ namespace klee {
   template<typename InputIterator>
   inline bool Assignment::satisfies(InputIterator begin, InputIterator end) {
     AssignmentEvaluator v(*this);
-    for (; begin!=end; ++begin) {
-      ref<Expr> res = v.visit(*begin);
-      ConstantExpr *CE = dyn_cast<ConstantExpr>(res);
-      if (!CE || !CE->getConstantValue())
+    for (; begin!=end; ++begin)
+      if (!v.visit(*begin)->isTrue())
         return false;
-    }
     return true;
   }
 }