From 31efb570a9d5811fd88a34d4915d7d08c81d13fa Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 28 Feb 2020 22:20:18 -0800 Subject: Add support for str.from_code (#3829) This commit adds support for `str.from_code`. This is work towards supporting the new strings standard. The code currently just does an eager expansion of the operator. The commit also renames `STRING_CODE` to `STRING_TO_CODE` to better reflect the names of the operators in the new standard. --- test/regress/regress0/strings/from_code.smt2 | 69 ++++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 test/regress/regress0/strings/from_code.smt2 (limited to 'test/regress/regress0/strings') diff --git a/test/regress/regress0/strings/from_code.smt2 b/test/regress/regress0/strings/from_code.smt2 new file mode 100644 index 000000000..ecde829ec --- /dev/null +++ b/test/regress/regress0/strings/from_code.smt2 @@ -0,0 +1,69 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; EXPECT: unsat +; EXPECT: unsat +(set-option :incremental true) +(set-logic QF_SLIA) +(declare-const s String) +(declare-const t String) +(declare-const n Int) + +(push) +(assert (not (= (str.to_code (str.from_code (str.to_code s))) (str.to_code s)))) +(check-sat) +(pop) + +(push) +(assert (not (= (str.from_code (str.to_code s)) s))) +(assert (<= (str.len s) 1)) +(check-sat) +(pop) + +(push) +(assert (not (= (str.from_code (str.to_code s)) s))) +(check-sat) +(pop) + +(push) +(assert (not (= (str.from_code (str.to_code (str.from_code n))) (str.from_code n)))) +(check-sat) +(pop) + +(push) +(assert (not (= (str.to_code (str.from_code n)) n))) +(assert (>= n 0)) +(check-sat) +(pop) + +(push) +(assert (not (= (str.to_code (str.from_code n)) n))) +(assert (and (>= n 0) (< n 50))) +(check-sat) +(pop) + +(push) +(assert (not (= (str.to_code (str.from_code n)) n))) +(check-sat) +(pop) + +(push) +(assert (= (str.to_code s) (str.to_code t))) +(assert (= (str.len s) 1)) +(assert (= (str.len t) 1)) +(assert (not (= (str.from_code (str.to_code s)) (str.from_code (str.to_code t))))) +(check-sat) +(pop) + +(push) +(assert (or + (not (= (str.from_code (- 1)) "")) + (not (= (str.from_code 100000000000000000000000) "")) + (not (= (str.from_code 65) "A")))) +(check-sat) +(pop) -- cgit v1.2.3