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?, 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) ⇒ AndTerm

Returns a new instance of AndTerm.



3
4
5
6
 
# 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
  check_nnf_reduced
end

Instance Method Details

#cnf? ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#nnf? ⇒ Boolean

Returns:

  • (Boolean) 


13
14
15
 
# File 'lib/prop_logic/and_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
37
 
# File 'lib/prop_logic/and_term.rb', line 21

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) 


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

def reduced?
  @is_reduced
end

#to_cnf ⇒ Object 



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

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 



8
9
10
11
 
# File 'lib/prop_logic/and_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 



52
53
54
55
56
57
 
# File 'lib/prop_logic/and_term.rb', line 52

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