Class: Sequent

Inherits:
Object
  • Object
show all
Defined in:
lib/rover_prover/language/sequent.rb

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(left, right, siblings, depth) ⇒ Sequent

Returns a new instance of Sequent.



4
5
6
7
8
9
10
11
12
13
 
# File 'lib/rover_prover/language/sequent.rb', line 4

def initialize(left, right, siblings, depth)
  @left = []
  @right = []
  @left_depth_tbl = {}
  @right_depth_tbl = {}
  left.each { |l| left_add(l) }
  right.each { |l| right_add(l) }
  @siblings = siblings
  @depth = depth
end

Instance Attribute Details

#depth ⇒ Object (readonly)

Returns the value of attribute depth.



3
4
5
 
# File 'lib/rover_prover/language/sequent.rb', line 3

def depth
  @depth
end

#left ⇒ Object (readonly)

Returns the value of attribute left.



3
4
5
 
# File 'lib/rover_prover/language/sequent.rb', line 3

def left
  @left
end

#right ⇒ Object (readonly)

Returns the value of attribute right.



3
4
5
 
# File 'lib/rover_prover/language/sequent.rb', line 3

def right
  @right
end

#siblings ⇒ Object (readonly)

Returns the value of attribute siblings.



3
4
5
 
# File 'lib/rover_prover/language/sequent.rb', line 3

def siblings
  @siblings
end

Instance Method Details

#deepen(enable_siblings: false) ⇒ Object 



15
16
17
18
19
20
21
22
23
24
25
 
# File 'lib/rover_prover/language/sequent.rb', line 15

def deepen(enable_siblings: false)
  new_siblings = @siblings.nil? ? (enable_siblings ? [] : @siblings): @siblings.dup
  new = Sequent.new(@left.dup, @right.dup, new_siblings, @depth + 1)
  @left.each do |formula|
    new.left_set_depth(formula, left_get_depth(formula))
  end
  @right.each do |formula|
    new.right_set_depth(formula, right_get_depth(formula))
  end
  new
end

#eql?(sequent) ⇒ Boolean

Returns:

  • (Boolean) 


113
114
115
116
117
118
 
# File 'lib/rover_prover/language/sequent.rb', line 113

def eql?(sequent)
  include?(@left, sequent.left) &&
  include?(@right, sequent.right) &&
  include?(sequent.left, @left) &&
  include?(sequent.right, @right)
end

#free_unification_terms ⇒ Object 



84
85
86
 
# File 'lib/rover_prover/language/sequent.rb', line 84

def free_unification_terms
  @left.map { |formula| formula.free_unification_terms }.flatten | @right.map { |formula| formula.free_unification_terms}.flatten
end

#free_variables ⇒ Object 



80
81
82
 
# File 'lib/rover_prover/language/sequent.rb', line 80

def free_variables
  @left.map { |formula| formula.free_variables }.flatten | @right.map { |formula| formula.free_variables}.flatten
end

#get_unifiable_pairs ⇒ Object 



99
100
101
102
103
104
105
106
107
 
# File 'lib/rover_prover/language/sequent.rb', line 99

def get_unifiable_pairs
  pairs = []
  @left.each do |formula_a|
    @right.each do |formula_b|
      pairs.push([formula_a, formula_b]) unless formula_a.unify(formula_b).nil?
    end
  end
  pairs
end

#get_variable_name(prefix) ⇒ Object 



88
89
90
91
92
93
94
95
96
97
 
# File 'lib/rover_prover/language/sequent.rb', line 88

def get_variable_name(prefix)
  names = free_variables.map(&:name) | free_unification_terms.map(&:name)
  index = 1
  name = prefix + index.to_s
  while names.include?(name) do
    index += 1
    name = prefix + index.to_s
  end
  name
end

#left_add(l) ⇒ Object 



44
45
46
47
 
# File 'lib/rover_prover/language/sequent.rb', line 44

def left_add(l)
  @left.push(l)
  @left_depth_tbl[l] = 0
end

#left_formula ⇒ Object 



36
37
38
 
# File 'lib/rover_prover/language/sequent.rb', line 36

def left_formula
  @left.reject { |f| f.is_a?(Predicate) }.min_by { |f| left_get_depth(f) }
end

#left_get_depth(l) ⇒ Object 



64
65
66
 
# File 'lib/rover_prover/language/sequent.rb', line 64

def left_get_depth(l)
  @left_depth_tbl[l]
end

#left_remove(l) ⇒ Object 



54
55
56
57
 
# File 'lib/rover_prover/language/sequent.rb', line 54

def left_remove(l)
  @left.delete(l)
  @left_depth_tbl.delete(l)
end

#left_set_depth(l, t) ⇒ Object 



72
73
74
 
# File 'lib/rover_prover/language/sequent.rb', line 72

def left_set_depth(l, t)
  @left_depth_tbl[l] = t
end

#right_add(r) ⇒ Object 



49
50
51
52
 
# File 'lib/rover_prover/language/sequent.rb', line 49

def right_add(r)
  @right.push(r)
  @right_depth_tbl[r] = 0
end

#right_formula ⇒ Object 



40
41
42
 
# File 'lib/rover_prover/language/sequent.rb', line 40

def right_formula
  @right.reject { |f| f.is_a?(Predicate) }.min_by { |f| right_get_depth(f) }
end

#right_get_depth(r) ⇒ Object 



68
69
70
 
# File 'lib/rover_prover/language/sequent.rb', line 68

def right_get_depth(r)
  @right_depth_tbl[r]
end

#right_remove(r) ⇒ Object 



59
60
61
62
 
# File 'lib/rover_prover/language/sequent.rb', line 59

def right_remove(r)
  @right.delete(r)
  @right_depth_tbl.delete(r)
end

#right_set_depth(r, t) ⇒ Object 



76
77
78
 
# File 'lib/rover_prover/language/sequent.rb', line 76

def right_set_depth(r, t)
  @right_depth_tbl[r] = t
end

#set_default_instantiation_time(time) ⇒ Object 



31
32
33
34
 
# File 'lib/rover_prover/language/sequent.rb', line 31

def set_default_instantiation_time(time)
  @left.each { |l| l.set_instantiation_time(time) }
  @right.each { |r| r.set_instantiation_time(time) }
end

#to_s ⇒ Object 



109
110
111
 
# File 'lib/rover_prover/language/sequent.rb', line 109

def to_s
  "#{@left.map(&:to_s).join(', ')} ⊢ #{@right.map(&:to_s).join(', ')}"
end

#trivial? ⇒ Boolean

Returns:

  • (Boolean) 


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

def trivial?
  (@left & @right).length > 0
end