Class: ThereExists

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

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from Expression

#unify

Constructor Details

#initialize(variable, formula) ⇒ ThereExists

Returns a new instance of ThereExists.



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

def initialize(variable, formula)
  @variable = variable
  @formula = formula
end

Instance Attribute Details

#formula ⇒ Object (readonly)

Returns the value of attribute formula.



2
3
4
 
# File 'lib/rover_prover/language/formula/there_exists.rb', line 2

def formula
  @formula
end

#variable ⇒ Object (readonly)

Returns the value of attribute variable.



2
3
4
 
# File 'lib/rover_prover/language/formula/there_exists.rb', line 2

def variable
  @variable
end

Instance Method Details

#eql?(exp) ⇒ Boolean

Returns:

  • (Boolean) 


38
39
40
41
 
# File 'lib/rover_prover/language/formula/there_exists.rb', line 38

def eql?(exp)
  return false unless exp.is_a?(ThereExists)
  @variable.eql?(exp.variable) && @formula.eql?(exp.formula)
end

#free_unification_terms ⇒ Object 



13
14
15
 
# File 'lib/rover_prover/language/formula/there_exists.rb', line 13

def free_unification_terms
  @formula.free_unification_terms
end

#free_variables ⇒ Object 



9
10
11
 
# File 'lib/rover_prover/language/formula/there_exists.rb', line 9

def free_variables
  @formula.free_variables.reject{ |var| var.eql?(@variable) }
end

#occurs(unification_term) ⇒ Object 



25
26
27
 
# File 'lib/rover_prover/language/formula/there_exists.rb', line 25

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

#replace(old, new) ⇒ Object 



17
18
19
20
21
22
23
 
# File 'lib/rover_prover/language/formula/there_exists.rb', line 17

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

#set_instantiation_time(time) ⇒ Object 



29
30
31
32
 
# File 'lib/rover_prover/language/formula/there_exists.rb', line 29

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

#to_s ⇒ Object 



34
35
36
 
# File 'lib/rover_prover/language/formula/there_exists.rb', line 34

def to_s
  "(∃#{@variable.to_s}. #{@formula.to_s})"
end