Remove SMT-LIB 2.5 and 2.0 support. (#6068)

This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.

6 files changed, 28 insertions, 30 deletions

diff --git a/test/regress/regress1/strings/bug686dd.smt2 b/test/regress/regress1/strings/bug686dd.smt2
index b5c9457ff..1449a09be 100644
--- a/test/regress/regress1/strings/bug686dd.smt2
+++ b/test/regress/regress1/strings/bug686dd.smt2
@@ -1,14 +1,13 @@
-(set-info :smt-lib-version 2.5)
 (set-logic UFDTSLIA)
 (set-info :status sat)
 
-(declare-datatypes () ((T (TC (TCb String)))))
+(declare-datatype T ((TC (TCb String))))
 
 (declare-fun root5 () String)
 (declare-fun root6 () T)
 
 (assert (and 
-(str.in.re root5 ((_ re.loop 4 4) (re.range "0" "9")) )
-(str.in.re (TCb root6) ((_ re.loop 4 4) (re.range "0" "9")) )
+(str.in_re root5 ((_ re.loop 4 4) (re.range "0" "9")) )
+(str.in_re (TCb root6) ((_ re.loop 4 4) (re.range "0" "9")) )
 ) )
 (check-sat)
diff --git a/test/regress/regress1/strings/issue1105.smt2 b/test/regress/regress1/strings/issue1105.smt2
index bf5cb7669..59f618403 100644
--- a/test/regress/regress1/strings/issue1105.smt2
+++ b/test/regress/regress1/strings/issue1105.smt2
@@ -1,11 +1,10 @@
-(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)
-(declare-datatypes () ((Val
-    (Str (str String))
-    (Num (num Int)))))
+(declare-datatype Val
+    ((Str (str String))
+    (Num (num Int))))
 
 (declare-const var0 Val)
-(assert (=> (is-Str var0) (distinct (str.to.int (str var0)) (- 1))))
+(assert (=> (is-Str var0) (distinct (str.to_int (str var0)) (- 1))))
 (check-sat)
diff --git a/test/regress/regress1/strings/issue1684-regex.smt2 b/test/regress/regress1/strings/issue1684-regex.smt2
index de0739bd8..41fa27120 100644
--- a/test/regress/regress1/strings/issue1684-regex.smt2
+++ b/test/regress/regress1/strings/issue1684-regex.smt2
@@ -1,8 +1,8 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
 (declare-const s String)
-(assert (str.in.re s (re.* (re.range "\x00" "\xFF"))))
-(assert (str.in.re s (re.range "\x00" "\xFF")))
+(assert (str.in_re s (re.* (re.range "\u{0}" "\u{ff}"))))
+(assert (str.in_re s (re.range "\u{0}" "\u{ff}")))
 (check-sat)
diff --git a/test/regress/regress1/strings/issue3272.smt2 b/test/regress/regress1/strings/issue3272.smt2
index cf33afb92..622e294d8 100644
--- a/test/regress/regress1/strings/issue3272.smt2
+++ b/test/regress/regress1/strings/issue3272.smt2
@@ -1,4 +1,4 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
 (set-logic ALL_SUPPORTED)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -9,13 +9,13 @@
     (and              
         (and                                      
             (and                          
-                (not (= (ite (= (str.at (str.substr c 1 (- (str.len (str.substr c 0 (- (str.len c) 1))) 1)) (- (str.len (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1))) 1)) "\t") 1 0) 0))   
+                (not (= (ite (= (str.at (str.substr c 1 (- (str.len (str.substr c 0 (- (str.len c) 1))) 1)) (- (str.len (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1))) 1)) "\u{9}") 1 0) 0))   
                    
                 (= (ite (= (str.at (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1)) 0) "B") 1 0) 0)
             )     
                             
             (= (ite (= (str.at (str.substr (str.substr c 1 (- (str.len c) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1)) 0) " ") 1 0) 0)                   
-            (not (= (ite (= (str.at (str.substr (str.replace a b "") 1 (- (str.len c) 1)) (- (str.len (str.substr c 1 (- (str.len c) 1))) 1)) "\v") 1 0) 0))
+            (not (= (ite (= (str.at (str.substr (str.replace a b "") 1 (- (str.len c) 1)) (- (str.len (str.substr c 1 (- (str.len c) 1))) 1)) "\u{b}") 1 0) 0))
         )       
         (= (ite (= (str.at (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0) " ") 1 0) 0)
     )
