Class: PropLogic::NotTerm

Inherits:
Term
  • Object
show all
Defined in:
lib/prop_logic/not_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_s_in_term, #unsat?, #variables

Methods included from Functions

all_and, all_or, new_variable, sat_loop

Constructor Details

#initialize(term) ⇒ NotTerm

Returns a new instance of NotTerm.



3
4
5
 
# File 'lib/prop_logic/not_term.rb', line 3

def initialize(term)
  @terms = [term].freeze
end

Instance Method Details

#nnf? ⇒ Boolean

Returns:

  • (Boolean) 


11
12
13
 
# File 'lib/prop_logic/not_term.rb', line 11

def nnf?
  @terms[0].is_a?(Variable)
end

#reduce ⇒ Object 



35
36
37
38
39
40
41
42
43
44
45
46
 
# File 'lib/prop_logic/not_term.rb', line 35

def reduce
  return self if reduced?
  reduced_term = @terms[0].reduce
  case reduced_term
  when TrueConstant
    False
  when FalseConstant
    True
  else
    (~reduced_term).to_nnf
  end
end

#reduced? ⇒ Boolean Also known as: cnf?

Returns:

  • (Boolean) 


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

def reduced?
  nnf? && ! (@terms[0].is_a?(Constant))
end

#to_cnf ⇒ Object 



48
49
50
51
52
53
54
 
# File 'lib/prop_logic/not_term.rb', line 48

def to_cnf
  if reduced?
    self
  else
    super
  end
end

#to_nnf ⇒ Object 



15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
 
# File 'lib/prop_logic/not_term.rb', line 15

def to_nnf
  term = @terms[0]
  case term
  when NotTerm
    term.terms[0].to_nnf
  when Variable
    self
  when ThenTerm
    (~(term.to_nnf)).to_nnf
  when AndTerm
    all_or(*term.terms.map{|t| (~t).to_nnf})
  when OrTerm
    all_and(*term.terms.map{|t| (~t).to_nnf})
  end
end

#to_s ⇒ Object 



7
8
9
 
# File 'lib/prop_logic/not_term.rb', line 7

def to_s(*)
  "~" + @terms[0].to_s(true)
end

#tseitin(pool) ⇒ Object 



56
57
58
59
60
61
62
63
64
 
# File 'lib/prop_logic/not_term.rb', line 56

def tseitin(pool)
  if nnf?
    self
  elsif @terms[0].is_a?(NotTerm) && @terms[0].terms[0].is_a(Variable)
    @terms[0].terms[0]
  else
    raise 'Non-NNF terms cannot be converted to Tseitin form.' + self.to_s
  end
end