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?
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
cnf()
click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 69 def cnf nnf? ? self : nnf.cnf end
literal?()
click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 20 def literal? @f.atomic_formula? end
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
not?()
click to toggle source
# File lib/dpll_solver/formulas/not.rb, line 33 def not? true end
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