From 03eca4ba3255665bd4b2e246b92f63cc2b06a1bf Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Tue, 16 Jun 2009 02:26:40 +0000
Subject: 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
---
 include/klee/ExprBuilder.h | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'include')

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
-- 
cgit 1.4.1