class Z3::FiniteDomainSort

# File lib/z3/sort/finite_domain_sort.rb, line 4
def initialize(name, size)
  raise Z3::Exception, "Finite domain size must be a positive Integer" unless size.is_a?(Integer) and size >= 1
  @name = name
  super LowLevel.mk_finite_domain_sort(LowLevel.mk_symbol(name), size)
end

# File lib/z3/sort/finite_domain_sort.rb, line 10
def expr_class
  FiniteDomainExpr
end

# File lib/z3/sort/finite_domain_sort.rb, line 18
def inspect
  "FiniteDomainSort(#{name}, #{size})"
end

# File lib/z3/sort/finite_domain_sort.rb, line 14
def size
  LowLevel.get_finite_domain_sort_size(_ast)
end