Initial support for string standard in smt lib 2.6 (#1848)

30 files changed, 48 insertions, 11 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index f8a32046f..3674e42bb 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -788,6 +788,7 @@ REG0_TESTS = \
 	regress0/strings/norn-simp-rew.smt2 \
 	regress0/strings/repl-rewrites2.smt2 \
 	regress0/strings/rewrites-v2.smt2 \
+	regress0/strings/std2.6.1.smt2 \
 	regress0/strings/str003.smt2 \
 	regress0/strings/str004.smt2 \
 	regress0/strings/str005.smt2 \
diff --git a/test/regress/regress0/strings/bug002.smt2 b/test/regress/regress0/strings/bug002.smt2
index f8a481e14..fd60089fd 100644
--- a/test/regress/regress0/strings/bug002.smt2
+++ b/test/regress/regress0/strings/bug002.smt2
@@ -1,5 +1,5 @@
-(set-logic ASLIA)
 (set-info :smt-lib-version 2.0)
+(set-logic ASLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
 
@@ -7,4 +7,4 @@
 (define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.loop re.allchar 6 ) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) )  ) )
 (assert (not (strinre "6O\1\127\n?")))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/strings/issue1189.smt2 b/test/regress/regress0/strings/issue1189.smt2
index fae641ea8..0b581994c 100644
--- a/test/regress/regress0/strings/issue1189.smt2
+++ b/test/regress/regress0/strings/issue1189.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress0/strings/leadingzero001.smt2 b/test/regress/regress0/strings/leadingzero001.smt2
index 2889348c1..09fd80a7b 100644
--- a/test/regress/regress0/strings/leadingzero001.smt2
+++ b/test/regress/regress0/strings/leadingzero001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress0/strings/norn-31.smt2 b/test/regress/regress0/strings/norn-31.smt2
index 4698f966f..1830dd882 100644
--- a/test/regress/regress0/strings/norn-31.smt2
+++ b/test/regress/regress0/strings/norn-31.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)
diff --git a/test/regress/regress0/strings/norn-simp-rew.smt2 b/test/regress/regress0/strings/norn-simp-rew.smt2
index 45f7ede94..d729fe5d0 100644
--- a/test/regress/regress0/strings/norn-simp-rew.smt2
+++ b/test/regress/regress0/strings/norn-simp-rew.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)
@@ -26,4 +27,4 @@
 (assert (str.in.re var_8 (re.* (re.range "a" "u"))))
 (assert (str.in.re var_7 (re.* (re.range "a" "u"))))
 (assert (not (str.in.re (str.++ "b" var_7 ) (re.* (re.range "a" "u")))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/strings/rewrites-v2.smt2 b/test/regress/regress0/strings/rewrites-v2.smt2
index 7e285b51a..ce2f140ae 100644
--- a/test/regress/regress0/strings/rewrites-v2.smt2
+++ b/test/regress/regress0/strings/rewrites-v2.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --strings-exp
 ; EXPECT: unsat
+(set-info :smt-lib-version 2.5)
 (set-logic SLIA)
 (set-info :status unsat)
 (declare-fun x () String)
diff --git a/test/regress/regress0/strings/std2.6.1.smt2 b/test/regress/regress0/strings/std2.6.1.smt2
new file mode 100644
index 000000000..3302a29e5
--- /dev/null
+++ b/test/regress/regress0/strings/std2.6.1.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp --lang=smt2.6.1
+; EXPECT: sat
+(set-logic QF_UFSLIA)
+(set-info :status sat)
+(declare-fun x () String)
+(assert (str.in-re x (str.to-re "A")))
+(declare-fun y () Int)
+(assert (= (str.to-int (str.from-int y)) y))
+(check-sat)
diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2
index 77eabcccc..89191ac34 100644
--- a/test/regress/regress0/strings/type001.smt2
+++ b/test/regress/regress0/strings/type001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -18,4 +19,4 @@
 ;should be -1
 (assert (= j (str.to.int "-783914785582390527685649")))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/strings/artemis-0512-nonterm.smt2 b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
index 4b1cad8f6..a3cca23a2 100644
--- a/test/regress/regress1/strings/artemis-0512-nonterm.smt2
+++ b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status unsat)
diff --git a/test/regress/regress1/strings/bug615.smt2 b/test/regress/regress1/strings/bug615.smt2
index 86cc592fb..673b0dbd0 100644
--- a/test/regress/regress1/strings/bug615.smt2
+++ b/test/regress/regress1/strings/bug615.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/bug686dd.smt2 b/test/regress/regress1/strings/bug686dd.smt2
index 7c923654d..0cb9fac26 100644
--- a/test/regress/regress1/strings/bug686dd.smt2
+++ b/test/regress/regress1/strings/bug686dd.smt2
@@ -1,7 +1,8 @@
+(set-info :smt-lib-version 2.5)
 (set-logic UFDTSLIA)
 (set-info :status sat)
 
-(declare-datatypes ((T 0)) ( ((TC (TCb String))) ) )
+(declare-datatypes () ((T (TC (TCb String)))))
 
 (declare-fun root5 () String)
 (declare-fun root6 () T)
diff --git a/test/regress/regress1/strings/bug799-min.smt2 b/test/regress/regress1/strings/bug799-min.smt2
index 06acffc97..0cd15af4e 100644
--- a/test/regress/regress1/strings/bug799-min.smt2
+++ b/test/regress/regress1/strings/bug799-min.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --incremental --strings-exp
 ; EXPECT: sat
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/fmf001.smt2 b/test/regress/regress1/strings/fmf001.smt2
index 6081c8e06..71ae63e87 100644
--- a/test/regress/regress1/strings/fmf001.smt2
+++ b/test/regress/regress1/strings/fmf001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
diff --git a/test/regress/regress1/strings/fmf002.smt2 b/test/regress/regress1/strings/fmf002.smt2
index d52dae2d2..ab3dc2ae2 100644
--- a/test/regress/regress1/strings/fmf002.smt2
+++ b/test/regress/regress1/strings/fmf002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
diff --git a/test/regress/regress1/strings/issue1105.smt2 b/test/regress/regress1/strings/issue1105.smt2
index 81e7672da..bf5cb7669 100644
--- a/test/regress/regress1/strings/issue1105.smt2
+++ b/test/regress/regress1/strings/issue1105.smt2
@@ -1,9 +1,10 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)
-(declare-datatype Val (
+(declare-datatypes () ((Val
     (Str (str String))
-    (Num (num Int))))
+    (Num (num Int)))))
 
 (declare-const var0 Val)
 (assert (=> (is-Str var0) (distinct (str.to.int (str var0)) (- 1))))
