Class: Predicate
- Defined in:
- lib/rover_prover/language/formula/predicate.rb
Instance Attribute Summary collapse
-
#name ⇒ Object
readonly
Returns the value of attribute name.
-
#terms ⇒ Object
readonly
Returns the value of attribute terms.
Instance Method Summary collapse
- #eql?(exp) ⇒ Boolean
- #free_unification_terms ⇒ Object
- #free_variables ⇒ Object
-
#initialize(name, terms) ⇒ Predicate
constructor
A new instance of Predicate.
- #occurs(unification_term) ⇒ Object
- #replace(old, new) ⇒ Object
- #set_instantiation_time(time) ⇒ Object
- #to_s ⇒ Object
- #unify(term) ⇒ Object
Constructor Details
#initialize(name, terms) ⇒ Predicate
Returns a new instance of Predicate.
6 7 8 9 |
# File 'lib/rover_prover/language/formula/predicate.rb', line 6 def initialize(name, terms) @name = name @terms = terms end |
Instance Attribute Details
#name ⇒ Object (readonly)
Returns the value of attribute name.
4 5 6 |
# File 'lib/rover_prover/language/formula/predicate.rb', line 4 def name @name end |
#terms ⇒ Object (readonly)
Returns the value of attribute terms.
4 5 6 |
# File 'lib/rover_prover/language/formula/predicate.rb', line 4 def terms @terms end |
Instance Method Details
#eql?(exp) ⇒ Boolean
37 38 39 40 41 42 |
# File 'lib/rover_prover/language/formula/predicate.rb', line 37 def eql?(exp) return false unless exp.is_a?(Predicate) return false unless @name == exp.name return false unless @terms.length == exp.terms.length @terms.zip(exp.terms).all? { |t1, t2| t1.eql?(t2) } end |
#free_unification_terms ⇒ Object
15 16 17 |
# File 'lib/rover_prover/language/formula/predicate.rb', line 15 def free_unification_terms @terms.map(&:free_unification_terms).flatten.uniq end |
#free_variables ⇒ Object
11 12 13 |
# File 'lib/rover_prover/language/formula/predicate.rb', line 11 def free_variables @terms.map(&:free_variables).flatten.uniq end |
#occurs(unification_term) ⇒ Object
28 29 30 |
# File 'lib/rover_prover/language/formula/predicate.rb', line 28 def occurs(unification_term) @terms.any? { |term| term.occurs(unification_term) } end |
#replace(old, new) ⇒ Object
19 20 21 22 |
# File 'lib/rover_prover/language/formula/predicate.rb', line 19 def replace(old, new) return new if eql?(old) Predicate.new(@name, @terms.map { |term| term.replace(old, new) }) end |
#set_instantiation_time(time) ⇒ Object
24 25 26 |
# File 'lib/rover_prover/language/formula/predicate.rb', line 24 def set_instantiation_time(time) @terms.each{ |term| term.set_instantiation_time(time) } end |
#to_s ⇒ Object
32 33 34 35 |
# File 'lib/rover_prover/language/formula/predicate.rb', line 32 def to_s terms_s = @terms.empty? ? "" : "(#{@terms.map(&:to_s).join(', ')})" "#{@name}#{terms_s}" end |
#unify(term) ⇒ Object
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 |
# File 'lib/rover_prover/language/formula/predicate.rb', line 44 def unify(term) return term.unify(self) if term.is_a?(UnificationTerm) return nil unless term.is_a?(Predicate) return nil unless @name == term.name 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 |