Class: Z3::Model

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

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(_model) ⇒ Model

Returns a new instance of Model.



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

def initialize(_model)
  @_model = _model
end

Instance Attribute Details

#_model ⇒ Object (readonly)

Returns the value of attribute _model.



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

def _model
  @_model
end

Instance Method Details

#! ⇒ Object 



53
54
55
56
57
 
# File 'lib/z3/model.rb', line 53

def !
  Z3.Or(
    *map{|v| v != self[v]}
  )
end

#[](ast) ⇒ Object 



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

def [](ast)
  model_eval(ast)
end

#consts ⇒ Object 



14
15
16
17
18
 
# 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 ⇒ Object 



44
45
46
47
48
49
50
51
 
# 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 ⇒ Object 



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

def inspect
  to_s
end

#model_eval(ast, model_completion = false) ⇒ Object 



28
29
30
 
# 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 ⇒ Object 



10
11
12
 
# File 'lib/z3/model.rb', line 10

def num_consts
  LowLevel.model_get_num_consts(self)
end

#num_funcs ⇒ Object 



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

def num_funcs
  LowLevel.model_get_num_funcs(self)
end

#num_sorts ⇒ Object 



20
21
22
 
# File 'lib/z3/model.rb', line 20

def num_sorts
  LowLevel.model_get_num_sorts(self)
end

#to_s ⇒ Object 



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

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