diff --git a/test/regress/regress1/strings/kaluza-fl.smt2 b/test/regress/regress1/strings/kaluza-fl.smt2
index 04775d61c..20c2e6aa4 100644
--- a/test/regress/regress1/strings/kaluza-fl.smt2
+++ b/test/regress/regress1/strings/kaluza-fl.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/norn-360.smt2 b/test/regress/regress1/strings/norn-360.smt2
index 573dcbe01..20ab0b338 100644
--- a/test/regress/regress1/strings/norn-360.smt2
+++ b/test/regress/regress1/strings/norn-360.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_4 (re.* (re.range "a" "u"))))
 (assert (str.in.re var_3 (re.* (re.range "a" "u"))))
 (assert (<= 0  (str.len var_4)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/strings/norn-ab.smt2 b/test/regress/regress1/strings/norn-ab.smt2
index 48d889847..47c218179 100644
--- a/test/regress/regress1/strings/norn-ab.smt2
+++ b/test/regress/regress1/strings/norn-ab.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (set-option :strings-exp true)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
 (assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))))
 (assert (and (<= 0  (str.len var_4)) (not (not (exists ((v Int)) (= (* v 2 ) (+ (str.len var_4) 2 )))))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/strings/norn-nel-bug-052116.smt2 b/test/regress/regress1/strings/norn-nel-bug-052116.smt2
index f0c2534a1..9f06152f7 100644
--- a/test/regress/regress1/strings/norn-nel-bug-052116.smt2
+++ b/test/regress/regress1/strings/norn-nel-bug-052116.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/norn-simp-rew-sat.smt2 b/test/regress/regress1/strings/norn-simp-rew-sat.smt2
index 01a102bf9..1336d3bfc 100644
--- a/test/regress/regress1/strings/norn-simp-rew-sat.smt2
+++ b/test/regress/regress1/strings/norn-simp-rew-sat.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_3 (re.* (re.range "a" "u"))))
 (assert (str.in.re var_3 (re.* (str.to.re "a"))))
 (assert (<= 0  (str.len var_4)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/strings/pierre150331.smt2 b/test/regress/regress1/strings/pierre150331.smt2
index 88d5ec10c..add60d534 100644
--- a/test/regress/regress1/strings/pierre150331.smt2
+++ b/test/regress/regress1/strings/pierre150331.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)

 (set-logic SLIA)

 (set-info :status sat)

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

@@ -10,4 +11,4 @@
 (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)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress1/strings/regexp001.smt2 b/test/regress/regress1/strings/regexp001.smt2
index 62c142d1d..142ff679d 100644
--- a/test/regress/regress1/strings/regexp001.smt2
+++ b/test/regress/regress1/strings/regexp001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/regexp002.smt2 b/test/regress/regress1/strings/regexp002.smt2
index a8bd2187a..f109a484e 100644
--- a/test/regress/regress1/strings/regexp002.smt2
+++ b/test/regress/regress1/strings/regexp002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/regexp003.smt2 b/test/regress/regress1/strings/regexp003.smt2
index 7696838fe..7c05b422f 100644
--- a/test/regress/regress1/strings/regexp003.smt2
+++ b/test/regress/regress1/strings/regexp003.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/reloop.smt2 b/test/regress/regress1/strings/reloop.smt2
index 9915504ae..967e564ce 100644
--- a/test/regress/regress1/strings/reloop.smt2
+++ b/test/regress/regress1/strings/reloop.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/string-unsound-sem.smt2 b/test/regress/regress1/strings/string-unsound-sem.smt2
index 771d8d4b0..44591b47b 100644
--- a/test/regress/regress1/strings/string-unsound-sem.smt2
+++ b/test/regress/regress1/strings/string-unsound-sem.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/type002.smt2 b/test/regress/regress1/strings/type002.smt2
index 0df0f20b0..458ac75fe 100644
--- a/test/regress/regress1/strings/type002.smt2
+++ b/test/regress/regress1/strings/type002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/type003.smt2 b/test/regress/regress1/strings/type003.smt2
index c2d4792cc..4185041f7 100644
--- a/test/regress/regress1/strings/type003.smt2
+++ b/test/regress/regress1/strings/type003.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/username_checker_min.smt2 b/test/regress/regress1/strings/username_checker_min.smt2
index 2f1c35844..f6c152a2a 100644
--- a/test/regress/regress1/strings/username_checker_min.smt2
+++ b/test/regress/regress1/strings/username_checker_min.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status unsat)