class Z3::Model

Public Class Methods

Source

# File lib/z3/model.rb, line 7
def initialize(_model)
  @_model = _model
  # Without this the solver reclaims the model as soon as it produces another one
  inc_ref! :model, _model
end

Public Instance Methods

! ()

Source

# File lib/z3/model.rb, line 104
def !
  differences = []
  each_const { |var, _value| differences << (var != self[var]) }
  # A model with no consts constrains nothing, so there is nothing to differ in
  return Z3.False if differences.empty?
  Z3.Or(*differences)
end

Only constants are negated. Saying “some function differs somewhere” needs a quantifier, so a model with functions in it can repeat under this.

[] (ast)

Source

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

consts ()

Source

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

each (&block)

Source

# File lib/z3/model.rb, line 79
def each(&block)
  return to_enum(:each) unless block_given?
  each_const(&block)
  each_func(&block)
end

Constants come back as ‘variable, value` pairs, functions as `func_decl, interpretation` - see func_interp for what an interpretation looks like

each_const () { |range.var(name), new_from_pointer(model_get_const_interp)| ... }

Source

# File lib/z3/model.rb, line 85
def each_const
  return to_enum(:each_const) unless block_given?
  consts.sort_by { |c| c.name.to_s }.each do |c|
    yield(
      c.range.var(c.name),
      Expr.new_from_pointer(LowLevel.model_get_const_interp(self, c))
    )
  end
end

each_func () { |f, func_interp(f)| ... }

Source

# File lib/z3/model.rb, line 95
def each_func
  return to_enum(:each_func) unless block_given?
  funcs.sort_by { |f| f.name.to_s }.each do |f|
    yield(f, func_interp(f))
  end
end

func_interp (func_decl)

Source

# File lib/z3/model.rb, line 54
def func_interp(func_decl)
  raise Z3::Exception, "FuncDecl expected, got #{AST.describe(func_decl)}" unless func_decl.is_a?(FuncDecl)
  _func_interp = LowLevel.model_get_func_interp(self, func_decl)
  raise Z3::Exception, "Model has no interpretation for #{func_decl}" if _func_interp.null?
  LowLevel.unpack_func_interp(_func_interp)
end

What the model decided a function does, as a Hash from argument lists to values with Ruby’s Hash default standing in for Z3’s ‘else` branch - so `interp[]` answers for arguments the model never had to pin down.

funcs ()

Source

# File lib/z3/model.rb, line 45
def funcs
  (0...num_funcs).map do |i|
    FuncDecl.new(LowLevel.model_get_func_decl(self, i))
  end
end

inspect ()

Source

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

model_eval (ast, model_completion=false)

Source

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

num_consts ()

Source

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

num_funcs ()

Source

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

num_sorts ()

Source

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

sort_universe (sort)

Source

# File lib/z3/model.rb, line 36
def sort_universe(sort)
  raise Z3::Exception, "Sort expected, got #{AST.describe(sort)}" unless sort.is_a?(Sort)
  LowLevel.unpack_ast_vector(LowLevel.model_get_sort_universe(self, sort))
end

Every element the model gave an uninterpreted sort. Z3 only ever needs finitely many, so this is the whole sort as far as this model is concerned.

sorts ()

Source

# File lib/z3/model.rb, line 28
def sorts
  (0...num_sorts).map do |i|
    Sort.from_pointer(LowLevel.model_get_sort(self, i))
  end
end

The uninterpreted sorts the model had to invent elements for

to_s ()

Source

# File lib/z3/model.rb, line 69
def to_s
  "Z3::Model<#{ map{|name, value| "#{name}=#{Printer.new.format_value(value)}"}.join(", ") }>"
end