class Z3::Probe
Attributes
_probe[R]
Public Class Methods
const(num)
click to toggle source
# 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)
click to toggle source
# 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()
click to toggle source
# File lib/z3/probe.rb, line 63 def names (0...LowLevel.get_num_probes).map{|i| LowLevel.get_probe_name(i) } end
new(_probe)
click to toggle source
# File lib/z3/probe.rb, line 4 def initialize(_probe) @_probe = _probe LowLevel.probe_inc_ref(self) end
Public Instance Methods
!()
click to toggle source
# File lib/z3/probe.rb, line 23 def ! Probe.new LowLevel.probe_not(self) end
&(other)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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
~()
click to toggle source
# File lib/z3/probe.rb, line 19 def ~ Probe.new LowLevel.probe_not(self) end