class UnificationTerm

Public Instance Methods

eql?(uni) click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 29
def eql?(uni)
  return false unless uni.is_a?(UnificationTerm)
  @name == uni.name
end
free_unification_terms() click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 8
def free_unification_terms
  [self]
end
free_variables() click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 4
def free_variables
  []
end
occurs(unification_term) click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 17
def occurs(unification_term)
  eql?(unification_term)
end
replace(old, new) click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 12
def replace(old, new)
  return new if eql?(old)
  self
end
set_instantiation_time(time) click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 21
def set_instantiation_time(time)
  @time = time
end
to_s() click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 25
def to_s
  @name
end
unify(term) click to toggle source
# File lib/rover_prover/language/term/unification_term.rb, line 34
def unify(term)
  return nil if term.occurs(self) || term.time > @time
  { self => term }
end