Class: UnificationTerm

Inherits:
Term
  • Object
show all
Defined in:
lib/rover_prover/language/term/unification_term.rb

Constant Summary

Constants inherited from Term

Term::TIME_DEFAULT

Instance Attribute Summary

Attributes inherited from Term

#name, #time

Instance Method Summary collapse

Methods inherited from Term

#initialize

Constructor Details

This class inherits a constructor from Term

Instance Method Details

#eql?(uni) ⇒ Boolean

Returns:

  • (Boolean)


29
30
31
32
# 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_termsObject



8
9
10
# File 'lib/rover_prover/language/term/unification_term.rb', line 8

def free_unification_terms
  [self]
end

#free_variablesObject



4
5
6
# File 'lib/rover_prover/language/term/unification_term.rb', line 4

def free_variables
  []
end

#occurs(unification_term) ⇒ Object



17
18
19
# File 'lib/rover_prover/language/term/unification_term.rb', line 17

def occurs(unification_term)
  eql?(unification_term)
end

#replace(old, new) ⇒ Object



12
13
14
15
# 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) ⇒ Object



21
22
23
# File 'lib/rover_prover/language/term/unification_term.rb', line 21

def set_instantiation_time(time)
  @time = time
end

#to_sObject



25
26
27
# File 'lib/rover_prover/language/term/unification_term.rb', line 25

def to_s
  @name
end

#unify(term) ⇒ Object



34
35
36
37
# 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