Class: Z3::Tactic

Inherits:
Object
  • Object
show all
Defined in:
lib/z3/tactic.rb

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(_tactic) ⇒ Tactic

Returns a new instance of Tactic.



4
5
6
 
# File 'lib/z3/tactic.rb', line 4

def initialize(_tactic)
  @_tactic = _tactic
end

Instance Attribute Details

#tactic ⇒ Object (readonly)

Returns the value of attribute tactic.



3
4
5
 
# File 'lib/z3/tactic.rb', line 3

def tactic
  @tactic
end

Class Method Details

.cond(probe, tactic1, tactic2) ⇒ Object

Raises:



61
62
63
64
65
66
 
# 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 ⇒ Object 



38
39
40
 
# File 'lib/z3/tactic.rb', line 38

def fail
  new LowLevel.tactic_fail
end

.fail_if(probe) ⇒ Object

Raises:



42
43
44
45
 
# 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 ⇒ Object 



47
48
49
 
# File 'lib/z3/tactic.rb', line 47

def fail_if_not_decided
  new LowLevel.tactic_fail_if_not_decided
end

.skip ⇒ Object 



51
52
53
 
# File 'lib/z3/tactic.rb', line 51

def skip
  new LowLevel.tactic_skip
end

.when(probe, tactic) ⇒ Object

Raises:



55
56
57
58
59
 
# 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

Instance Method Details

#and_then(other) ⇒ Object

Raises:



17
18
19
20
 
# 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 ⇒ Object 



8
9
10
 
# File 'lib/z3/tactic.rb', line 8

def help
  LowLevel.tactic_get_help(self)
end

#or_else(other) ⇒ Object

Raises:



12
13
14
15
 
# 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) ⇒ Object

Raises:



22
23
24
25
 
# 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) ⇒ Object

Raises:



27
28
29
30
 
# 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) ⇒ Object

Raises:



32
33
34
35
 
# 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