class Z3::ArrayExpr - RDoc Documentation

Source

# File lib/z3/expr/array_expr.rb, line 21
def [](key)
  select(key)
end

default ()

Source

# File lib/z3/expr/array_expr.rb, line 28
def default
  value_sort.new(LowLevel.mk_array_default(self))
end

The array’s fallback - what it answers for keys nothing has stored to. It’s the same idea as the Hash default a model reports for a function, and store leaves it alone, so ‘ArraySort#Const(0).store(7, 1).default` is still 0.

key_sort ()

Source

# File lib/z3/expr/array_expr.rb, line 5
def key_sort
  sort.key_sort
end

select (key)

Source

# File lib/z3/expr/array_expr.rb, line 17
def select(key)
  sort.value_sort.new LowLevel.mk_select(self, key_sort.cast(key))
end

store (key, value)

Source

# File lib/z3/expr/array_expr.rb, line 13
def store(key, value)
  sort.new LowLevel.mk_store(self, key_sort.cast(key), value_sort.cast(value))
end

value_sort ()

Source

# File lib/z3/expr/array_expr.rb, line 9
def value_sort
  sort.value_sort
end