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