Theory of strings

This file provides a theory over strings. It contains all the predicates and functions currently supported by the smt-solvers CVC4 and Z3.

String operations

module String

  use int.Int

The type string is built-in. Indexes for strings start at 0.

The following functions/predicates are available in this theory:

Description	Name	Arguments	Result
Concatenate	concat	string string	string
Length	length	string	int
Get string of length 1	s_at	string int	string
Get substring	substring	string int int	string
Index of substring	indexof	string string int	int
Replace first occurrence	replace	string string string	string
Replace all occurrences	replaceall	string string string	string
String to int	to_int	string	int
Int to string	from_int	int	string
Comparison less than	lt	string string
Comparison less or equal than	le	string string
Check if it a prefix	prefixof	string string
Check if it is a suffix	suffixof	string string
Check if contains	contains	string string
Check if it is a digit	is_digit	string

  constant empty : string = ""

  function concat string string : string

  axiom concat_assoc: forall s1 s2 s3.
    concat (concat s1 s2) s3 = concat s1 (concat s2 s3)

  axiom concat_empty: forall s.
    concat s empty = concat empty s = s

  function length string : int

  (* axiom length_nonneg: forall s. length s >= 0 *)

  axiom length_empty: length "" = 0

  axiom length_concat: forall s1 s2.
    length (concat s1 s2) = length s1 + length s2

  predicate lt string string

  axiom lt_empty: forall s.
    s <> empty -> lt empty s

  axiom lt_not_com: forall s1 s2.
    lt s1 s2 -> not (lt s2 s1)

  axiom lt_ref: forall s1. not (lt s1 s1)

  axiom lt_trans: forall s1 s2 s3.
    lt s1 s2 && lt s2 s3 -> lt s1 s3

  predicate le string string

  axiom le_empty: forall s.
    le empty s

  axiom le_ref: forall s1.
    le s1 s1

  axiom lt_le: forall s1 s2.
    lt s1 s2 -> le s1 s2

  axiom lt_le_eq: forall s1 s2.
    le s1 s2 -> lt s1 s2 || s1 = s2

  axiom le_trans: forall s1 s2 s3.
    le s1 s2 && le s2 s3 -> le s1 s3

  function s_at string int : string

  axiom at_out_of_range: forall s i.
    i < 0 || i >= length s -> s_at s i = empty

  axiom at_empty: forall i.
    s_at empty i = empty

  axiom at_length: forall s i.
    let j = s_at s i in
    if 0 <= i < length s then length j = 1 else length j = 0

  axiom concat_at: forall s1 s2.
    let s = concat s1 s2 in
    forall i. (0 <= i < length s1 -> s_at s i = s_at s1 i) &&
              (length s1 <= i < length s -> s_at s i = s_at s2 (i - length s1))

  function substring string int int : string

  axiom substring_out_of_range: forall s i x.
    i < 0 || i >= length s -> substring s i x = empty

  axiom substring_of_length_zero_or_less: forall s i x.
    x <= 0 -> substring s i x = ""

  axiom substring_of_empty: forall i x.
    substring "" i x = ""

  axiom substring_smaller: forall s i x.
    length (substring s i x) <= length s

  axiom substring_smaller_x: forall s i x.
    x >= 0 -> length (substring s i x) <= x

  axiom substring_length: forall s i x.
    x >= 0 && 0 <= i < length s ->
      if i + x > length s then
        length (substring s i x) = length s - i
      else length (substring s i x) = x

  axiom substring_at: forall s i.
    s_at s i = substring s i 1

  axiom substring_substring:
    forall s ofs len ofs' len'.
    0 <= ofs <= length s -> 0 <= len -> ofs + len <= length s ->
    0 <= ofs' <= len -> 0 <= len' -> ofs' + len' <= len ->
    substring (substring s ofs len) ofs' len' = substring s (ofs + ofs') len'

  axiom concat_substring:
    forall s ofs len len'.
    0 <= ofs <= length s -> 0 <= len -> ofs + len <= length s ->
    0 <= len' -> 0 <= ofs + len + len' <= length s ->
    concat (substring s ofs len) (substring s (ofs+len) len') =
    substring s ofs (len + len')

  predicate prefixof string string

  axiom prefixof_substring: forall s1 s2.
    prefixof s1 s2 <-> s1 = substring s2 0 (length s1)

  axiom prefixof_concat: forall s1 s2.
    prefixof s1 (concat s1 s2)

  axiom prefixof_empty: forall s2.
    prefixof "" s2

  axiom prefixof_empty2: forall s1.
    s1 <> empty -> not (prefixof s1 "")

  predicate suffixof string string

  axiom suffixof_substring: forall s1 s2.
    suffixof s1 s2 <-> s1 = substring s2 (length s2 - length s1) (length s1)

  axiom suffixof_concat: forall s1 s2.
    suffixof s2 (concat s1 s2)

  axiom suffixof_empty: forall s2.
    suffixof "" s2

  axiom suffixof_empty2: forall s1.
    s1 <> empty -> not (suffixof s1 "")

  predicate contains string string

  axiom contains_prefixof: forall s1 s2.
    prefixof s1 s2 -> contains s2 s1

  axiom contains_suffixof: forall s1 s2.
    suffixof s1 s2 -> contains s2 s1

  axiom contains_empty: forall s2.
    contains "" s2 <-> s2 = empty

  axiom contains_empty2: forall s1.
    contains s1 ""

  axiom contains_substring: forall s1 s2 i.
    substring s1 i (length s2) = s2 -> contains s1 s2

  axiom contains_concat: forall s1 s2.
    contains (concat s1 s2) s1 && contains (concat s1 s2) s2

  axiom contains_at: forall s1 s2 i.
    s_at s1 i = s2 -> contains s1 s2

  function indexof string string int : int

  axiom indexof_empty: forall s i.
    0 <= i <= length s -> indexof s "" i = i

  axiom indexof_empty1: forall s i.
    let j = indexof "" s i in
    j = -1 || (s = "" && i = j = 0)

  axiom indexof_contains: forall s1 s2.
    let j = indexof s1 s2 0 in
    contains s1 s2 ->
      0 <= j <= length s1 && substring s1 j (length s2) = s2

  axiom contains_indexof: forall s1 s2 i.
    indexof s1 s2 i >= 0 -> contains s1 s2

  axiom not_contains_indexof: forall s1 s2 i.
    not (contains s1 s2)  -> indexof s1 s2 i = -1

  axiom substring_indexof: forall s1 s2 i.
    let j = indexof s1 s2 i in
    j >= 0 -> substring s1 j (length s2) = s2

  axiom indexof_out_of_range: forall i s1 s2.
    not (0 <= i <= length s1) -> indexof s1 s2 i = -1

  axiom indexof_in_range: forall s1 s2 i.
    let j = indexof s1 s2 i in
    0 <= i <= length s1 -> j = -1 || i <= j <= length s1

  axiom indexof_contains_substring: forall s1 s2 i.
    0 <= i <= length s1 && contains (substring s1 i (length s1 - i)) s2 ->
      i <= indexof s1 s2 i <= length s1

  function replace string string string : string

  axiom replace_empty: forall s1 s3.
    replace s1 "" s3 = concat s3 s1

  axiom replace_not_contains: forall s1 s2 s3.
    not (contains s1 s2) -> replace s1 s2 s3 = s1

  axiom replace_empty2: forall s2 s3.
    let s4 = replace empty s2 s3 in
    if s2 = empty then s4 = s3 else s4 = empty

  axiom replace_substring_indexof: forall s1 s2 s3.
    let j = indexof s1 s2 0 in
    replace s1 s2 s3 =
      if j < 0 then s1 else
        concat (concat (substring s1 0 j) s3)
               (substring s1 (j + length s2) (length s1 - j - length s2))

  function replaceall string string string : string

  axiom replaceall_empty1: forall s1 s3.
    replaceall s1 "" s3 = s1

  axiom not_contains_replaceall: forall s1 s2 s3.
    not (contains s1 s2) -> replaceall s1 s2 s3 = s1

  function to_int string : int

  axiom to_int_gt_minus_1: forall s. to_int s >= -1

  axiom to_int_empty: to_int "" = -1

  predicate is_digit (s:string) = 0 <= to_int s <= 9 && length s = 1

  function from_int int : string

  axiom from_int_negative: forall i.
    i < 0 <-> from_int i = empty

  axiom from_int_to_int: forall i.
    if i >= 0 then to_int (from_int i) = i else to_int (from_int i) = -1

end

Characters

module Char

  use String
  use int.Int

  type char = abstract {
    contents: string;
  } invariant {
    length contents = 1
  }

  axiom char_eq: forall c1 c2.
    c1.contents = c2.contents -> c1 = c2

  function code char : int

  axiom code: forall c. 0 <= code c < 256

  function chr (n: int) : char

  axiom code_chr: forall n. 0 <= n < 256 -> code (chr n) = n

  axiom chr_code: forall c. chr (code c) = c

  function get (s: string) (i: int) : char

  axiom get: forall s i.
    0 <= i < length s -> (get s i).contents = s_at s i

  axiom substring_get:
    forall s ofs len i.
    0 <= ofs <= length s -> 0 <= len -> ofs + len <= length s -> 0 <= i < len ->
    get (substring s ofs len) i = get s (ofs + i)

  lemma concat_first: forall s1 s2.
    let s3 = concat s1 s2 in
    forall i. 0 <= i < length s1 ->
      get s3 i = get s1 i

  lemma concat_second: forall s1 s2.
    let s3 = concat s1 s2 in
    forall i. length s1 <= i < length s1 + length s2 ->
      get s3 i = get s2 (i - length s1)

  function ([]) (s: string) (i: int) : char = get s i

  predicate eq_string (s1 s2: string) = length s1 = length s2 &&
    (forall i. 0 <= i < length s1 -> get s1 i = get s2 i)

  axiom extensionality [@W:non_conservative_extension:N]:
    forall s1 s2. eq_string s1 s2 -> s1 = s2

  meta extensionality predicate eq_string

  function make (size: int) (v: char) : string

  axiom make_length: forall size v. size >= 0 ->
    length (make size v) = size

  axiom make_contents: forall size v. size >= 0 ->
    (forall i. 0 <= i < size -> get (make size v) i = v)

end

Programming API

The following program functions are mapped to OCaml's functions. See also module io.StdIO.

module OCaml

  use int.Int
  use mach.int.Int63
  use String
  use Char

  (* In OCaml max_string_length is 144_115_188_075_855_863 *)

  val eq_char (c1 c2: char) : bool
    ensures { result <-> c1 = c2 }

  val get (s: string) (i: int63) : char
    requires { 0 <= i < length s }
    ensures  { result = get s i }

  let ([]) (s: string) (i: int63) : char
    requires { 0 <= i < length s }
    ensures  { result = get s i }
  = get s i

  val code (c: char) : int63
    ensures { result = code c }

  val chr (n: int63) : char
    requires { 0 <= n < 256 }
    ensures  { result = chr n }

  val (=) (x y: string) : bool
    ensures { result <-> x = y }

  val partial length (s: string) : int63
    ensures { result = length s >= 0 }

  val sub (s: string) (start: int63) (len: int63) : string
    requires { 0 <= start <= length s }
    requires { 0 <= len <= length s - start }
    ensures  { result = substring s start len }

  val concat (s1 s2: string) : string
    ensures  { result = concat s1 s2 }

  val make (size: int63) (v: char) : string
    requires { 0 <= size }
    ensures  { result = make size v }

end

The following module is extracted to OCaml's Buffer

module StringBuffer

  use int.Int
  use mach.int.Int63
  use String
  use Char
  use OCaml

  type buffer = abstract {
    mutable str: string;
  }
  meta coercion function str

  val create (_: int63) : buffer
    ensures { result.str = "" }

  val length (b: buffer) : int63
    ensures { result = length b.str }

  val contents (b: buffer) : string
    ensures { result = b.str }

  val clear (b: buffer) : unit
    writes  { b }
    ensures { b.str = "" }

  val reset (b: buffer) : unit
    writes  { b }
    ensures { b.str = "" }

  val sub (b: buffer) (ofs len: int63) : string
    requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length b.str }
    ensures  { result = substring b.str ofs len }

  val add_char (b: buffer) (c: char) : unit
    writes   { b }
    ensures  { b.str = concat (old b.str) c.Char.contents }

  val add_string (b: buffer) (s: string) : unit
    writes   { b }
    ensures  { b.str = concat (old b.str) s }

  val truncate (b: buffer) (n: int63) : unit
    requires { 0 <= n <= length b.str }
    writes   { b }
    ensures  { b.str = substring (old b.str) 0 n }

end

String realization

This module is intended for string realization. It clones the String module replacing axioms by goals.

module StringRealization

  clone export String
    with goal .

end

Regular expressions

module RegExpr

  use String as S

  type re

  function to_re string : re

  predicate in_re string re

  function concat re re : re

  function union re re : re

  function inter re re : re

  function star re : re

  function plus re : re

  constant none : re

  constant allchar : re

  constant all : re = star allchar

  function opt re : re

  function range string string : re

  function power int re : re

  function loop int int re : re

end