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.

1 files changed, 69 insertions, 0 deletions

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)