class Z3::Tactic

# File lib/z3/tactic.rb, line 122
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 80
def description(name)
  raise Z3::Exception, "#{name} not on list of known tactics, available: #{names.join(" ")}" unless names.include?(name)
  LowLevel.tactic_get_descr(name)
end

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

# File lib/z3/tactic.rb, line 103
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 108
def fail_if_not_decided
  new LowLevel.tactic_fail_if_not_decided
end

# File lib/z3/tactic.rb, line 85
def named(str)
  new str
end

# File lib/z3/tactic.rb, line 76
def names
  (0...LowLevel.get_num_tactics).map{|i| LowLevel.get_tactic_name(i) }
end

# File lib/z3/tactic.rb, line 7
def initialize(_tactic)
  case _tactic
  when String
    names = Tactic.names
    raise Z3::Exception, "#{_tactic} not on list of known tactics, available: #{names.join(" ")}" unless names.include?(_tactic)
    _tactic = LowLevel.mk_tactic(_tactic)
  when FFI::Pointer
    # Nothing to do
  else
    raise Z3::Exception, "Tactic name or pointer expected, got #{_tactic.class}"
  end
  @_tactic = _tactic
  inc_ref! :tactic, _tactic
end

# File lib/z3/tactic.rb, line 91
def par_or(*tactics)
  raise Z3::Exception, "At least one tactic required" if tactics.empty?
  tactics.each do |tactic|
    raise Z3::Exception, "Tactic required" unless tactic.is_a?(Tactic)
  end
  new LowLevel.tactic_par_or(tactics)
end

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

# File lib/z3/tactic.rb, line 116
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 55
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 28
def apply(goal, params = {})
  raise Z3::Exception, "Goal required" unless goal.is_a?(Goal)
  # Skipped for the common no-parameters case, as building a Params has to build
  # the parameter descriptions to check against
  return ApplyResult.new(LowLevel.tactic_apply(self, goal)) if params == {}
  params = Params.new(params, param_descrs) unless params.is_a?(Params)
  ApplyResult.new(LowLevel.tactic_apply_ex(self, goal, params))
end

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

# File lib/z3/tactic.rb, line 50
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 60
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 39
def param_descrs
  ParamDescrs.new(LowLevel.tactic_get_param_descrs(self))
end

# File lib/z3/tactic.rb, line 65
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 70
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

# File lib/z3/tactic.rb, line 45
def using_params(params)
  params = Params.new(params, param_descrs) unless params.is_a?(Params)
  Tactic.new LowLevel.tactic_using_params(self, params)
end