Class: Not

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

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from Expression

#unify

Constructor Details

#initialize(formula) ⇒ Not

Returns a new instance of Not.



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

def initialize(formula)
  @formula = formula
end

Instance Attribute Details

#formula ⇒ Object (readonly)

Returns the value of attribute formula.



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

def formula
  @formula
end

Instance Method Details

#eql?(exp) ⇒ Boolean

Returns:

  • (Boolean) 


35
36
37
38
 
# File 'lib/rover_prover/language/formula/not.rb', line 35

def eql?(exp)
  return false unless exp.is_a?(Not)
  @formula.eql?(exp.formula)
end

#free_unification_terms ⇒ Object 



14
15
16
 
# File 'lib/rover_prover/language/formula/not.rb', line 14

def free_unification_terms
  @formula.free_unification_terms
end

#free_variables ⇒ Object 



10
11
12
 
# File 'lib/rover_prover/language/formula/not.rb', line 10

def free_variables
  @formula.free_variables
end

#occurs(unification_term) ⇒ Object 



27
28
29
 
# File 'lib/rover_prover/language/formula/not.rb', line 27

def occurs(unification_term)
  @formula.occurs(unification_term)
end

#replace(old, new) ⇒ Object 



18
19
20
21
 
# File 'lib/rover_prover/language/formula/not.rb', line 18

def replace(old, new)
  return new if eql?(old)
  Not.new(@formula.replace(old, new))
end

#set_instantiation_time(time) ⇒ Object 



23
24
25
 
# File 'lib/rover_prover/language/formula/not.rb', line 23

def set_instantiation_time(time)
  @formula.set_instantiation_time(time)
end

#to_s ⇒ Object 



31
32
33
 
# File 'lib/rover_prover/language/formula/not.rb', line 31

def to_s
  "¬#{@formula.to_s}"
end