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?, generate_cache, 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
6
7
 
# File 'lib/prop_logic/not_term.rb', line 3

def initialize(term)
  @terms = [term].freeze
  @is_nnf = @terms[0].is_a?(Variable)
  @is_reduced = @is_nnf && ! (@terms[0].is_a?(Constant))
end

Instance Method Details

#nnf? ⇒ Boolean

Returns:

  • (Boolean) 


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

def nnf?
  @is_nnf
end

#reduce ⇒ Object 



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

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) 


33
34
35
 
# File 'lib/prop_logic/not_term.rb', line 33

def reduced?
  @is_reduced
end

#to_cnf ⇒ Object 



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

def to_cnf
  if reduced?
    self
  else
    super
  end
end

#to_nnf ⇒ Object 



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

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 



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

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

#tseitin(pool) ⇒ Object 



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

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