class Z3::SeqExpr

Z3 has no String sort of its own - a String is a Seq(Char), and ‘str.++` is the same operation as `seq.++`. The Exprs still don’t share a hierarchy, because the Ruby side of them doesn’t: a SeqExpr should read like a Ruby Array and a StringExpr like a Ruby String, and those two have no common ancestor either. Where a seq and a string operation really are one Z3 operation, they share the LowLevel call, not a superclass.

That split is what settles the element-versus-subsequence question. Every Z3 seq operation takes a subsequence, but Ruby’s Array#include? / index take an element, and Ruby wins - as it does everywhere the two disagree: a bare element is wrapped into a one element sequence, while a SeqExpr of this very sort or a Ruby Array is taken as the subsequence it already is.

Public Class Methods

Concat (*args)

Source

# File lib/z3/expr/seq_expr.rb, line 160
def Concat(*args)
  raise Z3::Exception, "Concat requires at least one argument" if args.empty?
  args = coerce_to_same_seq_sort(*args)
  # Z3 rejects a concatenation of fewer than two sequences
  return args[0] if args.size == 1
  args[0].sort.new(LowLevel.mk_seq_concat(args))
end

Unit (element)

Source

# File lib/z3/expr/seq_expr.rb, line 150
def Unit(element)
  SeqSort.new(element.sort).new(LowLevel.mk_seq_unit(element))
end

A one element sequence. Z3 needs these to build any sequence value at all, and they’re what makes the element-taking methods above work.

coerce_to_same_seq_sort (*args)

Source

# File lib/z3/expr/seq_expr.rb, line 154
def coerce_to_same_seq_sort(*args)
  args = coerce_to_same_sort(*args)
  raise Z3::Exception, "Seq value with same element sort expected" unless args[0].is_a?(SeqExpr)
  args
end

new (_ast, sort)

Source

# File lib/z3/expr/expr.rb, line 5
def initialize(_ast, sort)
  super(_ast)
  @sort = sort
  raise Z3::Exception, "Values must have AST kind numeral, app, or quantifier" unless [:numeral, :app, :quantifier].include?(ast_kind)
end

Calls superclass method Z3::Expr::new

Public Instance Methods

* (count)

Source

# File lib/z3/expr/seq_expr.rb, line 41
def *(count)
  raise Z3::Exception, "Can only repeat a Seq a non-negative Integer number of times" unless count.is_a?(Integer) and count >= 0
  return sort.from_const([]) if count == 0
  SeqExpr.Concat(*([self] * count))
end

Ruby Array#* repeats. Only the Integer form - Array#*(String) is join, and there’s no joining a sequence of arbitrary element sort into a String.

+ (other)

Source

# File lib/z3/expr/seq_expr.rb, line 35
def +(other)
  SeqExpr.Concat(self, other)
end

Ruby Array#+ is concatenation, and so is ‘seq.++`

[] (index, len=nil)

Source

# File lib/z3/expr/seq_expr.rb, line 55
def [](index, len=nil)
  if len
    subseq(index, len)
  elsif index.is_a?(Range)
    subseq(*Expr.offset_and_length(index, length))
  else
    element_sort.new(LowLevel.mk_seq_nth(self, IntSort.new.cast(index)))
  end
end

Ruby Array#[]. ‘xs` is the element (`seq.nth`), `xs[i, len]` and `xs` are subsequences (`seq.extract`).

An index is an offset, and a negative one is not counted from the end the way Ruby’s is - see StringExpr#[] for why. Counting from the end is ‘xs[xs.length - 1]`, which is what last does. Out of range is whatever Z3 says: a subsequence is empty, and an element is left unspecified, so an out of range `xs` is a term the solver may pick any value for. It denotes an element, and no element is `nil`.

Also aliased as: slice

at (index)

Source

# File lib/z3/expr/seq_expr.rb, line 69
def at(index)
  self[index]
end

Ruby Array#at - the element, same as ‘xs`

element_sort ()

Source

# File lib/z3/expr/seq_expr.rb, line 17
def element_sort
  sort.element_sort
end

empty? ()

Source

# File lib/z3/expr/seq_expr.rb, line 30
def empty?
  length == 0
end

end_with? (*suffixes)

Source

# File lib/z3/expr/seq_expr.rb, line 100
def end_with?(*suffixes)
  return BoolSort.new.False if suffixes.empty?
  matches = suffixes.map { |suffix|
    BoolSort.new.new(LowLevel.mk_seq_suffix(cast_to_seq(suffix), self))
  }
  # `Or` of one thing prints as `or(...)`, and every caller is more likely to pass one
  matches.size == 1 ? matches[0] : BoolExpr.Or(*matches)