diff --git a/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2 b/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
index b2bb29577..4879cb3fb 100644
--- a/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
+++ b/test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
@@ -10,10 +10,10 @@
 ; EXPECT: sat

 ; EXPECT: sat

 ; EXPECT: sat

-(set-info :smt-lib-version 2.5)

+(set-info :smt-lib-version 2.6)

 (set-option :produce-models true)

 (set-logic ALL)

-(declare-datatypes () ((a0(c0$0)(c0$1)(c0$2)(c0$3(c0$3$0 a1)(c0$3$1 Int)(c0$3$2 String)(c0$3$3 Int))(c0$4(c0$4$0 Int))(c0$5))(a1(c1$0(c1$0$0 a0)(c1$0$1 a0)(c1$0$2 String)(c1$0$3 Int))(c1$1(c1$1$0 Int))(c1$2)(c1$3(c1$3$0 Int))(c1$4)(c1$5))(a2(c2$0(c2$0$0 Int)(c2$0$1 a0))(c2$1(c2$1$0 String)(c2$1$1 a0)(c2$1$2 a1)))))

+(declare-datatypes ((a0 0)(a1 0)(a2 0)) (((c0$0) (c0$1) (c0$2) (c0$3 (c0$3$0 a1) (c0$3$1 Int) (c0$3$2 String) (c0$3$3 Int)) (c0$4 (c0$4$0 Int)) (c0$5))((c1$0 (c1$0$0 a0) (c1$0$1 a0) (c1$0$2 String) (c1$0$3 Int)) (c1$1 (c1$1$0 Int)) (c1$2) (c1$3 (c1$3$0 Int)) (c1$4) (c1$5))((c2$0 (c2$0$0 Int) (c2$0$1 a0)) (c2$1 (c2$1$0 String) (c2$1$1 a0) (c2$1$2 a1)))))

 (push 1)

 (pop 1)

 (push 1)

diff --git a/test/regress/regress1/strings/pierre150331.smt2 b/test/regress/regress1/strings/pierre150331.smt2
index ae4277874..562904366 100644
--- a/test/regress/regress1/strings/pierre150331.smt2
+++ b/test/regress/regress1/strings/pierre150331.smt2
@@ -1,13 +1,13 @@
-(set-info :smt-lib-version 2.5)

-(set-logic SLIA)

-(set-info :status sat)

-(set-option :strings-exp true)

-(define-fun stringEval ((?s String)) Bool (str.in.re ?s 

-(re.union 

-(str.to.re "H")

-(re.++ ((_ re.loop 2 2) (str.to.re "{") ) ((_ re.loop 2 4) (re.union re.nostr (re.range "" "]") (re.range "" "^") ) ) ) ) ) )

-(declare-fun s0() String)

-(declare-fun s1() String)

-(declare-fun s2() String)

-(assert (and true (stringEval s0) (stringEval s1) (distinct s0 s1) (stringEval s2) (distinct s0 s2) (distinct s1 s2) ) )

-(check-sat)

+(set-info :smt-lib-version 2.6)
+(set-logic SLIA)
+(set-info :status sat)
+(set-option :strings-exp true)
+(define-fun stringEval ((?s String)) Bool (str.in_re ?s 
+(re.union 
+(str.to_re "H")
+(re.++ ((_ re.loop 2 2) (str.to_re "{") ) ((_ re.loop 2 4) (re.union re.none (re.range "\u{1d}" "]") (re.range "\u{e}" "^") ) ) ) ) ) )
+(declare-fun s0() String)
+(declare-fun s1() String)
+(declare-fun s2() String)
+(assert (and true (stringEval s0) (stringEval s1) (distinct s0 s1) (stringEval s2) (distinct s0 s2) (distinct s1 s2) ) )
+(check-sat)