class PropLogic::NotTerm

Public Class Methods

new(term) click to toggle source
# 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

Public Instance Methods

cnf?()
Alias for: reduced?
nnf?() click to toggle source
# File lib/prop_logic/not_term.rb, line 13
def nnf?
  @is_nnf
end
reduce() click to toggle source
# 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?() click to toggle source
# File lib/prop_logic/not_term.rb, line 33
def reduced?
  @is_reduced
end
Also aliased as: cnf?
to_cnf() click to toggle source
Calls superclass method PropLogic::Term#to_cnf
# File lib/prop_logic/not_term.rb, line 50
def to_cnf
  if reduced?
    self
  else
    super
  end
end
to_nnf() click to toggle source
# 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(*) click to toggle source
# File lib/prop_logic/not_term.rb, line 9
def to_s(*)
  "~" + @terms[0].to_s(true)
end
tseitin(pool) click to toggle source
# 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