class Z3::Model

# File lib/z3/model.rb, line 6
def initialize(_model)
  @_model = _model
end

# File lib/z3/model.rb, line 53
def !
  Z3.Or(
    *map{|v| v != self[v]}
  )
end

# File lib/z3/model.rb, line 32
def [](ast)
  model_eval(ast)
end

# File lib/z3/model.rb, line 14
def consts
  (0...num_consts).map do |i|
    FuncDecl.new(LowLevel.model_get_const_decl(self, i))
  end
end

# File lib/z3/model.rb, line 44
def each
  consts.sort_by(&:name).each do |c|
    yield(
      c.range.var(c.name),
      Expr.new_from_pointer(LowLevel.model_get_const_interp(self, c))
    )
  end
end

# File lib/z3/model.rb, line 40
def inspect
  to_s
end

# File lib/z3/model.rb, line 28
def model_eval(ast, model_completion=false)
  Expr.new_from_pointer(LowLevel.model_eval(self, ast, model_completion))
end

# File lib/z3/model.rb, line 10
def num_consts
  LowLevel.model_get_num_consts(self)
end

# File lib/z3/model.rb, line 24
def num_funcs
  LowLevel.model_get_num_funcs(self)
end

# File lib/z3/model.rb, line 20
def num_sorts
  LowLevel.model_get_num_sorts(self)
end

# File lib/z3/model.rb, line 36
def to_s
  "Z3::Model<#{ map{|n,v| "#{n}=#{v}"}.join(", ") }>"
end