Class: Z3::Probe

Inherits:
Object
  • Object
show all
Includes:
ReferenceCounted
Defined in:
lib/z3/probe.rb

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Methods included from ReferenceCounted

finalizer

Constructor Details

#initialize(_probe) ⇒ Probe

Takes either a probe name, or a pointer from the low level API



7
8
9
10
11
12
13
14
15
16
17
18
19
20
 
# File 'lib/z3/probe.rb', line 7

def initialize(_probe)
  case _probe
  when String
    names = Probe.names
    raise Z3::Exception, "#{_probe} not on list of known probes, available: #{names.join(" ")}" unless names.include?(_probe)
    _probe = LowLevel.mk_probe(_probe)
  when FFI::Pointer
    # Nothing to do
  else
    raise Z3::Exception, "Probe name or pointer expected, got #{_probe.class}"
  end
  @_probe = _probe
  inc_ref! :probe, _probe
end

Instance Attribute Details

#_probe ⇒ Object (readonly)

Returns the value of attribute _probe.



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

def _probe
  @_probe
end

Class Method Details

.const(num) ⇒ Object

Raises:



71
72
73
74
 
# File 'lib/z3/probe.rb', line 71

def const(num)
  raise Z3::Exception, "Number required" unless num.is_a?(Numeric)
  new LowLevel.probe_const(num.to_f)
end

.description(name) ⇒ Object

Raises:



80
81
82
83
 
# File 'lib/z3/probe.rb', line 80

def description(name)
  raise Z3::Exception, "#{name} not on list of known probes, available: #{names.join(" ")}" unless names.include?(name)
  LowLevel.probe_get_descr(name)
end

.named(str) ⇒ Object 



85
86
87
 
# File 'lib/z3/probe.rb', line 85

def named(str)
  new str
end

.names ⇒ Object 



76
77
78
 
# File 'lib/z3/probe.rb', line 76

def names
  (0...LowLevel.get_num_probes).map{|i| LowLevel.get_probe_name(i) }
end

Instance Method Details

#! ⇒ Object 



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

def !
  Probe.new LowLevel.probe_not(self)
end

#&(other) ⇒ Object

Raises:



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

def &(other)
  raise Z3::Exception, "Probe required" unless other.is_a?(Probe)
  Probe.new LowLevel.probe_and(self, other)
end

#<(other) ⇒ Object

Raises:



60
61
62
63
 
# File 'lib/z3/probe.rb', line 60

def <(other)
  raise Z3::Exception, "Probe required" unless other.is_a?(Probe)
  Probe.new LowLevel.probe_lt(self, other)
end

#<=(other) ⇒ Object

Raises:



55
56
57
58
 
# File 'lib/z3/probe.rb', line 55

def <=(other)
  raise Z3::Exception, "Probe required" unless other.is_a?(Probe)
  Probe.new LowLevel.probe_le(self, other)
end

#==(other) ⇒ Object

Raises:



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

def ==(other)
  raise Z3::Exception, "Probe required" unless other.is_a?(Probe)
  Probe.new LowLevel.probe_eq(self, other)
end

#>(other) ⇒ Object

Raises:



50
51
52
53
 
# File 'lib/z3/probe.rb', line 50

def >(other)
  raise Z3::Exception, "Probe required" unless other.is_a?(Probe)
  Probe.new LowLevel.probe_gt(self, other)
end

#>=(other) ⇒ Object

Raises:



45
46
47
48
 
# File 'lib/z3/probe.rb', line 45

def >=(other)
  raise Z3::Exception, "Probe required" unless other.is_a?(Probe)
  Probe.new LowLevel.probe_ge(self, other)
end

#apply(goal) ⇒ Object

Raises:



65
66
67
68
 
# File 'lib/z3/probe.rb', line 65

def apply(goal)
  raise Z3::Exception, "Goal required" unless goal.is_a?(Goal)
  LowLevel.probe_apply(self, goal)
end

#|(other) ⇒ Object

Raises:



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

def |(other)
  raise Z3::Exception, "Probe required" unless other.is_a?(Probe)
  Probe.new LowLevel.probe_or(self, other)
end

#~ ⇒ Object 



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

def ~
  Probe.new LowLevel.probe_not(self)
end