class BinaryFormula
Attributes
f1[RW]
f2[RW]
Public Class Methods
new(f1, f2)
click to toggle source
# File lib/dpll_solver/formulas/binary_formula.rb, line 3 def initialize(f1, f2) @f1 = f1 @f2 = f2 end
Public Instance Methods
==(other)
click to toggle source
syntactic equivalenz
# File lib/dpll_solver/formulas/binary_formula.rb, line 8 def ==(other) other.class == self.class && other.f1 == @f1 && other.f2 == @f2 end
Also aliased as: eql?
atomic_formula?()
click to toggle source
# File lib/dpll_solver/formulas/binary_formula.rb, line 17 def atomic_formula? false end
dnf?()
click to toggle source
# File lib/dpll_solver/formulas/binary_formula.rb, line 25 def dnf? @f1.dnf? && @f2.dnf? end
literal?()
click to toggle source
# File lib/dpll_solver/formulas/binary_formula.rb, line 13 def literal? false end
nnf()
click to toggle source
# File lib/dpll_solver/formulas/binary_formula.rb, line 29 def nnf self.class.new(@f1.nnf, @f2.nnf) end
nnf?()
click to toggle source
# File lib/dpll_solver/formulas/binary_formula.rb, line 21 def nnf? @f1.nnf? && @f2.nnf? end