Corrected reversed inputs and outputs in Messy benchmarks.

SemGuS-git · Mar 1, 2024 · 9d8a9ca · 9d8a9ca
1 parent 5d7bb28
commit 9d8a9ca
Show file tree

Hide file tree

Showing 309 changed files with 13,220 additions and 0 deletions.
diff --git a/benchmarks/messy/README.md b/benchmarks/messy/README.md
@@ -0,0 +1,3 @@
+# Messy Benchmarks
+
+There are 2 sorts of benchmarks in each category. The first, under "correct_input_output", are the synthesis queries one would expect from the filename. The second, under "inverted_input_output", are the same queries with inputs and outputs reversed (i.e., we take inputs as outputs and vice versa.)
diff --git a/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_ADD_01.sem b/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_ADD_01.sem
@@ -0,0 +1,36 @@
+(declare-term-types
+((E 0) (Start 0))
+((($IBVVary )
+($bvsub E E)
+($bvadd E E)
+($IBVVarx ))
+(($bv=x E))))
+
+
+(define-funs-rec
+((E.Sem ((E_term_0 E) (r__0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start.Sem ((Start_term_0 Start) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool))
+
+((match E_term_0
+  (($IBVVary (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 y))))
+(($bvsub E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvadd r__1 (bvneg r__2)))
+  (E.Sem E_term_1 r__1 x y)
+  (E.Sem E_term_2 r__2 x y))))
+(($bvadd E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvadd r__1 r__2))
+  (E.Sem E_term_1 r__1 x y)
+  (E.Sem E_term_2 r__2 x y))))
+($IBVVarx (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 x))))))
+(match Start_term_0
+  ((($bv=x E_term_1) (exists ((r__1 (_ BitVec 32))) (and (and (= x_r0 r__1)
+  (= y y_r0))
+  (E.Sem E_term_1 r__1 x y))))))))
+
+
+(synth-fun BVtest_ADD_01() Start)
+
+
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_ADD_01 #x00000003 y #x00000004 #x00000004)))
+
+(check-synth)
diff --git a/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_AND_01.sem b/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_AND_01.sem
@@ -0,0 +1,33 @@
+(declare-term-types
+((E 0) (Start 0))
+((($bvxor E E)
+($IBVVarx )
+($IBVVary ))
+(($bv=x E))))
+
+
+(define-funs-rec
+((E.Sem ((E_term_0 E) (r__0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start.Sem ((Start_term_0 Start) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool))
+
+((match E_term_0
+  ((($bvxor E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvor (bvand r__1 (bvnot r__2)) (bvand (bvnot r__1) r__2)))
+  (E.Sem E_term_1 r__1 x y)
+  (E.Sem E_term_2 r__2 x y))))
+($IBVVarx (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 x))))
+($IBVVary (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 y))))))
+(match Start_term_0
+  ((($bv=x E_term_1) (exists ((r__1 (_ BitVec 32))) (and (and (= x_r0 r__1)
+  (= y y_r0))
+  (E.Sem E_term_1 r__1 x y))))))))
+
+
+(synth-fun BVtest_AND_01() Start)
+
+
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_01 #x00000000 y #x00000009 #x00000006)))
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_01 #x00000024 y #x000000f7 #x0000002c)))
+
+(check-synth)
diff --git a/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_AND_02.sem b/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_AND_02.sem
@@ -0,0 +1,33 @@
+(declare-term-types
+((E 0) (Start 0))
+((($bvadd E E)
+($IBVVarx )
+($IBVVary ))
+(($bv=x E))))
+
+
+(define-funs-rec
+((E.Sem ((E_term_0 E) (r__0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start.Sem ((Start_term_0 Start) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool))
+
+((match E_term_0
+  ((($bvadd E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvadd r__1 r__2))
+  (E.Sem E_term_1 r__1 x y)
+  (E.Sem E_term_2 r__2 x y))))
+($IBVVarx (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 x))))
+($IBVVary (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 y))))))
+(match Start_term_0
+  ((($bv=x E_term_1) (exists ((r__1 (_ BitVec 32))) (and (and (= x_r0 r__1)
+  (= y y_r0))
+  (E.Sem E_term_1 r__1 x y))))))))
+
+
+(synth-fun BVtest_AND_02() Start)
+
+
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_02 #x00000000 y #x00000009 #x00000006)))
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_02 #x00000024 y #x000000f7 #x0000002c)))
+
+(check-synth)
diff --git a/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_AND_03.sem b/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_AND_03.sem
@@ -0,0 +1,36 @@
+(declare-term-types
+((E 0) (Start 0))
+((($IBVVarx )
+($bvneg E)
+($IBVVary )
+($bvor E E))
+(($bv=x E))))
+
+
+(define-funs-rec
+((E.Sem ((E_term_0 E) (r__0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start.Sem ((Start_term_0 Start) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool))
+
+((match E_term_0
+  (($IBVVarx (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 x))))
+(($bvneg E_term_1) (exists ((r__1 (_ BitVec 32))) (and (= r__0 (bvnot r__1))
+  (E.Sem E_term_1 r__1 x y))))
+($IBVVary (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 y))))
+(($bvor E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvor r__1 r__2))
+  (E.Sem E_term_1 r__1 x y)
+  (E.Sem E_term_2 r__2 x y))))))
+(match Start_term_0
+  ((($bv=x E_term_1) (exists ((r__1 (_ BitVec 32))) (and (and (= x_r0 r__1)
+  (= y y_r0))
+  (E.Sem E_term_1 r__1 x y))))))))
+
+
+(synth-fun BVtest_AND_03() Start)
+
+
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_03 #x00000000 y #x00000009 #x00000006)))
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_03 #x00000024 y #x000000f7 #x0000002c)))
+
+(check-synth)
diff --git a/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_MAX_01.sem b/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_MAX_01.sem
@@ -0,0 +1,43 @@
+(declare-term-types
+((E 0) (Start 0))
+((($IBVVarx )
+($bvadd E E)
+($IBVVary )
+($bvor E E)
+($bvand E E))
+(($bv=x E))))
+
+
+(define-funs-rec
+((E.Sem ((E_term_0 E) (r__0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start.Sem ((Start_term_0 Start) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool))
+
+((match E_term_0
+  (($IBVVarx (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 x))))
+(($bvadd E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvadd r__1 r__2))
+  (E.Sem E_term_1 r__1 x y)
+  (E.Sem E_term_2 r__2 x y))))
+($IBVVary (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 y))))
+(($bvor E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvor r__1 r__2))
+  (E.Sem E_term_1 r__1 x y)
+  (E.Sem E_term_2 r__2 x y))))
+(($bvand E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvand r__1 r__2))
+  (E.Sem E_term_1 r__1 x y)
+  (E.Sem E_term_2 r__2 x y))))))
+(match Start_term_0
+  ((($bv=x E_term_1) (exists ((r__1 (_ BitVec 32))) (and (and (= x_r0 r__1)
+  (= y y_r0))
+  (E.Sem E_term_1 r__1 x y))))))))
+
+
+(synth-fun BVtest_MAX_01() Start)
+
+
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x00000009 y #x00000009 #x00000006)))
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x000000f7 y #x0000002c #x000000f7)))
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x00000020 y #x00000020 #x00000011)))
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x0000008e y #x0000008e #x0000008e)))
+
+(check-synth)
diff --git a/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_NAND_01.sem b/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_NAND_01.sem
@@ -0,0 +1,36 @@
+(declare-term-types
+((E 0) (Start 0))
+((($IBVVarx )
+($IBVVary )
+($bvand E E)
+($bvneg E))
+(($bv=x E))))
+
+
+(define-funs-rec
+((E.Sem ((E_term_0 E) (r__0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start.Sem ((Start_term_0 Start) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool))
+
+((match E_term_0
+  (($IBVVarx (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 x))))
+($IBVVary (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 y))))
+(($bvand E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvand r__1 r__2))
+  (E.Sem E_term_1 r__1 x y)
+  (E.Sem E_term_2 r__2 x y))))
+(($bvneg E_term_1) (exists ((r__1 (_ BitVec 32))) (and (= r__0 (bvnot r__1))
+  (E.Sem E_term_1 r__1 x y))))))
+(match Start_term_0
+  ((($bv=x E_term_1) (exists ((r__1 (_ BitVec 32))) (and (and (= x_r0 r__1)
+  (= y y_r0))
+  (E.Sem E_term_1 r__1 x y))))))))
+
+
+(synth-fun BVtest_NAND_01() Start)
+
+
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_NAND_01 #x0000001f y #x00000009 #x00000006)))
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_NAND_01 #x000000d1 y #x000000f7 #x0000002c)))
+
+(check-synth)
diff --git a/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_PLUS_01.sem b/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_PLUS_01.sem
@@ -0,0 +1,33 @@
+(declare-term-types
+((E 0) (Start 0))
+((($bvand E E)
+($IBVVarx )
+($IBVVary ))
+(($bv=x E))))
+
+
+(define-funs-rec
+((E.Sem ((E_term_0 E) (r__0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start.Sem ((Start_term_0 Start) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool))
+
+((match E_term_0
+  ((($bvand E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvand r__1 r__2))
+  (E.Sem E_term_1 r__1 x y)
+  (E.Sem E_term_2 r__2 x y))))
+($IBVVarx (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 x))))
+($IBVVary (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 y))))))
+(match Start_term_0
+  ((($bv=x E_term_1) (exists ((r__1 (_ BitVec 32))) (and (and (= x_r0 r__1)
+  (= y y_r0))
+  (E.Sem E_term_1 r__1 x y))))))))
+
+
+(synth-fun BVtest_PLUS_01() Start)
+
+
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_PLUS_01 #x0000000f y #x00000009 #x00000006)))
+(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_PLUS_01 #x00000123 y #x000000f7 #x0000002c)))
+
+(check-synth)
diff --git a/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_Swap_XOR_01.sem b/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_Swap_XOR_01.sem
@@ -0,0 +1,44 @@
+(declare-term-types
+((E 0) (Start 0) (Start1 0) (V 0))
+((($bvxor V V))
+(($seq Start1 Start1))
+(($bv=x E)
+($bv=y E))
+(($IBVVary )
+($IBVVarx ))))
+
+
+(define-funs-rec
+((E.Sem ((E_term_0 E) (r__0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start.Sem ((Start_term_0 Start) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start1.Sem ((Start1_term_0 Start1) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(V.Sem ((V_term_0 V) (r__0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool))
+
+((match E_term_0
+  ((($bvxor V_term_1 V_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvor (bvand r__1 (bvnot r__2)) (bvand (bvnot r__1) r__2)))
+  (V.Sem V_term_1 r__1 x y)
+  (V.Sem V_term_2 r__2 x y))))))
+(match Start_term_0
+  ((($seq Start1_term_1 Start1_term_2) (exists ((x_r1 (_ BitVec 32)) (y_r1 (_ BitVec 32))) (and (Start1.Sem Start1_term_1 x_r1 y_r1 x y)
+  (Start1.Sem Start1_term_2 x_r0 y_r0 x_r1 y_r1))))))
+(match Start1_term_0
+  ((($bv=x E_term_1) (exists ((r__1 (_ BitVec 32))) (and (and (= x_r0 r__1)
+  (= y y_r0))
+  (E.Sem E_term_1 r__1 x y))))
+(($bv=y E_term_1) (exists ((r__1 (_ BitVec 32))) (and (and (= x x_r0)
+  (= y_r0 r__1))
+  (E.Sem E_term_1 r__1 x y))))))
+(match V_term_0
+  (($IBVVary (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 y))))
+($IBVVarx (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 x))))))))
+
+
+(synth-fun BVtest_Swap_XOR_01() Start)
+
+
+(constraint (Start.Sem BVtest_Swap_XOR_01 #x00000006 #x00000009 #x00000009 #x00000006))
+(constraint (Start.Sem BVtest_Swap_XOR_01 #x0000002c #x000000f7 #x000000f7 #x0000002c))
+
+(check-synth)
diff --git a/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_Swap_XOR_02.sem b/benchmarks/messy/basic_bv/correct_input_outputs/BVtest_Swap_XOR_02.sem
@@ -0,0 +1,46 @@
+SAME AS XOR_01
+
+(declare-term-types
+((E 0) (Start 0) (Start1 0) (V 0))
+((($bvxor V V))
+(($seq Start1 Start1))
+(($bv=x E)
+($bv=y E))
+(($IBVVary )
+($IBVVarx ))))
+
+
+(define-funs-rec
+((E.Sem ((E_term_0 E) (r__0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start.Sem ((Start_term_0 Start) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start1.Sem ((Start1_term_0 Start1) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(V.Sem ((V_term_0 V) (r__0 (_ BitVec 32)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool))
+
+((match E_term_0
+  ((($bvxor V_term_1 V_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32))) (and (= r__0 (bvor (bvand r__1 (bvnot r__2)) (bvand (bvnot r__1) r__2)))
+  (V.Sem V_term_1 r__1 x y)
+  (V.Sem V_term_2 r__2 x y))))))
+(match Start_term_0
+  ((($seq Start1_term_1 Start1_term_2) (exists ((x_r1 (_ BitVec 32)) (y_r1 (_ BitVec 32))) (and (Start1.Sem Start1_term_1 x_r1 y_r1 x y)
+  (Start1.Sem Start1_term_2 x_r0 y_r0 x_r1 y_r1))))))
+(match Start1_term_0
+  ((($bv=x E_term_1) (exists ((r__1 (_ BitVec 32))) (and (and (= x_r0 r__1)
+  (= y y_r0))
+  (E.Sem E_term_1 r__1 x y))))
+(($bv=y E_term_1) (exists ((r__1 (_ BitVec 32))) (and (and (= x x_r0)
+  (= y_r0 r__1))
+  (E.Sem E_term_1 r__1 x y))))))
+(match V_term_0
+  (($IBVVary (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 y))))
+($IBVVarx (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 x))))))))
+
+
+(synth-fun BVtest_Swap_XOR_02() Start)
+
+
+(constraint (Start.Sem BVtest_Swap_XOR_02 #x00000006 #x00000009 #x00000009 #x00000006))
+(constraint (Start.Sem BVtest_Swap_XOR_02 #x0000002c #x000000f7 #x000000f7 #x0000002c))
+
+(check-synth)