From 91a5055015a97935d19b3dbf18062e189268a1f9 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Fri, 6 Sep 2019 15:28:07 -0700
Subject: Remove SMT1 parser. (#3228)

This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).

Fixes #2948 and fixes #1313.
---
 test/regress/regress0/decision/wchains010ue.smt | 224 ------------------------
 1 file changed, 224 deletions(-)
 delete mode 100644 test/regress/regress0/decision/wchains010ue.smt

(limited to 'test/regress/regress0/decision/wchains010ue.smt')

diff --git a/test/regress/regress0/decision/wchains010ue.smt b/test/regress/regress0/decision/wchains010ue.smt
deleted file mode 100644
index ad47c6260..000000000
--- a/test/regress/regress0/decision/wchains010ue.smt
+++ /dev/null
@@ -1,224 +0,0 @@
-; COMMAND-LINE: --decision=justification
-; EXPECT: unsat
-
-(benchmark wchains010ue.smt
-:source {
-This benchmark generates write chain permutations and tries to show
-via extensionality that they are equal.
-
-Contributed by Armin Biere (armin.biere@jku.at).
-}
-:status unsat
-:category { crafted }
-:logic QF_AUFBV
-:difficulty { 2 }
-:extrafuns ((a1 Array[32:8]))
-:extrafuns ((v6 BitVec[32]))
-:extrafuns ((v7 BitVec[32]))
-:extrafuns ((v8 BitVec[32]))
-:extrafuns ((v9 BitVec[32]))
-:extrafuns ((v10 BitVec[32]))
-:extrafuns ((v11 BitVec[32]))
-:extrafuns ((v12 BitVec[32]))
-:extrafuns ((v13 BitVec[32]))
-:extrafuns ((v14 BitVec[32]))
-:extrafuns ((v15 BitVec[32]))
-:formula
-(let (?e2 bv0[32])
-(let (?e3 bv1[32])
-(let (?e4 bv2[32])
-(let (?e5 bv3[32])
-(let (?e16 (bvadd ?e2 v6))
-(let (?e17 (extract[7:0] v6))
-(let (?e18 (store a1 ?e16 ?e17))
-(let (?e19 (bvadd ?e3 v6))
-(let (?e20 (extract[15:8] v6))
-(let (?e21 (store ?e18 ?e19 ?e20))
-(let (?e22 (bvadd ?e4 v6))
-(let (?e23 (extract[23:16] v6))
-(let (?e24 (store ?e21 ?e22 ?e23))
-(let (?e25 (bvadd ?e5 v6))
-(let (?e26 (extract[31:24] v6))
-(let (?e27 (store ?e24 ?e25 ?e26))
-(let (?e28 (bvadd ?e2 v7))
-(let (?e29 (extract[7:0] v7))
-(let (?e30 (store ?e27 ?e28 ?e29))
-(let (?e31 (bvadd ?e3 v7))
-(let (?e32 (extract[15:8] v7))
-(let (?e33 (store ?e30 ?e31 ?e32))
-(let (?e34 (bvadd ?e4 v7))
-(let (?e35 (extract[23:16] v7))
-(let (?e36 (store ?e33 ?e34 ?e35))
-(let (?e37 (bvadd ?e5 v7))
-(let (?e38 (extract[31:24] v7))
-(let (?e39 (store ?e36 ?e37 ?e38))
-(let (?e40 (bvadd ?e2 v8))
-(let (?e41 (extract[7:0] v8))
-(let (?e42 (store ?e39 ?e40 ?e41))
-(let (?e43 (bvadd ?e3 v8))
-(let (?e44 (extract[15:8] v8))
-(let (?e45 (store ?e42 ?e43 ?e44))
-(let (?e46 (bvadd ?e4 v8))
-(let (?e47 (extract[23:16] v8))
-(let (?e48 (store ?e45 ?e46 ?e47))
-(let (?e49 (bvadd ?e5 v8))
-(let (?e50 (extract[31:24] v8))
-(let (?e51 (store ?e48 ?e49 ?e50))
-(let (?e52 (bvadd ?e2 v9))
-(let (?e53 (extract[7:0] v9))
-(let (?e54 (store ?e51 ?e52 ?e53))
-(let (?e55 (bvadd ?e3 v9))
-(let (?e56 (extract[15:8] v9))
-(let (?e57 (store ?e54 ?e55 ?e56))
-(let (?e58 (bvadd ?e4 v9))
-(let (?e59 (extract[23:16] v9))
-(let (?e60 (store ?e57 ?e58 ?e59))
-(let (?e61 (bvadd ?e5 v9))
-(let (?e62 (extract[31:24] v9))
-(let (?e63 (store ?e60 ?e61 ?e62))
-(let (?e64 (bvadd ?e2 v10))
-(let (?e65 (extract[7:0] v10))
-(let (?e66 (store ?e63 ?e64 ?e65))
-(let (?e67 (bvadd ?e3 v10))
-(let (?e68 (extract[15:8] v10))
-(let (?e69 (store ?e66 ?e67 ?e68))
-(let (?e70 (bvadd ?e4 v10))
-(let (?e71 (extract[23:16] v10))
-(let (?e72 (store ?e69 ?e70 ?e71))
-(let (?e73 (bvadd ?e5 v10))
-(let (?e74 (extract[31:24] v10))
-(let (?e75 (store ?e72 ?e73 ?e74))
-(let (?e76 (bvadd ?e2 v11))
-(let (?e77 (extract[7:0] v11))
-(let (?e78 (store ?e75 ?e76 ?e77))
-(let (?e79 (bvadd ?e3 v11))
-(let (?e80 (extract[15:8] v11))
-(let (?e81 (store ?e78 ?e79 ?e80))
-(let (?e82 (bvadd ?e4 v11))
-(let (?e83 (extract[23:16] v11))
-(let (?e84 (store ?e81 ?e82 ?e83))
-(let (?e85 (bvadd ?e5 v11))
-(let (?e86 (extract[31:24] v11))
-(let (?e87 (store ?e84 ?e85 ?e86))
-(let (?e88 (bvadd ?e2 v12))
-(let (?e89 (extract[7:0] v12))
-(let (?e90 (store ?e87 ?e88 ?e89))
-(let (?e91 (bvadd ?e3 v12))
-(let (?e92 (extract[15:8] v12))
-(let (?e93 (store ?e90 ?e91 ?e92))
-(let (?e94 (bvadd ?e4 v12))
-(let (?e95 (extract[23:16] v12))
-(let (?e96 (store ?e93 ?e94 ?e95))
-(let (?e97 (bvadd ?e5 v12))
-(let (?e98 (extract[31:24] v12))
-(let (?e99 (store ?e96 ?e97 ?e98))
-(let (?e100 (bvadd ?e2 v13))
-(let (?e101 (extract[7:0] v13))
-(let (?e102 (store ?e99 ?e100 ?e101))
-(let (?e103 (bvadd ?e3 v13))
-(let (?e104 (extract[15:8] v13))
-(let (?e105 (store ?e102 ?e103 ?e104))
-(let (?e106 (bvadd ?e4 v13))
-(let (?e107 (extract[23:16] v13))
-(let (?e108 (store ?e105 ?e106 ?e107))
-(let (?e109 (bvadd ?e5 v13))
-(let (?e110 (extract[31:24] v13))
-(let (?e111 (store ?e108 ?e109 ?e110))
-(let (?e112 (bvadd ?e2 v14))
-(let (?e113 (extract[7:0] v14))
-(let (?e114 (store ?e111 ?e112 ?e113))
-(let (?e115 (bvadd ?e3 v14))
-(let (?e116 (extract[15:8] v14))
-(let (?e117 (store ?e114 ?e115 ?e116))
-(let (?e118 (bvadd ?e4 v14))
-(let (?e119 (extract[23:16] v14))
-(let (?e120 (store ?e117 ?e118 ?e119))
-(let (?e121 (bvadd ?e5 v14))
-(let (?e122 (extract[31:24] v14))
-(let (?e123 (store ?e120 ?e121 ?e122))
-(let (?e124 (bvadd ?e2 v15))
-(let (?e125 (extract[7:0] v15))
-(let (?e126 (store ?e123 ?e124 ?e125))
-(let (?e127 (bvadd ?e3 v15))
-(let (?e128 (extract[15:8] v15))
-(let (?e129 (store ?e126 ?e127 ?e128))
-(let (?e130 (bvadd ?e4 v15))
-(let (?e131 (extract[23:16] v15))
-(let (?e132 (store ?e129 ?e130 ?e131))
-(let (?e133 (bvadd ?e5 v15))
-(let (?e134 (extract[31:24] v15))
-(let (?e135 (store ?e132 ?e133 ?e134))
-(let (?e136 (store a1 ?e124 ?e125))
-(let (?e137 (store ?e136 ?e127 ?e128))
-(let (?e138 (store ?e137 ?e130 ?e131))
-(let (?e139 (store ?e138 ?e133 ?e134))
-(let (?e140 (store ?e139 ?e112 ?e113))
-(let (?e141 (store ?e140 ?e115 ?e116))
-(let (?e142 (store ?e141 ?e118 ?e119))
-(let (?e143 (store ?e142 ?e121 ?e122))
-(let (?e144 (store ?e143 ?e100 ?e101))
-(let (?e145 (store ?e144 ?e103 ?e104))
-(let (?e146 (store ?e145 ?e106 ?e107))
-(let (?e147 (store ?e146 ?e109 ?e110))
-(let (?e148 (store ?e147 ?e88 ?e89))
-(let (?e149 (store ?e148 ?e91 ?e92))
-(let (?e150 (store ?e149 ?e94 ?e95))
-(let (?e151 (store ?e150 ?e97 ?e98))
-(let (?e152 (store ?e151 ?e76 ?e77))
-(let (?e153 (store ?e152 ?e79 ?e80))
-(let (?e154 (store ?e153 ?e82 ?e83))
-(let (?e155 (store ?e154 ?e85 ?e86))
-(let (?e156 (store ?e155 ?e64 ?e65))
-(let (?e157 (store ?e156 ?e67 ?e68))
-(let (?e158 (store ?e157 ?e70 ?e71))
-(let (?e159 (store ?e158 ?e73 ?e74))
-(let (?e160 (store ?e159 ?e52 ?e53))
-(let (?e161 (store ?e160 ?e55 ?e56))
-(let (?e162 (store ?e161 ?e58 ?e59))
-(let (?e163 (store ?e162 ?e61 ?e62))
-(let (?e164 (store ?e163 ?e40 ?e41))
-(let (?e165 (store ?e164 ?e43 ?e44))
-(let (?e166 (store ?e165 ?e46 ?e47))
-(let (?e167 (store ?e166 ?e49 ?e50))
-(let (?e168 (store ?e167 ?e28 ?e29))
-(let (?e169 (store ?e168 ?e31 ?e32))
-(let (?e170 (store ?e169 ?e34 ?e35))
-(let (?e171 (store ?e170 ?e37 ?e38))
-(let (?e172 (store ?e171 ?e16 ?e17))
-(let (?e173 (store ?e172 ?e19 ?e20))
-(let (?e174 (store ?e173 ?e22 ?e23))
-(let (?e175 (store ?e174 ?e25 ?e26))
-(let (?e176 (ite (= ?e135 ?e175) bv1[1] bv0[1]))
-(let (?e177 (extract[1:0] v6))
-(let (?e178 bv0[2])
-(let (?e179 (ite (= ?e177 ?e178) bv1[1] bv0[1]))
-(let (?e180 (bvand (bvnot ?e176) ?e179))
-(let (?e181 (extract[1:0] v7))
-(let (?e182 (ite (= ?e178 ?e181) bv1[1] bv0[1]))
-(let (?e183 (bvand ?e180 ?e182))
-(let (?e184 (extract[1:0] v8))
-(let (?e185 (ite (= ?e178 ?e184) bv1[1] bv0[1]))
-(let (?e186 (bvand ?e183 ?e185))
-(let (?e187 (extract[1:0] v9))
-(let (?e188 (ite (= ?e178 ?e187) bv1[1] bv0[1]))
-(let (?e189 (bvand ?e186 ?e188))
-(let (?e190 (extract[1:0] v10))
-(let (?e191 (ite (= ?e178 ?e190) bv1[1] bv0[1]))
-(let (?e192 (bvand ?e189 ?e191))
-(let (?e193 (extract[1:0] v11))
-(let (?e194 (ite (= ?e178 ?e193) bv1[1] bv0[1]))
-(let (?e195 (bvand ?e192 ?e194))
-(let (?e196 (extract[1:0] v12))
-(let (?e197 (ite (= ?e178 ?e196) bv1[1] bv0[1]))
-(let (?e198 (bvand ?e195 ?e197))
-(let (?e199 (extract[1:0] v13))
-(let (?e200 (ite (= ?e178 ?e199) bv1[1] bv0[1]))
-(let (?e201 (bvand ?e198 ?e200))
-(let (?e202 (extract[1:0] v14))
-(let (?e203 (ite (= ?e178 ?e202) bv1[1] bv0[1]))
-(let (?e204 (bvand ?e201 ?e203))
-(let (?e205 (extract[1:0] v15))
-(let (?e206 (ite (= ?e178 ?e205) bv1[1] bv0[1]))
-(let (?e207 (bvand ?e204 ?e206))
-(not (= ?e207 bv0[1]))
-)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-- 
cgit v1.2.3