Class: PropLogic::OrTerm

Inherits:
Term
  • Object
show all
Defined in:
lib/prop_logic/or_term.rb

Instance Attribute Summary

Attributes inherited from Term

#terms

Instance Method Summary collapse

Methods inherited from Term

#and, #assign, #assign_false, #assign_true, #each_sat, #equiv?, get, #initialize_copy, #not, #or, #sat?, #then, #to_nnf, #to_s_in_term, #unsat?, #variables

Methods included from Functions

all_and, all_or, new_variable, sat_loop

Constructor Details

#initialize(*terms) ⇒ OrTerm

Returns a new instance of OrTerm.



3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
 
# File 'lib/prop_logic/or_term.rb', line 3

def initialize(*terms)
  @terms = terms.map{|t| t.is_a?(OrTerm) ? t.terms : t}.flatten.freeze
  @is_nnf = @terms.all?(&:nnf?)
  @is_reduced = @is_nnf && @terms.all? do |term|
    if term.is_a?(Constant) || !(term.reduced?)
      false
    elsif !(term.is_a?(NotTerm))
      true
    else
      # NotTerm
      term.terms[0].is_a?(Variable)
    end
  end
  return unless @is_reduced
  # check duplication of terms
  if @terms.length != @terms.uniq.length
    @is_reduced = false
    return
  end
  # check obvious variables (mark as unreduced)
  # Negated terms (except variables) doesn't come here
  not_terms = @terms.select{ |t| t.is_a?(NotTerm) }
  negated_variales = not_terms.map{|t| t.terms[0]}
  @is_reduced = false unless (negated_variales & @terms).empty?
end

Instance Method Details

#cnf? ⇒ Boolean

Returns:

  • (Boolean) 


59
60
61
62
 
# File 'lib/prop_logic/or_term.rb', line 59

def cnf?
  return false unless reduced?
  ! @terms.any?{ |term| term.is_a?(AndTerm) }
end

#nnf? ⇒ Boolean

Returns:

  • (Boolean) 


34
35
36
 
# File 'lib/prop_logic/or_term.rb', line 34

def nnf?
  @is_nnf
end

#reduce ⇒ Object 



42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
 
# File 'lib/prop_logic/or_term.rb', line 42

def reduce
  return self if reduced?
  reduced_terms = @terms.map(&:reduce).uniq
  reduced_terms.reject!{|term| term.equal?(False)}
  return False if reduced_terms.empty?
  if reduced_terms.any?{|term| term.equal?(True)}
    True
  elsif reduced_terms.length == 1
    reduced_terms[0]
  else
    not_terms = reduced_terms.select{|term| term.is_a?(NotTerm)}
    negated_terms = not_terms.map{|term| term.terms[0]}
    return True unless (negated_terms & reduced_terms).empty?
    Term.get self.class, *reduced_terms
  end
end

#reduced? ⇒ Boolean

Returns:

  • (Boolean) 


38
39
40
 
# File 'lib/prop_logic/or_term.rb', line 38

def reduced?
  @is_reduced
end

#to_cnf ⇒ Object 



64
65
66
67
68
69
70
 
# File 'lib/prop_logic/or_term.rb', line 64

def to_cnf
  return super unless reduced?
  return self if cnf?
  pool = []
  without_pools = tseitin(pool)
  all_and(without_pools, *pool)
end

#to_s(in_term = false) ⇒ Object 



29
30
31
32
 
# File 'lib/prop_logic/or_term.rb', line 29

def to_s(in_term = false)
  str = @terms.map(&:to_s_in_term).join(' | ')
  in_term ? "( #{str} )" : str
end

#tseitin(pool) ⇒ Object 



72
73
74
75
76
77
 
# File 'lib/prop_logic/or_term.rb', line 72

def tseitin(pool)
  val = Variable.new
  terms = @terms.map{|t| t.tseitin(pool)}
  pool << (~val | all_or(*terms))
  val
end