class Z3::Printer

Z3 always spells the starting offset out, Ruby’s String#index / Array#index default it to 0 - so a trailing 0 is noise, and ‘s.index(“a”)` is what anyone would have written

Same idea, but Z3 takes the prefix/suffix first and the string second, where Ruby’s String#start_with? / end_with? take it the other way round - so it’s the second argument that prints as the receiver.

Z3 decl name => Ruby method, printed as ‘receiver.method` or `receiver.method(rest)` with the first argument as the receiver. Z3 names the same operation `str.foo` for Strings and `seq.foo` for every other Seq, so both spellings map to the one Ruby method - except `replace_all`, which Z3 calls `str.replace_all` even for sequences of non-characters.

Lexicographic string comparison. These are operators in Ruby, but their Z3 names contain letters, so the generic operator path doesn’t catch them.

Concat, union and intersection are associative, and Z3 hands them back as a nested binary tree however many arguments they were built with

The regexes with no arguments at all, named after the constructors that build them. Z3 calls the empty language ‘re.none` over Strings and `re.empty` over every other sequence sort.

…and the ones that print as methods, since Ruby has no operators to spare

Regex operations that print as Ruby operators on ReExpr. ‘re.++` is concatenation and `re.+` is one-or-more - different Z3 names, so no clash.

‘str.++` is the same operation as `seq.++`, Z3 just names it differently for String

Argument positions that take an element-or-subsequence. ‘xs.include?(7)` builds `(seq.contains xs (seq.unit 7))`, and printing that back as `xs.include?()` is correct but isn’t what anyone wrote - Ruby’s Array#include? takes the element, so a lone unit in one of these positions prints as the element it wraps.