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, 9 insertions, 0 deletions

diff --git a/test/regress/regress0/bv/fuzz37.smtv1.smt2 b/test/regress/regress0/bv/fuzz37.smtv1.smt2
new file mode 100644
index 000000000..2e79f86ce
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz37.smtv1.smt2
@@ -0,0 +1,9 @@
+(set-option :incremental false)
+(set-info :status sat)
+(set-logic QF_BV)
+(declare-fun v0 () (_ BitVec 4))
+(declare-fun v1 () (_ BitVec 4))
+(declare-fun v2 () (_ BitVec 4))
+(declare-fun v3 () (_ BitVec 4))
+(declare-fun v4 () (_ BitVec 4))
+(check-sat-assuming ( (let ((_let_0 (bvsub v0 (_ bv2 4)))) (let ((_let_1 (bvnor (_ bv2 4) ((_ zero_extend 3) (ite (bvugt (_ bv2 4) v1) (_ bv1 1) (_ bv0 1)))))) (let ((_let_2 (bvnor v1 _let_0))) (let ((_let_3 ((_ zero_extend 0) (bvmul _let_1 v1)))) (let ((_let_4 (bvsub v3 _let_3))) (let ((_let_5 (bvshl v4 (bvnot v4)))) (let ((_let_6 (concat (ite (bvult v0 _let_0) (_ bv1 1) (_ bv0 1)) (ite (bvult v0 _let_0) (_ bv1 1) (_ bv0 1))))) (let ((_let_7 ((_ rotate_left 0) v1))) (let ((_let_8 (bvlshr _let_4 ((_ zero_extend 3) (ite (bvugt (_ bv2 4) v1) (_ bv1 1) (_ bv0 1)))))) (let ((_let_9 ((_ zero_extend 3) (ite (= (bvnot v4) v3) (_ bv1 1) (_ bv0 1))))) (let ((_let_10 (distinct (bvashr (bvor v3 v1) (_ bv2 4)) _let_2))) (let ((_let_11 (= _let_4 _let_3))) (let ((_let_12 ((_ sign_extend 3) (bvcomp _let_2 _let_0)))) (let ((_let_13 (bvugt v3 v1))) (let ((_let_14 ((_ sign_extend 3) (ite (bvule (bvnot v4) ((_ sign_extend 3) (ite (= (bvnot v4) v3) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))))) (let ((_let_15 (distinct (bvnot v4) (bvashr (bvor v3 v1) (_ bv2 4))))) (let ((_let_16 (bvuge ((_ zero_extend 3) (ite (bvugt (_ bv2 4) v1) (_ bv1 1) (_ bv0 1))) _let_4))) (let ((_let_17 (bvslt v1 (bvnor _let_7 (bvlshr v4 v3))))) (let ((_let_18 (bvsgt v3 (bvor v3 v1)))) (let ((_let_19 (= v2 ((_ zero_extend 3) (ite (bvule (bvnot v4) ((_ sign_extend 3) (ite (= (bvnot v4) v3) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))))) (let ((_let_20 (bvsge _let_9 _let_8))) (let ((_let_21 (distinct ((_ zero_extend 3) (bvcomp (bvnot v4) v2)) (bvnot v4)))) (let ((_let_22 ((_ zero_extend 2) _let_6))) (let ((_let_23 (bvule (bvshl _let_5 v1) (bvlshr v4 v3)))) (let ((_let_24 (distinct ((_ zero_extend 3) (bvcomp (bvnot v4) v2)) (_ bv2 4)))) (let ((_let_25 (distinct ((_ sign_extend 3) (ite (= (bvnot v4) v3) (_ bv1 1) (_ bv0 1))) (bvashr (bvor v3 v1) (_ bv2 4))))) (let ((_let_26 (bvule (bvand _let_0 v0) _let_4))) (let ((_let_27 (bvule _let_5 v2))) (let ((_let_28 (not (bvslt _let_4 _let_7)))) (let ((_let_29 (not _let_19))) (let ((_let_30 (not _let_27))) (let ((_let_31 (not (bvule ((_ sign_extend 3) (ite (bvult v0 _let_0) (_ bv1 1) (_ bv0 1))) v2)))) (let ((_let_32 (not (bvsge (bvshl _let_5 v1) _let_5)))) (let ((_let_33 (not _let_25))) (let ((_let_34 (not _let_20))) (let ((_let_35 (not (bvugt _let_7 _let_9)))) (let ((_let_36 (not _let_11))) (let ((_let_37 (not (bvsle _let_4 (bvmul _let_1 v1))))) (let ((_let_38 (not (bvule (ite (= (bvnot v4) v3) (_ bv1 1) (_ bv0 1)) (ite (bvule (bvnot v4) ((_ sign_extend 3) (ite (= (bvnot v4) v3) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))))) (and (or _let_10 _let_27 _let_28) (or _let_28 _let_23 (bvule (ite (= (bvnot v4) v3) (_ bv1 1) (_ bv0 1)) (ite (bvule (bvnot v4) ((_ sign_extend 3) (ite (= (bvnot v4) v3) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (or _let_29 (not (bvsgt _let_2 v3)) _let_18) (or (bvuge _let_9 v2) (bvsle _let_4 (bvmul _let_1 v1)) _let_25) (or _let_13 _let_21 _let_30) (or (bvuge _let_7 _let_2) _let_30 (not _let_23)) (or (bvsgt v0 _let_22) _let_31 (bvult (bvnot v4) (bvand _let_0 v0))) (or (not _let_17) _let_32 (bvuge ((_ zero_extend 3) (bvcomp _let_2 _let_0)) _let_5)) (or _let_33 _let_34 _let_31) (or (bvule (ite (= (bvnot v4) v3) (_ bv1 1) (_ bv0 1)) (ite (bvule (bvnot v4) ((_ sign_extend 3) (ite (= (bvnot v4) v3) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))) (not (bvuge (bvand _let_0 v0) _let_12)) _let_35) (or (not _let_10) (not (bvule (bvcomp (bvnot v4) v2) (ite (bvule (bvnot v4) ((_ sign_extend 3) (ite (= (bvnot v4) v3) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) _let_32) (or (bvsle _let_22 (bvand _let_0 v0)) _let_21 _let_31) (or _let_24 _let_29 _let_15) (or _let_16 _let_28 _let_25) (or _let_34 _let_36 _let_19) (or (not (bvugt (bvashr (bvor v3 v1) (_ bv2 4)) _let_1)) (not (bvsle _let_14 (_ bv2 4))) _let_26) (or _let_27 _let_15 (not _let_16)) (or _let_13 (not (bvuge _let_9 _let_1)) _let_18) (or (not (bvsgt v1 (bvashr (bvor v3 v1) (_ bv2 4)))) (not (bvuge _let_0 v4)) _let_24) (or _let_36 _let_35 _let_37) (or (bvslt (_ bv2 4) _let_8) (not (bvsge _let_5 (_ bv2 4))) _let_24) (or (bvugt _let_7 _let_14) _let_11 _let_37) (or _let_38 (not (bvult ((_ zero_extend 3) (ite (bvugt (_ bv2 4) v1) (_ bv1 1) (_ bv0 1))) v4)) (not _let_15)) (or _let_20 (bvult v1 ((_ sign_extend 2) _let_6)) (not (bvslt v1 (bvmul _let_1 v1)))) (or _let_11 _let_38 _let_25) (or _let_17 (bvule v1 _let_12) (not _let_13)) (or _let_26 _let_33 (not (bvult _let_2 _let_1))))))))))))))))))))))))))))))))))))))))))) ))