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

diff --git a/test/regress/regress0/bv/fuzz15.delta01.smt b/test/regress/regress0/bv/fuzz15.delta01.smt
deleted file mode 100644
index b3fad3a2b..000000000
--- a/test/regress/regress0/bv/fuzz15.delta01.smt
+++ /dev/null
@@ -1,107 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_BV
-:extrafuns ((v11 BitVec[8]))
-:extrafuns ((v12 BitVec[8]))
-:extrafuns ((v10 BitVec[12]))
-:extrafuns ((v2 BitVec[10]))
-:extrafuns ((v8 BitVec[11]))
-:extrafuns ((v17 BitVec[8]))
-:extrafuns ((v5 BitVec[13]))
-:extrafuns ((v0 BitVec[15]))
-:extrafuns ((v14 BitVec[14]))
-:extrafuns ((v19 BitVec[10]))
-:status unsat
-:formula
-(let (?n1 (sign_extend[2] v11))
-(let (?n2 (sign_extend[6] ?n1))
-(let (?n3 (zero_extend[2] v14))
-(flet ($n4 (bvult ?n2 ?n3))
-(flet ($n5 (not $n4))
-(let (?n6 bv0[12])
-(flet ($n7 (bvslt ?n6 v10))
-(let (?n8 bv1[1])
-(let (?n9 bv0[1])
-(let (?n10 (ite $n7 ?n8 ?n9))
-(let (?n11 (sign_extend[15] ?n10))
-(let (?n12 bv0[10])
-(flet ($n13 (bvslt ?n12 v19))
-(let (?n14 (ite $n13 ?n8 ?n9))
-(flet ($n15 (= ?n8 ?n14))
-(let (?n16 bv0[14])
-(let (?n17 (bvxnor v14 ?n16))
-(let (?n18 (extract[9:0] v0))
-(let (?n19 (sign_extend[4] ?n18))
-(let (?n20 bv6240[14])
-(let (?n21 (bvxnor ?n19 ?n20))
-(let (?n22 (ite $n15 ?n17 ?n21))
-(let (?n23 (zero_extend[2] ?n22))
-(let (?n24 (bvsub ?n11 ?n23))
-(let (?n25 bv0[16])
-(flet ($n26 (bvugt ?n24 ?n25))
-(flet ($n27 (not $n26))
-(flet ($n28 false)
-(let (?n29 (zero_extend[2] v8))
-(let (?n30 bv0[15])
-(flet ($n31 (bvsle v0 ?n30))
-(let (?n32 (ite $n31 ?n8 ?n9))
-(let (?n33 (zero_extend[12] ?n32))
-(let (?n34 (bvshl ?n29 ?n33))
-(flet ($n35 (bvsge ?n25 ?n3))
-(let (?n36 (ite $n35 ?n8 ?n9))
-(let (?n37 (zero_extend[12] ?n36))
-(flet ($n38 (bvugt ?n34 ?n37))
-(flet ($n39 (not $n38))
-(flet ($n40 (distinct ?n3 ?n25))
-(let (?n41 (ite $n40 ?n8 ?n9))
-(let (?n42 (sign_extend[14] ?n41))
-(flet ($n43 (bvsge ?n42 ?n30))
-(flet ($n44 (or $n28 $n39 $n43))
-(let (?n45 bv0[13])
-(let (?n46 (sign_extend[2] v17))
-(let (?n47 (zero_extend[3] ?n46))
-(flet ($n48 (distinct ?n45 ?n47))
-(let (?n49 (ite $n48 ?n8 ?n9))
-(let (?n50 (sign_extend[14] ?n49))
-(let (?n51 (bvnot ?n30))
-(flet ($n52 (bvult ?n50 ?n51))
-(let (?n53 (sign_extend[2] v14))
-(flet ($n54 (bvuge ?n25 ?n53))
-(flet ($n55 (not $n54))
-(flet ($n56 (or $n28 $n52 $n55))
-(let (?n57 (sign_extend[6] v12))
-(flet ($n58 (bvsgt ?n57 ?n21))
-(let (?n59 (ite $n58 ?n8 ?n9))
-(flet ($n60 (bvugt ?n8 ?n59))
-(let (?n61 (zero_extend[1] ?n29))
-(let (?n62 (bvmul ?n20 ?n61))
-(flet ($n63 (bvsgt ?n45 v5))
-(let (?n64 (ite $n63 ?n8 ?n9))
-(let (?n65 (zero_extend[13] ?n64))
-(flet ($n66 (bvule ?n62 ?n65))
-(flet ($n67 (not $n66))
-(let (?n68 (sign_extend[4] v2))
-(let (?n69 (bvxnor ?n16 ?n68))
-(let (?n70 (zero_extend[2] ?n46))
-(let (?n71 (zero_extend[2] ?n70))
-(flet ($n72 (= ?n69 ?n71))
-(let (?n73 (extract[6:3] ?n29))
-(let (?n74 (sign_extend[12] ?n73))
-(flet ($n75 (bvsle ?n25 ?n74))
-(let (?n76 (sign_extend[9] ?n10))
-(let (?n77 (bvxnor v2 ?n76))
-(let (?n78 (extract[3:3] ?n77))
-(flet ($n79 (= ?n8 ?n78))
-(let (?n80 (ite $n79 ?n16 ?n57))
-(flet ($n81 (bvugt ?n1 ?n12))
-(let (?n82 (ite $n81 ?n8 ?n9))
-(let (?n83 (bvnot ?n82))
-(let (?n84 (zero_extend[13] ?n83))
-(flet ($n85 (bvult ?n80 ?n84))
-(let (?n86 (ite $n85 ?n8 ?n9))
-(let (?n87 (zero_extend[12] ?n86))
-(let (?n88 (zero_extend[1] ?n87))
-(flet ($n89 (= ?n16 ?n88))
-(flet ($n90 (or $n28 $n75 $n89))
-(flet ($n91 (and $n5 $n27 $n44 $n56 $n60 $n67 $n72 $n90))
-$n91
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))