class Z3::Tactic

Attributes

tactic[R]

Public Class Methods

cond(probe, tactic1, tactic2) click to toggle source
# 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
fail() click to toggle source
# File lib/z3/tactic.rb, line 38
def fail
  new LowLevel.tactic_fail
end
fail_if(probe) click to toggle source
# 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
fail_if_not_decided() click to toggle source
# File lib/z3/tactic.rb, line 47
def fail_if_not_decided
  new LowLevel.tactic_fail_if_not_decided
end
new(_tactic) click to toggle source
# File lib/z3/tactic.rb, line 4
def initialize(_tactic)
  @_tactic = _tactic
end
skip() click to toggle source
# File lib/z3/tactic.rb, line 51
def skip
  new LowLevel.tactic_skip
end
when(probe, tactic) click to toggle source
# 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

Public Instance Methods

and_then(other) click to toggle source
# 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
help() click to toggle source
# File lib/z3/tactic.rb, line 8
def help
  LowLevel.tactic_get_help(self)
end
or_else(other) click to toggle source
# 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
parallel_and_then(other) click to toggle source
# 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
repeat(num) click to toggle source
# 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
try_for(time_ms) click to toggle source
# 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