class Sequent

Attributes

depth[R]
left[R]
right[R]
siblings[R]

Public Class Methods

new(left, right, siblings, depth) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 4
def initialize(left, right, siblings, depth)
  @left = []
  @right = []
  @left_depth_tbl = {}
  @right_depth_tbl = {}
  left.each { |l| left_add(l) }
  right.each { |l| right_add(l) }
  @siblings = siblings
  @depth = depth
end

Public Instance Methods

deepen(enable_siblings: false) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 15
def deepen(enable_siblings: false)
  new_siblings = @siblings.nil? ? (enable_siblings ? [] : @siblings): @siblings.dup
  new = Sequent.new(@left.dup, @right.dup, new_siblings, @depth + 1)
  @left.each do |formula|
    new.left_set_depth(formula, left_get_depth(formula))
  end
  @right.each do |formula|
    new.right_set_depth(formula, right_get_depth(formula))
  end
  new
end
eql?(sequent) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 113
def eql?(sequent)
  include?(@left, sequent.left) &&
  include?(@right, sequent.right) &&
  include?(sequent.left, @left) &&
  include?(sequent.right, @right)
end
free_unification_terms() click to toggle source
# File lib/rover_prover/language/sequent.rb, line 84
def free_unification_terms
  @left.map { |formula| formula.free_unification_terms }.flatten | @right.map { |formula| formula.free_unification_terms}.flatten
end
free_variables() click to toggle source
# File lib/rover_prover/language/sequent.rb, line 80
def free_variables
  @left.map { |formula| formula.free_variables }.flatten | @right.map { |formula| formula.free_variables}.flatten
end
get_unifiable_pairs() click to toggle source
# File lib/rover_prover/language/sequent.rb, line 99
def get_unifiable_pairs
  pairs = []
  @left.each do |formula_a|
    @right.each do |formula_b|
      pairs.push([formula_a, formula_b]) unless formula_a.unify(formula_b).nil?
    end
  end
  pairs
end
get_variable_name(prefix) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 88
def get_variable_name(prefix)
  names = free_variables.map(&:name) | free_unification_terms.map(&:name)
  index = 1
  name = prefix + index.to_s
  while names.include?(name) do
    index += 1
    name = prefix + index.to_s
  end
  name
end
left_add(l) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 44
def left_add(l)
  @left.push(l)
  @left_depth_tbl[l] = 0
end
left_formula() click to toggle source
# File lib/rover_prover/language/sequent.rb, line 36
def left_formula
  @left.reject { |f| f.is_a?(Predicate) }.min_by { |f| left_get_depth(f) }
end
left_get_depth(l) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 64
def left_get_depth(l)
  @left_depth_tbl[l]
end
left_remove(l) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 54
def left_remove(l)
  @left.delete(l)
  @left_depth_tbl.delete(l)
end
left_set_depth(l, t) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 72
def left_set_depth(l, t)
  @left_depth_tbl[l] = t
end
right_add(r) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 49
def right_add(r)
  @right.push(r)
  @right_depth_tbl[r] = 0
end
right_formula() click to toggle source
# File lib/rover_prover/language/sequent.rb, line 40
def right_formula
  @right.reject { |f| f.is_a?(Predicate) }.min_by { |f| right_get_depth(f) }
end
right_get_depth(r) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 68
def right_get_depth(r)
  @right_depth_tbl[r]
end
right_remove(r) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 59
def right_remove(r)
  @right.delete(r)
  @right_depth_tbl.delete(r)
end
right_set_depth(r, t) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 76
def right_set_depth(r, t)
  @right_depth_tbl[r] = t
end
set_default_instantiation_time(time) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 31
def set_default_instantiation_time(time)
  @left.each { |l| l.set_instantiation_time(time) }
  @right.each { |r| r.set_instantiation_time(time) }
end
to_s() click to toggle source
# File lib/rover_prover/language/sequent.rb, line 109
def to_s
  "#{@left.map(&:to_s).join(', ')} ⊢ #{@right.map(&:to_s).join(', ')}"
end
trivial?() click to toggle source
# File lib/rover_prover/language/sequent.rb, line 27
def trivial?
  (@left & @right).length > 0
end

Private Instance Methods

include?(formulas1, formulas2) click to toggle source
# File lib/rover_prover/language/sequent.rb, line 121
def include?(formulas1, formulas2)
  formulas2.all? do |f2|
    formulas1.any? { |f1| f1.eql?(f2) }
  end
end