class Predicate
Attributes
name[R]
terms[R]
Public Class Methods
new(name, terms)
click to toggle source
# File lib/rover_prover/language/formula/predicate.rb, line 6 def initialize(name, terms) @name = name @terms = terms end
Public Instance Methods
eql?(exp)
click to toggle source
# 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()
click to toggle source
# File lib/rover_prover/language/formula/predicate.rb, line 15 def free_unification_terms @terms.map(&:free_unification_terms).flatten.uniq end
free_variables()
click to toggle source
# File lib/rover_prover/language/formula/predicate.rb, line 11 def free_variables @terms.map(&:free_variables).flatten.uniq end
occurs(unification_term)
click to toggle source
# 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)
click to toggle source
# 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)
click to toggle source
# 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()
click to toggle source
# 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)
click to toggle source
# 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