Class: Z3::ArraySort

Inherits:
Sort show all
Defined in:
lib/z3/sort/array_sort.rb

Instance Attribute Summary collapse

Attributes inherited from AST

#_ast

Instance Method Summary collapse

Methods inherited from Sort

#<, #<=, #<=>, #==, #>, #>=, #cast, #eql?, from_pointer, #from_value, #hash, #new, #value_class, #var

Methods inherited from AST

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

Constructor Details

#initialize(key_sort, value_sort) ⇒ ArraySort

Returns a new instance of ArraySort.



4
5
6
7
8
 
# File 'lib/z3/sort/array_sort.rb', line 4

def initialize(key_sort, value_sort)
  @key_sort = key_sort
  @value_sort = value_sort
  super LowLevel.mk_array_sort(key_sort, value_sort)
end

Instance Attribute Details

#key_sort ⇒ Object (readonly)

Returns the value of attribute key_sort.



3
4
5
 
# File 'lib/z3/sort/array_sort.rb', line 3

def key_sort
  @key_sort
end

#value_sort ⇒ Object (readonly)

Returns the value of attribute value_sort.



3
4
5
 
# File 'lib/z3/sort/array_sort.rb', line 3

def value_sort
  @value_sort
end

Instance Method Details

#expr_class ⇒ Object 



10
11
12
 
# File 'lib/z3/sort/array_sort.rb', line 10

def expr_class
  ArrayExpr
end

#inspect ⇒ Object 



18
19
20
 
# File 'lib/z3/sort/array_sort.rb', line 18

def inspect
  "ArraySort(#{key_sort}, #{value_sort})"
end

#to_s ⇒ Object 



14
15
16
 
# File 'lib/z3/sort/array_sort.rb', line 14

def to_s
  "Array(#{key_sort}, #{value_sort})"
end