Start SimplifyingExprBuilder

 - Normalize Ne, Ugt, Uge, Slt, Sge


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73458 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 10 insertions, 0 deletions

diff --git a/include/klee/ExprBuilder.h b/include/klee/ExprBuilder.h
index 6c1f6809..18941876 100644
--- a/include/klee/ExprBuilder.h
+++ b/include/klee/ExprBuilder.h
@@ -57,6 +57,16 @@ namespace klee {
     virtual ref<Expr> Sle(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
     virtual ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
     virtual ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
+
+    // Utility functions
+
+    ref<Expr> False() { return ConstantExpr::alloc(0, Expr::Bool); }
+
+    ref<Expr> True() { return ConstantExpr::alloc(0, Expr::Bool); }
+
+    ref<Expr> Not(const ref<Expr> &LHS) {
+      return Eq(False(), LHS);
+    }
   };
 
   /// createDefaultExprBuilder - Create an expression builder which does no