class Z3::ApplyResult

What a Tactic made of a Goal: the subgoals it broke that goal into.

The original goal is satisfiable exactly when one of the subgoals is, so no subgoals at all means the tactic decided the goal is unsatisfiable, and a single subgoal which is ‘decided_sat?` means it decided the other way.

Attributes

_apply_result [R]

Public Class Methods

new (_apply_result)

Source

# File lib/z3/apply_result.rb, line 12
def initialize(_apply_result)
  @_apply_result = _apply_result
  inc_ref! :apply_result, _apply_result
end

Public Instance Methods

[] (num)

Source

# File lib/z3/apply_result.rb, line 21
def [](num)
  raise Z3::Exception, "Out of range" unless num.between?(0, size-1)
  Goal.from_pointer(LowLevel.apply_result_get_subgoal(self, num))
end

each () { |self| ... }

Source

# File lib/z3/apply_result.rb, line 26
def each
  return to_enum(:each) unless block_given?
  size.times { |i| yield self[i] }
  self
end

inspect ()

Source

# File lib/z3/apply_result.rb, line 36
def inspect
  "Z3::ApplyResult<#{size} subgoal#{"s" unless size == 1}>"
end

size ()

Source

# File lib/z3/apply_result.rb, line 17
def size
  LowLevel.apply_result_get_num_subgoals(self)
end

to_s ()

Source

# File lib/z3/apply_result.rb, line 32
def to_s
  LowLevel.apply_result_to_string(self)
end