class DpllSolver::Formulas::Not

Attributes

f[RW]

Public Class Methods

new(f) click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 6
def initialize(f)
  @f = f
end

Public Instance Methods

==(other) click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 10
def ==(other)
  other.class == self.class && other.f == @f
end
Also aliased as: eql?
and?()
Alias for: verum?
apply_DeMorgan() click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 73
def apply_DeMorgan
  if @f.and?
    return DpllSolver::Formulas::Or.new(self.class.new(@f.f1), self.class.new(@f.f2))
  elsif @f.or?
    return DpllSolver::Formulas::And.new(self.class.new(@f.f1), self.class.new(@f.f2))
  else
    raise ArgumentError, 'DeMorgan can not be applied unless @f is either AND or OR'
  end
end
atomic_formula?() click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 24
def atomic_formula?
  false
end
clause?()
Alias for: literal?
cnf() click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 69
def cnf
  nnf? ? self : nnf.cnf
end
cnf?()
Alias for: nnf?
dnf?()
Alias for: nnf?
eql?(other)
Alias for: ==
falsum?()
Alias for: verum?
literal?() click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 20
def literal?
  @f.atomic_formula?
end
Also aliased as: nnf?, clause?, min_term?
min_term?()
Alias for: literal?
nnf() click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 59
def nnf
  if @f.and? || @f.or?
    return apply_DeMorgan.nnf
  elsif @f.not?
    return @f.f.nnf
  else
    return self
  end
end
nnf?()
Also aliased as: cnf?, dnf?
Alias for: literal?
not?() click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 33
def not?
  true
end
or?()
Alias for: verum?
simplify() click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 45
def simplify
  result = @f.simplify
  if result.not?
    result = result.f.simplify
  elsif result.verum?
    result = DpllSolver::Formulas::Falsum
  elsif result.falsum?
    result = DpllSolver::Formulas::Verum
  else
    result = self.class.new(result)
  end
  result
end
to_s() click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 16
def to_s
  "-#{@f.to_s}"
end
variable?()
Alias for: verum?
verum?() click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 37
def verum?
  false
end
Also aliased as: falsum?, and?, or?, variable?