Class: Z3::Tactic

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

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Methods included from ReferenceCounted

finalizer

Constructor Details

#initialize(_tactic) ⇒ Tactic

Returns a new instance of Tactic.



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

def initialize(_tactic)
  @_tactic = _tactic
  inc_ref! :tactic, _tactic
end

Instance Attribute Details

#_tactic ⇒ Object (readonly)

Returns the value of attribute _tactic.



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

def _tactic
  @_tactic
end

Class Method Details

.cond(probe, tactic1, tactic2) ⇒ Object

Raises:



69
70
71
72
73
74
 
# File 'lib/z3/tactic.rb', line 69

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

.description(name) ⇒ Object

Z3 itself raises on unknown names, as we have no tactic name list to check against



42
43
44
 
# File 'lib/z3/tactic.rb', line 42

def description(name)
  LowLevel.tactic_get_descr(name)
end

.fail ⇒ Object 



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

def fail
  new LowLevel.tactic_fail
end

.fail_if(probe) ⇒ Object

Raises:



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

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 



55
56
57
 
# File 'lib/z3/tactic.rb', line 55

def fail_if_not_decided
  new LowLevel.tactic_fail_if_not_decided
end

.skip ⇒ Object 



59
60
61
 
# File 'lib/z3/tactic.rb', line 59

def skip
  new LowLevel.tactic_skip
end

.when(probe, tactic) ⇒ Object

Raises:



63
64
65
66
67
 
# File 'lib/z3/tactic.rb', line 63

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:



20
21
22
23
 
# File 'lib/z3/tactic.rb', line 20

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 



11
12
13
 
# File 'lib/z3/tactic.rb', line 11

def help
  LowLevel.tactic_get_help(self)
end

#or_else(other) ⇒ Object

Raises:



15
16
17
18
 
# File 'lib/z3/tactic.rb', line 15

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:



25
26
27
28
 
# File 'lib/z3/tactic.rb', line 25

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:



30
31
32
33
 
# File 'lib/z3/tactic.rb', line 30

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:



35
36
37
38
 
# File 'lib/z3/tactic.rb', line 35

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