Class: Z3::ArrayExpr

Inherits:
Expr show all
Defined in:
lib/z3/expr/array_expr.rb

Instance Attribute Summary

Attributes inherited from Expr

#sort

Attributes inherited from AST

#_ast

Instance Method Summary collapse

Methods inherited from Expr

#!=, #==, Add, And, Distinct, Eq, Ge, Gt, Le, Lt, Mul, Or, Sub, Xor, coerce_to_same_sort, #initialize, #inspect, new_from_pointer, sort_for_const

Methods inherited from AST

#arguments, #ast_kind, #eql?, #func_decl, #hash, #initialize, #sexpr, #simplify, #to_s

Constructor Details

This class inherits a constructor from Z3::Expr

Instance Method Details

#[](key) ⇒ Object 



21
22
23
 
# File 'lib/z3/expr/array_expr.rb', line 21

def [](key)
  select(key)
end

#key_sort ⇒ Object 



5
6
7
 
# File 'lib/z3/expr/array_expr.rb', line 5

def key_sort
  sort.key_sort
end

#select(key) ⇒ Object 



17
18
19
 
# 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) ⇒ Object 



13
14
15
 
# 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 ⇒ Object 



9
10
11
 
# File 'lib/z3/expr/array_expr.rb', line 9

def value_sort
  sort.value_sort
end