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?, generate_cache, 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
 
# 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
  check_nnf_reduced
end

Instance Method Details

#cnf? ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#nnf? ⇒ Boolean

Returns:

  • (Boolean) 


13
14
15
 
# File 'lib/prop_logic/or_term.rb', line 13

def nnf?
  @is_nnf
end

#reduce ⇒ Object 



21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
 
# File 'lib/prop_logic/or_term.rb', line 21

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) 


17
18
19
 
# File 'lib/prop_logic/or_term.rb', line 17

def reduced?
  @is_reduced
end

#to_cnf ⇒ Object 



43
44
45
46
47
48
49
 
# File 'lib/prop_logic/or_term.rb', line 43

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 



8
9
10
11
 
# File 'lib/prop_logic/or_term.rb', line 8

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

#tseitin(pool) ⇒ Object 



51
52
53
54
55
56
 
# File 'lib/prop_logic/or_term.rb', line 51

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