Class: Function

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

Constant Summary

Constants inherited from Term

Term::TIME_DEFAULT

Instance Attribute Summary collapse

Attributes inherited from Term

#name, #time

Instance Method Summary collapse

Constructor Details

#initialize(name, terms) ⇒ Function

Returns a new instance of Function.



5
6
7
8
 
# File 'lib/rover_prover/language/term/function.rb', line 5

def initialize(name, terms)
  super(name)
  @terms = terms
end

Instance Attribute Details

#terms ⇒ Object (readonly)

Returns the value of attribute terms.



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

def terms
  @terms
end

Instance Method Details

#eql?(function) ⇒ Boolean

Returns:

  • (Boolean) 


33
34
35
36
37
38
 
# File 'lib/rover_prover/language/term/function.rb', line 33

def eql?(function)
  return false unless function.is_a?(Function)
  return false unless @name == function.name
  return false unless @terms.length == function.terms.length
  @terms.zip(function.terms).all? { |t1, t2| t1.eql?(t2) }
end

#free_unification_terms ⇒ Object 



14
15
16
 
# File 'lib/rover_prover/language/term/function.rb', line 14

def free_unification_terms
  @terms.map(&:free_unification_terms).flatten.uniq
end

#free_variables ⇒ Object 



10
11
12
 
# File 'lib/rover_prover/language/term/function.rb', line 10

def free_variables
  @terms.map(&:free_variables).flatten.uniq
end

#occurs(unification_term) ⇒ Object 



28
29
30
 
# File 'lib/rover_prover/language/term/function.rb', line 28

def occurs(unification_term)
  @terms.any? { |term| term.occurs(unification_term) }
end

#replace(old, new) ⇒ Object 



18
19
20
21
 
# File 'lib/rover_prover/language/term/function.rb', line 18

def replace(old, new)
  return new if eql?(old)
  Function.new(@name, @terms.map { |term| term.replace(old, new) })
end

#set_instantiation_time(time) ⇒ Object 



23
24
25
26
 
# File 'lib/rover_prover/language/term/function.rb', line 23

def set_instantiation_time(time)
  @time = time
  @terms.each{ |term| term.set_instantiation_time(time) }
end

#to_s ⇒ Object 



40
41
42
43
 
# File 'lib/rover_prover/language/term/function.rb', line 40

def to_s
  terms_s = @terms.empty? ? "" : "(#{@terms.map(&:to_s).join(', ')})"
  "#{@name}#{terms_s}"
end

#unify(term) ⇒ Object 



45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
 
# File 'lib/rover_prover/language/term/function.rb', line 45

def unify(term)
  return term.unify(self) if term.is_a?(UnificationTerm)
  return nil unless term.is_a?(Function)
  return nil unless @terms.length == term.terms.length
  term_pair = @terms.zip(term.terms)
  subst = {}

  term_pair.each do |term_a, term_b|
    subst.each do |k, v| 
      term_a = term_a.replace(k, v)
      term_b = term_b.replace(k, v)
    end
    sub = term_a.unify(term_b)
    return nil if sub == nil
    subst.merge!(sub)
  end
  subst
end