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

diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt
deleted file mode 100644
index f1212a876..000000000
--- a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt
+++ /dev/null
@@ -1,67 +0,0 @@
-(benchmark mathsat
-:logic QF_UFLIA
-:extrafuns ((fmt_length Int))
-:extrafuns ((fmt1 Int))
-:extrafuns ((x_count Int Int))
-:extrafuns ((select_format Int Int))
-:extrafuns ((percent Int))
-:extrafuns ((s_count Int Int))
-:status sat
-:formula
-(let (?n1 1)
-(let (?n2 5)
-(let (?n3 (x_count ?n2))
-(flet ($n4 (= ?n1 ?n3))
-(let (?n5 4)
-(let (?n6 (x_count ?n5))
-(flet ($n7 (= ?n1 ?n6))
-(let (?n8 3)
-(let (?n9 (x_count ?n8))
-(let (?n10 2)
-(let (?n11 (x_count ?n10))
-(flet ($n12 (= ?n9 ?n11))
-(let (?n13 0)
-(let (?n14 (select_format ?n8))
-(flet ($n15 (= ?n13 ?n14))
-(let (?n16 (x_count ?n13))
-(flet ($n17 (= ?n1 ?n16))
-(flet ($n18 (= ?n1 percent))
-(flet ($n19 true)
-(let (?n20 (s_count ?n13))
-(flet ($n21 (= ?n13 ?n20))
-(flet ($n22 (if_then_else $n18 $n19 $n21))
-(let (?n23 (select_format ?n10))
-(flet ($n24 (= percent ?n23))
-(flet ($n25 (= ?n1 ?n14))
-(flet ($n26 (and $n24 $n25))
-(flet ($n27 false)
-(flet ($n28 (if_then_else $n26 $n27 $n19))
-(flet ($n29 (and $n22 $n28))
-(flet ($n30 (and $n17 $n29))
-(flet ($n31 (= ?n13 percent))
-(flet ($n32 (= ?n13 ?n23))
-(flet ($n33 (and $n31 $n32))
-(let (?n34 (x_count ?n1))
-(flet ($n35 (= ?n13 ?n34))
-(flet ($n36 (= ?n16 ?n34))
-(flet ($n37 (if_then_else $n33 $n35 $n36))
-(flet ($n38 (and $n30 $n37))
-(flet ($n39 (and $n15 $n38))
-(flet ($n40 (and $n12 $n39))
-(flet ($n41 (and $n7 $n40))
-(flet ($n42 (and $n4 $n41))
-(let (?n43 9)
-(flet ($n44 (= ?n43 fmt_length))
-(let (?n45 (- fmt1 ?n10))
-(let (?n46 (x_count ?n45))
-(let (?n47 (+ ?n1 ?n46))
-(flet ($n48 (= ?n13 ?n47))
-(flet ($n49 (> fmt1 ?n1))
-(let (?n50 (- fmt_length ?n1))
-(flet ($n51 (< fmt1 ?n50))
-(flet ($n52 (and $n49 $n51))
-(flet ($n53 (and $n48 $n52))
-(flet ($n54 (and $n44 $n53))
-(flet ($n55 (and $n42 $n54))
-$n55
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))