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