Added support for bitwise not. Replacing "false == " with Not in

the canonical form.



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

1 files changed, 16 insertions, 0 deletions

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 2f9e04a0..763a4be1 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -122,6 +122,7 @@ void Expr::printKind(std::ostream &os, Kind k) {
     X(SDiv);
     X(URem);
     X(SRem);
+    X(Not);
     X(And);
     X(Or);
     X(Xor);
@@ -188,6 +189,11 @@ unsigned ReadExpr::computeHash() {
   return hashValue;
 }
 
+unsigned NotExpr::computeHash() {
+  unsigned hashValue = expr->hash() * Expr::MAGIC_HASH_CONSTANT * Expr::Not;
+  return hashValue;
+}
+
 ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) {
   unsigned numArgs = args.size();
   (void) numArgs;
@@ -621,6 +627,16 @@ ref<Expr> ExtractExpr::create(ref<Expr> expr, unsigned off, Width w) {
 
 /***/
 
+ref<Expr> NotExpr::create(const ref<Expr> &e) {
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
+    return CE->Not();
+  
+  return NotExpr::alloc(e);
+}
+
+
+/***/
+
 ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
   unsigned kBits = e->getWidth();
   if (w == kBits) {