Class: Z3::Model

Inherits:
Object
  • Object
show all
Includes:
Enumerable, ReferenceCounted
Defined in:
lib/z3/model.rb

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from ReferenceCounted

finalizer

Constructor Details

#initialize(_model) ⇒ Model

Returns a new instance of Model.



7
8
9
10
11
 
# 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

Instance Attribute Details

#_model ⇒ Object (readonly)

Returns the value of attribute _model.



6
7
8
 
# File 'lib/z3/model.rb', line 6

def _model
  @_model
end

Instance Method Details

#! ⇒ Object 



56
57
58
59
60
61
 
# File 'lib/z3/model.rb', line 56

def !
  differences = map{|v| v != self[v]}
  # A model with no consts constrains nothing, so there is nothing to differ in
  return Z3.False if differences.empty?
  Z3.Or(*differences)
end

#[](ast) ⇒ Object 



35
36
37
 
# File 'lib/z3/model.rb', line 35

def [](ast)
  model_eval(ast)
end

#consts ⇒ Object 



17
18
19
20
21
 
# 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 ⇒ Object 



47
48
49
50
51
52
53
54
 
# File 'lib/z3/model.rb', line 47

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 ⇒ Object 



43
44
45
 
# File 'lib/z3/model.rb', line 43

def inspect
  to_s
end

#model_eval(ast, model_completion = false) ⇒ Object 



31
32
33
 
# File 'lib/z3/model.rb', line 31

def model_eval(ast, model_completion=false)
  Expr.new_from_pointer(LowLevel.model_eval(self, ast, model_completion))
end

#num_consts ⇒ Object 



13
14
15
 
# File 'lib/z3/model.rb', line 13

def num_consts
  LowLevel.model_get_num_consts(self)
end

#num_funcs ⇒ Object 



27
28
29
 
# File 'lib/z3/model.rb', line 27

def num_funcs
  LowLevel.model_get_num_funcs(self)
end

#num_sorts ⇒ Object 



23
24
25
 
# File 'lib/z3/model.rb', line 23

def num_sorts
  LowLevel.model_get_num_sorts(self)
end

#to_s ⇒ Object 



39
40
41
 
# File 'lib/z3/model.rb', line 39

def to_s
  "Z3::Model<#{ map{|n,v| "#{n}=#{v}"}.join(", ") }>"
end