3 files changed, 59 insertions, 124 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
diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index 0c8ce06e..098da6ea 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -854,142 +854,39 @@ namespace {
   typedef ConstantSpecializedExprBuilder<ConstantFoldingBuilder>
     ConstantFoldingExprBuilder;
 
-  class SimplifyingExprBuilder : public ExprBuilder {
-    ExprBuilder *Base;
-
+  class SimplifyingBuilder : public ChainedBuilder {
   public:
-    SimplifyingExprBuilder(ExprBuilder *_Base) : Base(_Base) {}
-    ~SimplifyingExprBuilder() {
-      delete Base;
-    }
-
-    virtual ref<Expr> Constant(uint64_t Value, Expr::Width W) {
-      return Base->Constant(Value, W);
-    }
-
-    virtual ref<Expr> NotOptimized(const ref<Expr> &Index) {
-      return Base->NotOptimized(Index);
-    }
-
-    virtual ref<Expr> Read(const UpdateList &Updates,
-                           const ref<Expr> &Index) {
-      return Base->Read(Updates, Index);
-    }
-
-    virtual ref<Expr> Select(const ref<Expr> &Cond,
-                             const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Select(Cond, LHS, RHS);
-    }
-
-    virtual ref<Expr> Concat(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Concat(LHS, RHS);
-    }
-
-    virtual ref<Expr> Extract(const ref<Expr> &LHS,
-                              unsigned Offset, Expr::Width W) {
-      return Base->Extract(LHS, Offset, W);
-    }
-
-    virtual ref<Expr> ZExt(const ref<Expr> &LHS, Expr::Width W) {
-      return Base->ZExt(LHS, W);
-    }
-
-    virtual ref<Expr> SExt(const ref<Expr> &LHS, Expr::Width W) {
-      return Base->SExt(LHS, W);
-    }
-
-    virtual ref<Expr> Add(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Add(LHS, RHS);
-    }
-
-    virtual ref<Expr> Sub(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Sub(LHS, RHS);
-    }
-
-    virtual ref<Expr> Mul(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Mul(LHS, RHS);
-    }
-
-    virtual ref<Expr> UDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->UDiv(LHS, RHS);
-    }
-
-    virtual ref<Expr> SDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->SDiv(LHS, RHS);
-    }
-
-    virtual ref<Expr> URem(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->URem(LHS, RHS);
-    }
-
-    virtual ref<Expr> SRem(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->SRem(LHS, RHS);
-    }
-
-    virtual ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->And(LHS, RHS);
-    }
-
-    virtual ref<Expr> Or(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Or(LHS, RHS);
-    }
-
-    virtual ref<Expr> Xor(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Xor(LHS, RHS);
-    }
-
-    virtual ref<Expr> Shl(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Shl(LHS, RHS);
-    }
-
-    virtual ref<Expr> LShr(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->LShr(LHS, RHS);
-    }
-
-    virtual ref<Expr> AShr(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->AShr(LHS, RHS);
-    }
-
-    virtual ref<Expr> Eq(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Eq(LHS, RHS);
-    }
-
-    virtual ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Ne(LHS, RHS);
-    }
-
-    virtual ref<Expr> Ult(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Ult(LHS, RHS);
-    }
-
-    virtual ref<Expr> Ule(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Ule(LHS, RHS);
-    }
-
-    virtual ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Ugt(LHS, RHS);
-    }
+    SimplifyingBuilder(ExprBuilder *Builder, ExprBuilder *Base)
+      : ChainedBuilder(Builder, Base) {}
 
-    virtual ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Uge(LHS, RHS);
+    ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) {
+      // X != Y ==> !(X == Y)
+      return Builder->Not(Builder->Eq(LHS, RHS));
     }
 
-    virtual ref<Expr> Slt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Slt(LHS, RHS);
+    ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
+      // X u> Y ==> Y u< X
+      return Builder->Ult(RHS, LHS);
     }
 
-    virtual ref<Expr> Sle(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Sle(LHS, RHS);
+    ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
+      // X u>= Y ==> Y u<= X
+      return Builder->Ule(RHS, LHS);
     }
 
-    virtual ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Sgt(LHS, RHS);
+    ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
+      // X s> Y ==> Y s< X
+      return Builder->Slt(RHS, LHS);
     }
 
-    virtual ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
-      return Base->Sge(LHS, RHS);
+    ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
+      // X s>= Y ==> Y s<= X
+      return Builder->Sle(RHS, LHS);
     }
   };
+
+  typedef ConstantSpecializedExprBuilder<SimplifyingBuilder>
+    SimplifyingExprBuilder;
 }
 
 ExprBuilder *klee::createDefaultExprBuilder() {
diff --git a/test/Expr/Parser/Simplify.pc b/test/Expr/Parser/Simplify.pc
new file mode 100644
index 00000000..cf6d90ab
--- /dev/null
+++ b/test/Expr/Parser/Simplify.pc
@@ -0,0 +1,28 @@
+# RUN: %kleaver --builder=simplify -print-ast %s > %t
+
+array a[64] : w32 -> w8 = symbolic
+
+# Check -- X u> Y ==> Y u< X
+# RUN: grep -A 2 \"# Query 1\" %t > %t2
+# RUN: grep \"(query .. false .(Ult (Read w8 1 a) (Read w8 0 a)).)\" %t2
+(query [] false [(Ugt (Read w8 0 a) (Read w8 1 a))])
+
+# Check -- X u>= Y ==> Y u<= X
+# RUN: grep -A 2 \"# Query 2\" %t > %t2
+# RUN: grep \"(query .. false .(Ule (Read w8 1 a) (Read w8 0 a)).)\" %t2
+(query [] false [(Uge (Read w8 0 a) (Read w8 1 a))])
+
+# Check -- X u> Y ==> Y u< X
+# RUN: grep -A 2 \"# Query 3\" %t > %t2
+# RUN: grep \"(query .. false .(Slt (Read w8 1 a) (Read w8 0 a)).)\" %t2
+(query [] false [(Sgt (Read w8 0 a) (Read w8 1 a))])
+
+# Check -- X u>= Y ==> Y u<= X
+# RUN: grep -A 2 \"# Query 4\" %t > %t2
+# RUN: grep \"(query .. false .(Sle (Read w8 1 a) (Read w8 0 a)).)\" %t2
+(query [] false [(Sge (Read w8 0 a) (Read w8 1 a))])
+
+# Check -- X != Y ==> !(X == Y)
+# RUN: grep -A 2 \"# Query 5\" %t > %t2
+# RUN: grep \"(query .. false .(Not (Eq (Read w8 0 a) (Read w8 1 a))).)\" %t2
+(query [] false [(Ne (Read w8 0 a) (Read w8 1 a))])