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
eql?(other)
Alias for: ==
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