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, 129 deletions

diff --git a/test/regress/regress0/bv/fuzz19.delta01.smt b/test/regress/regress0/bv/fuzz19.delta01.smt
deleted file mode 100644
index fd044074d..000000000
--- a/test/regress/regress0/bv/fuzz19.delta01.smt
+++ /dev/null
@@ -1,129 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_BV
-:extrafuns ((v0 BitVec[4]))
-:extrafuns ((v1 BitVec[4]))
-:extrafuns ((v2 BitVec[4]))
-:extrafuns ((v3 BitVec[4]))
-:extrafuns ((v4 BitVec[4]))
-:extrafuns ((v5 BitVec[4]))
-:status unsat
-:formula
-(flet ($n1 true)
-(let (?n2 (extract[0:0] v2))
-(let (?n3 (zero_extend[1] ?n2))
-(let (?n4 (zero_extend[2] ?n3))
-(let (?n5 bv0[4])
-(flet ($n6 (distinct ?n5 v4))
-(let (?n7 bv1[1])
-(let (?n8 bv0[1])
-(let (?n9 (ite $n6 ?n7 ?n8))
-(let (?n10 (sign_extend[3] ?n9))
-(let (?n11 (bvadd ?n4 ?n10))
-(flet ($n12 (bvsle ?n11 ?n5))
-(let (?n13 (ite $n12 ?n7 ?n8))
-(let (?n14 (sign_extend[3] ?n13))
-(let (?n15 bv11[4])
-(flet ($n16 (bvsge ?n15 v5))
-(let (?n17 (ite $n16 ?n7 ?n8))
-(let (?n18 (zero_extend[3] ?n17))
-(flet ($n19 (bvult ?n14 ?n18))
-(let (?n20 (ite $n19 ?n7 ?n8))
-(flet ($n21 (bvsge v2 ?n15))
-(let (?n22 (ite $n21 ?n7 ?n8))
-(let (?n23 (sign_extend[3] ?n22))
-(let (?n24 (bvlshr v4 ?n23))
-(let (?n25 (bvmul v5 ?n24))
-(flet ($n26 (bvslt ?n25 v2))
-(let (?n27 (ite $n26 ?n7 ?n8))
-(flet ($n28 (bvsge ?n20 ?n27))
-(let (?n29 (ite $n28 ?n7 ?n8))
-(let (?n30 (zero_extend[3] ?n29))
-(flet ($n31 (bvugt v3 ?n30))
-(flet ($n32 (bvugt v0 ?n5))
-(let (?n33 (ite $n32 ?n7 ?n8))
-(let (?n34 (zero_extend[3] ?n33))
-(flet ($n35 (bvsge v1 ?n34))
-(let (?n36 (ite $n35 ?n7 ?n8))
-(let (?n37 (sign_extend[3] ?n36))
-(let (?n38 (bvashr v1 ?n37))
-(let (?n39 bv10[4])
-(flet ($n40 (bvult ?n38 ?n39))
-(flet ($n41 false)
-(let (?n42 (bvashr v3 ?n4))
-(let (?n43 bv1[4])
-(flet ($n44 (bvule ?n42 ?n43))
-(let (?n45 (ite $n44 ?n7 ?n8))
-(let (?n46 (zero_extend[3] ?n45))
-(flet ($n47 (bvsge ?n46 ?n38))
-(let (?n48 (ite $n47 ?n7 ?n8))
-(let (?n49 (sign_extend[1] ?n48))
-(let (?n50 bv0[2])
-(flet ($n51 (bvsge ?n49 ?n50))
-(let (?n52 (ite $n51 ?n7 ?n8))
-(flet ($n53 (= ?n27 ?n52))
-(let (?n54 (ite $n53 ?n7 ?n8))
-(flet ($n55 (bvult ?n25 v1))
-(let (?n56 (ite $n55 ?n7 ?n8))
-(let (?n57 (bvadd ?n7 ?n56))
-(let (?n58 (bvneg v4))
-(flet ($n59 (bvslt ?n58 ?n5))
-(let (?n60 (ite $n59 ?n7 ?n8))
-(let (?n61 (bvashr ?n57 ?n60))
-(let (?n62 (sign_extend[3] ?n61))
-(let (?n63 (sign_extend[3] ?n54))
-(flet ($n64 (bvugt ?n62 ?n63))
-(let (?n65 (ite $n64 ?n7 ?n8))
-(flet ($n66 (distinct ?n54 ?n65))
-(flet ($n67 (not $n66))
-(let (?n68 (sign_extend[3] ?n45))
-(let (?n69 (bvcomp v3 ?n68))
-(flet ($n70 (bvule ?n7 ?n69))
-(flet ($n71 (or $n41 $n67 $n70))
-(let (?n72 (sign_extend[3] ?n7))
-(flet ($n73 (bvsle ?n72 ?n58))
-(let (?n74 (sign_extend[3] ?n2))
-(flet ($n75 (distinct ?n5 ?n74))
-(let (?n76 (ite $n75 ?n7 ?n8))
-(let (?n77 (sign_extend[3] ?n76))
-(flet ($n78 (bvsle ?n25 ?n5))
-(let (?n79 (ite $n78 ?n7 ?n8))
-(let (?n80 (zero_extend[3] ?n79))
-(let (?n81 (bvxnor ?n11 ?n80))
-(flet ($n82 (bvsle ?n77 ?n81))
-(flet ($n83 (not $n82))
-(let (?n84 (extract[2:0] v3))
-(let (?n85 (concat ?n84 ?n52))
-(flet ($n86 (bvsle ?n85 ?n72))
-(flet ($n87 (bvuge ?n5 ?n10))
-(let (?n88 (ite $n87 ?n7 ?n8))
-(let (?n89 (zero_extend[3] ?n88))
-(let (?n90 (bvmul v4 ?n89))
-(flet ($n91 (bvsgt ?n90 ?n5))
-(let (?n92 (ite $n91 ?n7 ?n8))
-(let (?n93 (sign_extend[3] ?n92))
-(flet ($n94 (bvsgt ?n18 ?n5))
-(let (?n95 (ite $n94 ?n7 ?n8))
-(flet ($n96 (bvult v4 v4))
-(let (?n97 (ite $n96 ?n7 ?n8))
-(flet ($n98 (bvsge ?n95 ?n97))
-(let (?n99 (ite $n98 ?n7 ?n8))
-(let (?n100 (zero_extend[3] ?n99))
-(flet ($n101 (bvsge ?n93 ?n100))
-(let (?n102 (ite $n101 ?n7 ?n8))
-(flet ($n103 (bvsle ?n8 ?n102))
-(flet ($n104 (or $n41 $n86 $n103))
-(let (?n105 (zero_extend[3] ?n20))
-(flet ($n106 (bvuge ?n5 ?n105))
-(flet ($n107 (bvule ?n25 ?n5))
-(let (?n108 (ite $n107 ?n7 ?n8))
-(let (?n109 (sign_extend[2] ?n108))
-(flet ($n110 (= ?n2 ?n7))
-(let (?n111 (ite $n110 ?n25 ?n42))
-(flet ($n112 (bvsle ?n5 ?n111))
-(let (?n113 (ite $n112 ?n7 ?n8))
-(let (?n114 (extract[1:0] ?n38))
-(let (?n115 (concat ?n113 ?n114))
-(flet ($n116 (= ?n109 ?n115))
-(flet ($n117 (and $n31 $n40 $n71 $n73 $n83 $n104 $n106 $n116))
-$n117
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))