class And

Attributes

formula_a[R]

formula_b[R]

Public Class Methods

new(formula_a, formula_b) click to toggle source

# File lib/rover_prover/language/formula/and.rb, line 6
def initialize(formula_a, formula_b)
  @formula_a = formula_a
  @formula_b = formula_b
end

Public Instance Methods

eql?(exp) click to toggle source

# File lib/rover_prover/language/formula/and.rb, line 37
def eql?(exp)
  return false unless exp.is_a?(And)
  @formula_a.eql?(exp.formula_a) && @formula_b.eql?(exp.formula_b)
end

free_unification_terms() click to toggle source

# File lib/rover_prover/language/formula/and.rb, line 15
def free_unification_terms
  @formula_a.free_unification_terms | @formula_b.free_unification_terms
end

free_variables() click to toggle source

# File lib/rover_prover/language/formula/and.rb, line 11
def free_variables
  @formula_a.free_variables | @formula_b.free_variables
end

occurs(unification_term) click to toggle source

# File lib/rover_prover/language/formula/and.rb, line 24
def occurs(unification_term)
  @formula_a.occurs(unification_term) || @formula_b.occurs(unification_term)
end

replace(old, new) click to toggle source

# File lib/rover_prover/language/formula/and.rb, line 19
def replace(old, new)
  return new if eql?(old)
  And.new(@formula_a.replace(old, new), @formula_b.replace(old, new))
end

set_instantiation_time(time) click to toggle source

# File lib/rover_prover/language/formula/and.rb, line 28
def set_instantiation_time(time)
  @formula_a.set_instantiation_time(time)
  @formula_b.set_instantiation_time(time)
end

to_s() click to toggle source

# File lib/rover_prover/language/formula/and.rb, line 33
def to_s
  "(#{@formula_a.to_s} ∧ #{@formula_b.to_s})"
end