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.

1 files changed, 0 insertions, 191 deletions

diff --git a/test/regress/regress0/bv/fuzz20.smt b/test/regress/regress0/bv/fuzz20.smt
deleted file mode 100644
index b7b493c82..000000000
--- a/test/regress/regress0/bv/fuzz20.smt
+++ /dev/null
@@ -1,191 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_BV
-:status unsat
-:extrafuns ((v0 BitVec[4]))
-:extrafuns ((v1 BitVec[4]))
-:extrafuns ((v2 BitVec[4]))
-:formula
-(let (?e3 bv2[4])
-(let (?e4 bv6[4])
-(let (?e5 bv8[4])
-(let (?e6 bv7[4])
-(let (?e7 bv3[4])
-(let (?e8 (bvmul v2 v2))
-(let (?e9 (bvnand ?e3 v0))
-(let (?e10 (bvnot v0))
-(let (?e11 (bvor ?e6 v1))
-(let (?e12 (zero_extend[0] v1))
-(let (?e13 (bvor v2 v0))
-(let (?e14 (bvlshr v2 ?e11))
-(let (?e15 (rotate_right[0] ?e8))
-(let (?e16 (ite (distinct ?e14 ?e15) bv1[1] bv0[1]))
-(let (?e17 (bvnor ?e11 (sign_extend[3] ?e16)))
-(let (?e18 (bvshl ?e3 ?e15))
-(let (?e19 (bvashr ?e9 ?e5))
-(let (?e20 (ite (bvule ?e3 ?e12) bv1[1] bv0[1]))
-(let (?e21 (bvnot ?e16))
-(let (?e22 (bvadd ?e8 ?e15))
-(let (?e23 (ite (bvsgt ?e12 ?e9) bv1[1] bv0[1]))
-(let (?e24 (zero_extend[0] v1))
-(let (?e25 (bvxor ?e14 v1))
-(let (?e26 (ite (bvsle ?e8 ?e25) bv1[1] bv0[1]))
-(let (?e27 (bvashr (sign_extend[3] ?e26) v0))
-(let (?e28 (rotate_right[1] ?e27))
-(let (?e29 (bvashr ?e22 ?e22))
-(let (?e30 (bvadd ?e3 ?e28))
-(let (?e31 (bvneg ?e27))
-(let (?e32 (ite (distinct ?e5 ?e5) bv1[1] bv0[1]))
-(let (?e33 (ite (bvslt (zero_extend[3] ?e16) ?e30) bv1[1] bv0[1]))
-(let (?e34 (rotate_left[0] ?e21))
-(let (?e35 (bvmul ?e9 ?e11))
-(let (?e36 (ite (distinct ?e18 ?e27) bv1[1] bv0[1]))
-(let (?e37 (bvand (zero_extend[3] ?e20) v0))
-(let (?e38 (rotate_left[1] ?e8))
-(let (?e39 (repeat[1] ?e22))
-(let (?e40 (ite (distinct ?e5 ?e17) bv1[1] bv0[1]))
-(let (?e41 (bvxnor (sign_extend[3] ?e40) v0))
-(let (?e42 (bvor v0 ?e7))
-(let (?e43 (ite (bvsgt ?e24 ?e15) bv1[1] bv0[1]))
-(let (?e44 (bvnot ?e33))
-(let (?e45 (bvsub ?e24 ?e11))
-(let (?e46 (bvsub ?e26 ?e44))
-(let (?e47 (bvneg ?e29))
-(let (?e48 (ite (bvsgt ?e37 ?e7) bv1[1] bv0[1]))
-(let (?e49 (bvlshr ?e29 ?e14))
-(let (?e50 (ite (bvsgt ?e18 ?e4) bv1[1] bv0[1]))
-(flet ($e51 (bvsle ?e20 ?e21))
-(flet ($e52 (bvsle ?e3 ?e41))
-(flet ($e53 (bvult ?e39 ?e39))
-(flet ($e54 (bvsgt (sign_extend[3] ?e32) ?e35))
-(flet ($e55 (= (zero_extend[3] ?e20) ?e18))
-(flet ($e56 (bvugt ?e41 ?e6))
-(flet ($e57 (bvsge ?e41 ?e38))
-(flet ($e58 (bvugt ?e5 ?e25))
-(flet ($e59 (bvult ?e12 ?e30))
-(flet ($e60 (bvslt ?e11 ?e8))
-(flet ($e61 (bvugt ?e35 ?e15))
-(flet ($e62 (bvugt ?e47 ?e17))
-(flet ($e63 (= ?e17 (zero_extend[3] ?e33)))
-(flet ($e64 (bvsge (sign_extend[3] ?e43) v0))
-(flet ($e65 (bvugt ?e6 ?e5))
-(flet ($e66 (bvugt (sign_extend[3] ?e43) ?e30))
-(flet ($e67 (bvsgt (sign_extend[3] ?e34) ?e22))
-(flet ($e68 (= ?e13 ?e12))
-(flet ($e69 (bvslt ?e45 ?e4))
-(flet ($e70 (distinct ?e19 (sign_extend[3] ?e50)))
-(flet ($e71 (distinct ?e47 v0))
-(flet ($e72 (bvsgt ?e8 (sign_extend[3] ?e36)))
-(flet ($e73 (bvule ?e25 ?e8))
-(flet ($e74 (bvsgt ?e10 ?e3))
-(flet ($e75 (distinct ?e31 ?e10))
-(flet ($e76 (= ?e29 ?e8))
-(flet ($e77 (= v0 (zero_extend[3] ?e21)))
-(flet ($e78 (bvsgt ?e49 v1))
-(flet ($e79 (bvsgt ?e19 ?e35))
-(flet ($e80 (bvule ?e16 ?e21))
-(flet ($e81 (bvslt ?e14 ?e10))
-(flet ($e82 (distinct ?e35 ?e14))
-(flet ($e83 (= ?e25 ?e3))
-(flet ($e84 (distinct ?e29 (zero_extend[3] ?e20)))
-(flet ($e85 (bvult ?e22 (zero_extend[3] ?e23)))
-(flet ($e86 (bvugt ?e23 ?e16))
-(flet ($e87 (bvult (sign_extend[3] ?e34) ?e35))
-(flet ($e88 (bvule ?e29 (zero_extend[3] ?e46)))
-(flet ($e89 (bvsgt ?e13 (sign_extend[3] ?e32)))
-(flet ($e90 (bvugt ?e42 ?e31))
-(flet ($e91 (bvuge ?e47 (zero_extend[3] ?e34)))
-(flet ($e92 (distinct ?e42 ?e28))
-(flet ($e93 (= ?e44 ?e20))
-(flet ($e94 (bvsle ?e35 (zero_extend[3] ?e34)))
-(flet ($e95 (bvule ?e42 ?e12))
-(flet ($e96 (bvsgt (zero_extend[3] ?e23) v1))
-(flet ($e97 (bvule v2 (sign_extend[3] ?e16)))
-(flet ($e98 (bvuge (sign_extend[3] ?e43) ?e37))
-(flet ($e99 (bvult ?e28 ?e3))
-(flet ($e100 (bvugt ?e19 (zero_extend[3] ?e26)))
-(flet ($e101 (= ?e27 ?e7))
-(flet ($e102 (bvsge ?e18 ?e14))
-(flet ($e103 (bvsgt ?e31 ?e18))
-(flet ($e104 (= (zero_extend[3] ?e50) ?e9))
-(flet ($e105 (bvult ?e39 v0))
-(flet ($e106 (distinct ?e19 v1))
-(flet ($e107 (bvsle ?e4 ?e4))
-(flet ($e108 (= ?e26 ?e46))
-(flet ($e109 (bvsle ?e35 ?e3))
-(flet ($e110 (bvuge ?e10 ?e14))
-(flet ($e111 (distinct ?e5 (zero_extend[3] ?e44)))
-(flet ($e112 (bvule v1 ?e27))
-(flet ($e113 (bvugt ?e41 (zero_extend[3] ?e23)))
-(flet ($e114 (bvule (sign_extend[3] ?e33) ?e11))
-(flet ($e115 (bvugt ?e48 ?e34))
-(flet ($e116 (= ?e47 ?e45))
-(flet ($e117 (bvugt ?e12 v0))
-(flet ($e118 (bvslt ?e41 ?e5))
-(flet ($e119 (bvsge (sign_extend[3] ?e21) ?e38))
-(flet ($e120 (bvugt ?e42 ?e47))
-(flet ($e121 (bvslt ?e18 (zero_extend[3] ?e16)))
-(flet ($e122 (bvsge ?e4 ?e45))
-(flet ($e123 (bvslt ?e37 (sign_extend[3] ?e48)))
-(flet ($e124 (bvugt ?e28 (zero_extend[3] ?e21)))
-(flet ($e125 (bvuge ?e30 ?e19))
-(flet ($e126 (bvsgt ?e35 ?e22))
-(flet ($e127 (bvuge (zero_extend[3] ?e34) ?e13))
-(flet ($e128 (bvsgt ?e5 ?e3))
-(flet ($e129 (bvslt ?e24 (zero_extend[3] ?e44)))
-(flet ($e130 (bvule ?e48 ?e33))
-(flet ($e131 (distinct ?e10 (zero_extend[3] ?e50)))
-(flet ($e132 (bvsle (sign_extend[3] ?e32) ?e28))
-(flet ($e133 (bvugt ?e3 v1))
-(flet ($e134 (= (sign_extend[3] ?e33) ?e42))
-(flet ($e135 (distinct ?e21 ?e46))
-(flet ($e136 (bvsle ?e15 ?e41))
-(flet ($e137 (bvsle (sign_extend[3] ?e40) v2))
-(flet ($e138 
-(and
- (or (not $e65) (not $e121) $e55)
- (or $e98 $e77 (not $e80))
- (or (not $e135) $e133 $e66)
- (or (not $e74) (not $e104) (not $e66))
- (or (not $e120) (not $e65) $e125)
- (or (not $e117) $e132 $e129)
- (or $e76 (not $e106) (not $e55))
- (or $e128 (not $e79) $e83)
- (or $e80 (not $e96) (not $e107))
- (or (not $e72) $e70 (not $e79))
- (or $e114 $e118 (not $e94))
- (or $e54 (not $e128) $e78)
- (or $e79 $e79 $e126)
- (or $e116 $e69 (not $e52))
- (or $e111 $e99 $e62)
- (or $e108 (not $e126) $e131)
- (or $e71 $e96 (not $e121))
- (or (not $e70) (not $e60) $e89)
- (or (not $e57) $e128 (not $e73))
- (or (not $e118) (not $e59) (not $e81))
- (or $e112 (not $e102) $e91)
- (or (not $e66) (not $e74) (not $e63))
- (or $e134 (not $e111) (not $e134))
- (or (not $e126) (not $e70) $e137)
- (or $e76 $e124 $e74)
- (or (not $e108) $e96 $e65)
- (or $e122 (not $e92) $e59)
- (or (not $e107) (not $e136) (not $e123))
- (or (not $e76) (not $e53) (not $e118))
- (or (not $e105) (not $e121) $e85)
- (or (not $e99) $e102 $e106)
- (or (not $e61) $e121 $e90)
- (or (not $e53) (not $e77) (not $e54))
- (or (not $e72) $e76 (not $e114))
- (or (not $e104) $e101 (not $e105))
- (or $e128 (not $e129) $e84)
- (or (not $e95) (not $e128) (not $e130))
- (or (not $e90) $e129 $e133)
- (or $e131 $e72 (not $e82))
- (or $e128 (not $e113) (not $e120))
- (or (not $e80) (not $e87) (not $e59))
- (or $e57 $e123 $e118)
- (or (not $e109) $e73 $e81)
-))
-$e138
-)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-