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