Class: PropLogic::AndTerm

Inherits:
Term
  • Object
show all
Defined in:
lib/prop_logic/and_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) ⇒ AndTerm

Returns a new instance of AndTerm.



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
28
 
# File 'lib/prop_logic/and_term.rb', line 3

def initialize(*terms)
  @terms = terms.map{|t| t.is_a?(AndTerm) ? t.terms : t}.flatten.freeze
  @is_nnf = @terms.all?(&:nnf?)
  # term with negative terms are no longer terated as reduced
  @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 contradicted 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) 


61
62
63
64
 
# File 'lib/prop_logic/and_term.rb', line 61

def cnf?
  return false unless reduced?
  @terms.all?(&:cnf?)
end

#nnf? ⇒ Boolean

Returns:

  • (Boolean) 


35
36
37
 
# File 'lib/prop_logic/and_term.rb', line 35

def nnf?
  @is_nnf
end

#reduce ⇒ Object 



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

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

#reduced? ⇒ Boolean

Returns:

  • (Boolean) 


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

def reduced?
  @is_reduced
end

#to_cnf ⇒ Object 



66
67
68
69
70
71
72
 
# File 'lib/prop_logic/and_term.rb', line 66

def to_cnf
  return super unless reduced?
  return self if cnf?
  pool = []
  without_pools = all_and(*@terms.map{|t| t.tseitin(pool)})
  all_and(without_pools, *pool)
end

#to_s(in_term = false) ⇒ Object 



30
31
32
33
 
# File 'lib/prop_logic/and_term.rb', line 30

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

#tseitin(pool) ⇒ Object 



74
75
76
77
78
79
 
# File 'lib/prop_logic/and_term.rb', line 74

def tseitin(pool)
  val = Variable.new
  terms = @terms.map{|t| t.cnf? ? t : t.tseitin(pool)}
  pool.concat terms.map{|t| ~val | t }
  val
end