Class: Z3::Probe

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

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(_probe) ⇒ Probe

Returns a new instance of Probe.



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

def initialize(_probe)
  @_probe = _probe
  LowLevel.probe_inc_ref(self)
end

Instance Attribute Details

#_probe ⇒ Object (readonly)

Returns the value of attribute _probe.



3
4
5
 
# File 'lib/z3/probe.rb', line 3

def _probe
  @_probe
end

Class Method Details

.const(num) ⇒ Object

Raises:



58
59
60
61
 
# File 'lib/z3/probe.rb', line 58

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

.named(str) ⇒ Object

Raises:



67
68
69
70
 
# File 'lib/z3/probe.rb', line 67

def named(str)
  raise Z3::Exception, "#{str} not on list of known probes, available: #{names.join(" ")}" unless names.include?(str)
  new LowLevel.mk_probe(str)
end

.names ⇒ Object 



63
64
65
 
# File 'lib/z3/probe.rb', line 63

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

Instance Method Details

#! ⇒ Object 



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

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

#&(other) ⇒ Object

Raises:



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

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

#<(other) ⇒ Object

Raises:



47
48
49
50
 
# File 'lib/z3/probe.rb', line 47

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

#<=(other) ⇒ Object

Raises:



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

def <=(other)
  raise Z3::Exception, "Probe required" unless other.is_a?(Probe)
  Probe.new LowLevel.probe_le(self, other)
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_eq(self, other)
end

#>(other) ⇒ Object

Raises:



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

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

#>=(other) ⇒ Object

Raises:



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

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

#apply(goal) ⇒ Object

Raises:



52
53
54
55
 
# File 'lib/z3/probe.rb', line 52

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

#|(other) ⇒ Object

Raises:



14
15
16
17
 
# File 'lib/z3/probe.rb', line 14

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

#~ ⇒ Object 



19
20
21
 
# File 'lib/z3/probe.rb', line 19

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