class Z3::Probe

# 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

# 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

# File lib/z3/probe.rb, line 63
def names
  (0...LowLevel.get_num_probes).map{|i| LowLevel.get_probe_name(i) }
end

# File lib/z3/probe.rb, line 4
def initialize(_probe)
  @_probe = _probe
  LowLevel.probe_inc_ref(self)
end

# File lib/z3/probe.rb, line 23
def !
  Probe.new LowLevel.probe_not(self)
end

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# File lib/z3/probe.rb, line 19
def ~
  Probe.new LowLevel.probe_not(self)
end

# 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