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