end

first (n=nil)

Source

# File lib/z3/expr/seq_expr.rb, line 74
def first(n=nil)
  n ? subseq(0, n) : self[0]
end

Ruby Array#first / last, including their “n of them” second form

gsub (pattern, replacement)

Source

# File lib/z3/expr/seq_expr.rb, line 139
def gsub(pattern, replacement)
  if pattern.is_a?(ReExpr)
    sort.new(LowLevel.mk_seq_replace_re_all(self, ReExpr.expect_re_over(pattern, sort), cast_to_seq(replacement)))
  else
    sort.new(LowLevel.mk_seq_replace_all(self, cast_to_seq(pattern), cast_to_seq(replacement)))
  end
end

include? (element_or_subsequence)

Source

# File lib/z3/expr/seq_expr.rb, line 84
def include?(element_or_subsequence)
  BoolSort.new.new(LowLevel.mk_seq_contains(self, cast_to_seq(element_or_subsequence)))
end

Ruby Array#include? takes an element, so that’s what this expects - pass a SeqExpr of this sort, or a Ruby Array, to ask about a subsequence instead

index (element_or_subsequence, offset=0)

Source

# File lib/z3/expr/seq_expr.rb, line 112
def index(element_or_subsequence, offset=0)
  IntSort.new.new(LowLevel.mk_seq_index(self, cast_to_seq(element_or_subsequence), IntSort.new.cast(offset)))
end

Ruby Array#index. This denotes an Int, so there’s no ‘nil` available for it to be when there’s no match - ‘seq.indexof` answers -1, and that’s what comes back. It also takes a starting offset, which Ruby’s Array#index doesn’t.

last (n=nil)

Source

# File lib/z3/expr/seq_expr.rb, line 78
def last(n=nil)
  n ? subseq(length - n, n) : self[length - 1]
end

length ()

Source

# File lib/z3/expr/seq_expr.rb, line 22
def length
  IntSort.new.new(LowLevel.mk_seq_length(self))
end

Ruby Array has both length and size, so this has both too

matches? (re)

Source

# File lib/z3/expr/seq_expr.rb, line 123
def matches?(re)
  BoolSort.new.new(LowLevel.mk_seq_in_re(self, ReExpr.expect_re_over(re, sort)))
end

‘seq.in_re`, the same operation as StringExpr#matches? and named the same way - see there for why it isn’t ‘match?`, and why the argument is never converted

rindex (element_or_subsequence)

Source

# File lib/z3/expr/seq_expr.rb, line 117
def rindex(element_or_subsequence)
  IntSort.new.new(LowLevel.mk_seq_last_index(self, cast_to_seq(element_or_subsequence)))
end

Ruby Array#rindex. Z3’s ‘seq.last_indexof` takes no offset, so neither does this.

size ()

Source

# File lib/z3/expr/seq_expr.rb, line 26
def size
  length
end

slice (index, len=nil)

Ruby Array#slice is Array#[]

Alias for: []

start_with? (*prefixes)

Source

# File lib/z3/expr/seq_expr.rb, line 91
def start_with?(*prefixes)
  return BoolSort.new.False if prefixes.empty?
  matches = prefixes.map { |prefix|
    BoolSort.new.new(LowLevel.mk_seq_prefix(cast_to_seq(prefix), self))
  }
  # `Or` of one thing prints as `or(...)`, and every caller is more likely to pass one
  matches.size == 1 ? matches[0] : BoolExpr.Or(*matches)
end

Z3’s ‘seq.prefixof` takes the prefix first and the sequence second. Ruby’s Array has no start_with?, so String’s spelling is reused, and like String’s it holds if any candidate matches.

sub (pattern, replacement)

Source

# File lib/z3/expr/seq_expr.rb, line 131
def sub(pattern, replacement)
  if pattern.is_a?(ReExpr)
    sort.new(LowLevel.mk_seq_replace_re(self, ReExpr.expect_re_over(pattern, sort), cast_to_seq(replacement)))
  else
    sort.new(LowLevel.mk_seq_replace(self, cast_to_seq(pattern), cast_to_seq(replacement)))
  end
end

Ruby Array has nothing like these, so they keep String’s names along with String’s first-one versus every-one split. The pattern can be a ReExpr here too, which is the one argument that isn’t read as an element-or-subsequence - and which Z3 4.16 can build but not yet reason about, see StringExpr#sub.