Class: Or

Inherits:
Formula show all
Defined in:
lib/rover_prover/language/formula/or.rb

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from Expression

#unify

Constructor Details

#initialize(formula_a, formula_b) ⇒ Or

Returns a new instance of Or.



6
7
8
9
 
# File 'lib/rover_prover/language/formula/or.rb', line 6

def initialize(formula_a, formula_b)
  @formula_a = formula_a
  @formula_b = formula_b
end

Instance Attribute Details

#formula_a ⇒ Object (readonly)

Returns the value of attribute formula_a.



4
5
6
 
# File 'lib/rover_prover/language/formula/or.rb', line 4

def formula_a
  @formula_a
end

#formula_b ⇒ Object (readonly)

Returns the value of attribute formula_b.



4
5
6
 
# File 'lib/rover_prover/language/formula/or.rb', line 4

def formula_b
  @formula_b
end

Instance Method Details

#eql?(exp) ⇒ Boolean

Returns:

  • (Boolean) 


37
38
39
40
 
# File 'lib/rover_prover/language/formula/or.rb', line 37

def eql?(exp)
  return false unless exp.is_a?(Or)
  @formula_a.eql?(exp.formula_a) && @formula_b.eql?(exp.formula_b)
end

#free_unification_terms ⇒ Object 



15
16
17
 
# File 'lib/rover_prover/language/formula/or.rb', line 15

def free_unification_terms
  @formula_a.free_unification_terms | @formula_b.free_unification_terms
end

#free_variables ⇒ Object 



11
12
13
 
# File 'lib/rover_prover/language/formula/or.rb', line 11

def free_variables
  @formula_a.free_variables | @formula_b.free_variables
end

#occurs(unification_term) ⇒ Object 



24
25
26
 
# File 'lib/rover_prover/language/formula/or.rb', line 24

def occurs(unification_term)
  @formula_a.occurs(unification_term) || @formula_b.occurs(unification_term)
end

#replace(old, new) ⇒ Object 



19
20
21
22
 
# File 'lib/rover_prover/language/formula/or.rb', line 19

def replace(old, new)
  return new if eql?(old)
  Or.new(@formula_a.replace(old, new), @formula_b.replace(old, new))
end

#set_instantiation_time(time) ⇒ Object 



28
29
30
31
 
# File 'lib/rover_prover/language/formula/or.rb', line 28

def set_instantiation_time(time)
  @formula_a.set_instantiation_time(time)
  @formula_b.set_instantiation_time(time)
end

#to_s ⇒ Object 



33
34
35
 
# File 'lib/rover_prover/language/formula/or.rb', line 33

def to_s
  "(#{@formula_a.to_s} ∨ #{@formula_b.to_s})"
end