class Z3::ReSort

Public Instance Methods

Source

# File lib/z3/sort/re_sort.rb, line 40
def all_char
  new(LowLevel.mk_re_allchar(self))
end

empty ()

Source

# File lib/z3/sort/re_sort.rb, line 32
def empty
  new(LowLevel.mk_re_empty(self))
end

‘re.none`, `re.all` and `re.allchar` - the empty language, every sequence, and every one element sequence. Values rather than operations, so they live here the way BoolSort#True does.

expr_class ()

Source

# File lib/z3/sort/re_sort.rb, line 9
def expr_class
  ReExpr
end

from_const (val)

Source

# File lib/z3/sort/re_sort.rb, line 17
def from_const(val)
  new(LowLevel.mk_seq_to_re(seq_sort.from_const(val)))
end

Z3 has no regex literals, and nothing converts a Ruby Regexp - see ReExpr for why. What does convert is a sequence: ‘seq.to_re` is the regex matching exactly that one sequence, so a Ruby String converts to a `Re(String)` and a Ruby Array to a `Re(Seq(…))`, through the basis sort’s own conversion.

from_value (v)

Source

# File lib/z3/sort/re_sort.rb, line 23
def from_value(v)
  return v if v.sort == self
  raise cant_convert(v) unless v.sort == seq_sort
  new(LowLevel.mk_seq_to_re(v))
end

The same conversion for a sequence that’s already an Expr, so a StringExpr or a SeqExpr of the basis sort can stand in for a regex too

full ()

Source

# File lib/z3/sort/re_sort.rb, line 36
def full
  new(LowLevel.mk_re_full(self))
end

inspect ()

Source

# File lib/z3/sort/re_sort.rb, line 48
def inspect
  "ReSort(#{seq_sort})"
end

to_s ()

Source

# File lib/z3/sort/re_sort.rb, line 44
def to_s
  "Re(#{seq_sort})"
end

class Z3::ReSort

Attributes

Public Class Methods

Public Instance Methods