class Implies
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/implies.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/implies.rb, line 37 def eql?(exp) return false unless exp.is_a?(Implies) @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/implies.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/implies.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/implies.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/implies.rb, line 19 def replace(old, new) return new if eql?(old) Implies.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/implies.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/implies.rb, line 33 def to_s "(#{@formula_a.to_s} -> #{@formula_b.to_s})" end