class Z3::Tactic

# File lib/z3/tactic.rb, line 61
def cond(probe, tactic1, tactic2)
  raise Z3::Exception, "Prope required" unless probe.is_a?(Probe)
  raise Z3::Exception, "Tactic required" unless tactic1.is_a?(Tactic)
  raise Z3::Exception, "Tactic required" unless tactic2.is_a?(Tactic)
  new LowLevel.tactic_cond(probe, tactic1, tactic2)
end

# File lib/z3/tactic.rb, line 38
def fail
  new LowLevel.tactic_fail
end

# File lib/z3/tactic.rb, line 42
def fail_if(probe)
  raise Z3::Exception, "Prope required" unless probe.is_a?(Probe)
  new LowLevel.tactic_fail_if(probe)
end

# File lib/z3/tactic.rb, line 47
def fail_if_not_decided
  new LowLevel.tactic_fail_if_not_decided
end

# File lib/z3/tactic.rb, line 4
def initialize(_tactic)
  @_tactic = _tactic
end

# File lib/z3/tactic.rb, line 51
def skip
  new LowLevel.tactic_skip
end

# File lib/z3/tactic.rb, line 55
def when(probe, tactic)
  raise Z3::Exception, "Prope required" unless probe.is_a?(Probe)
  raise Z3::Exception, "Tactic required" unless tactic.is_a?(Tactic)
  new LowLevel.tactic_when(probe, tactic)
end

# File lib/z3/tactic.rb, line 17
def and_then(other)
  raise Z3::Exception, "Tactic required" unless other.is_a?(Tactic)
  Tactic.new LowLevel.tactic_and_then(self, other)
end

# File lib/z3/tactic.rb, line 8
def help
  LowLevel.tactic_get_help(self)
end

# File lib/z3/tactic.rb, line 12
def or_else(other)
  raise Z3::Exception, "Tactic required" unless other.is_a?(Tactic)
  Tactic.new LowLevel.tactic_or_else(self, other)
end

# File lib/z3/tactic.rb, line 22
def parallel_and_then(other)
  raise Z3::Exception, "Tactic required" unless other.is_a?(Tactic)
  Tactic.new LowLevel.tactic_par_and_then(self, other)
end

# File lib/z3/tactic.rb, line 27
def repeat(num)
  raise Z3::Exception, "Nonnegative Integer required" unless num.is_a?(Integer) and num >= 0
  Tactic.new LowLevel.tactic_repeat(self, num)
end

# File lib/z3/tactic.rb, line 32
def try_for(time_ms)
  raise Z3::Exception, "Nonnegative Integer required" unless time_ms.is_a?(Integer) and time_ms >= 0
  Tactic.new LowLevel.tactic_try_for(self, time_ms)
end