class Z3::Model

Attributes

_model[R]

Public Class Methods

new(_model) click to toggle source
# File lib/z3/model.rb, line 6
def initialize(_model)
  @_model = _model
end

Public Instance Methods

!() click to toggle source
# File lib/z3/model.rb, line 53
def !
  Z3.Or(
    *map{|v| v != self[v]}
  )
end
[](ast) click to toggle source
# File lib/z3/model.rb, line 32
def [](ast)
  model_eval(ast)
end
consts() click to toggle source
# 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
each() { |range.var(name), new_from_pointer(model_get_const_interp)| ... } click to toggle source
# 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
inspect() click to toggle source
# File lib/z3/model.rb, line 40
def inspect
  to_s
end
model_eval(ast, model_completion=false) click to toggle source
# 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
num_consts() click to toggle source
# File lib/z3/model.rb, line 10
def num_consts
  LowLevel.model_get_num_consts(self)
end
num_funcs() click to toggle source
# File lib/z3/model.rb, line 24
def num_funcs
  LowLevel.model_get_num_funcs(self)
end
num_sorts() click to toggle source
# File lib/z3/model.rb, line 20
def num_sorts
  LowLevel.model_get_num_sorts(self)
end
to_s() click to toggle source
# File lib/z3/model.rb, line 36
def to_s
  "Z3::Model<#{ map{|n,v| "#{n}=#{v}"}.join(", ") }>"
end