1 files changed, 40 insertions, 0 deletions
diff --git a/test/Expr/Parser/Simplify.kquery b/test/Expr/Parser/Simplify.kquery
new file mode 100644
index 00000000..6d817b6f
--- /dev/null
+++ b/test/Expr/Parser/Simplify.kquery
@@ -0,0 +1,40 @@
+# 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))])
+
+# Check -- !(X or Y) ==> !X and !Y
+# RUN: grep -A 3 "# Query 6$" %t > %t2
+# RUN: grep "(query .. false .(And (Not (Eq 0 (Read w8 0 a)))" %t2
+# RUN: grep                       "(Not (Eq 1 (Read w8 1 a))))" %t2
+(query [] false [(Not (Or (Eq 0 (Read w8 0 a))
+                          (Eq 1 (Read w8 1 a))))])
+
+# Check -- false == X ==> !X
+# RUN: grep -A 2 "# Query 7" %t > %t2
+# RUN: grep "(query .. false .(Not (Extract 1 (Read w8 0 a))).)" %t2
+(query [] false [(Eq (Extract w1 1 (Read w8 0 a)) false)])