Skip to main content

Unicode Characters

The Unicode sort ranges over unicode characters.

A few operations are supported over characters.

1
2
3
4
5
6
7
(declare-const a Unicode)

(declare-const b Unicode)

(simplify (char.<= a b))

(simplify (char.<= (_ Char 1) (_ Char 2)))

(simplify (char.to_int (_ Char 1)))

(simplify (char.is_digit (_ Char 1)))

(simplify (char.is_digit (_ Char 49))) ; it is the digit 1

While Unicode is the default you can set the encoding of characters to ASCII (8 bit) or Bmp (16 bit).

(set-option :encoding unicode)
(set-option :encoding ascii)
(set-option :encoding bmp)