class DpllSolver::Formulas::Or

Public Instance Methods

and?()
Alias for: verum?
clause?() click to toggle source
# File lib/dpll_solver/formulas/or.rb, line 8
def clause?
  @f1.clause? && @f2.clause?
end
Also aliased as: cnf?
cnf() click to toggle source
# File lib/dpll_solver/formulas/or.rb, line 46
def cnf
  if cnf?
    return self
  elsif nnf?
    if @f1.and?
      return DpllSolver::Formulas::And.new(self.class.new(@f1.f1, @f2).cnf, self.class.new(@f1.f2, @f2).cnf)
    elsif @f2.and?
      return DpllSolver::Formulas::And.new(self.class.new(@f1, @f2.f1).cnf, self.class.new(@f1, @f2.f2).cnf)
    else
      return self.class.new(@f1.cnf, @f2.cnf).cnf
    end
  else
    return nnf.cnf
  end
end
cnf?()
Alias for: clause?
falsum?()
Alias for: verum?
min_term?() click to toggle source
# File lib/dpll_solver/formulas/or.rb, line 12
def min_term?
  false
end
not?()
Alias for: verum?
or?() click to toggle source
# File lib/dpll_solver/formulas/or.rb, line 18
def or?
  true
end
simplify() click to toggle source
# File lib/dpll_solver/formulas/or.rb, line 30
def simplify
  res_f1 = @f1.simplify
  res_f2 = @f2.simplify
  if res_f1.falsum? #identity
    return res_f2
  elsif res_f2.falsum? #identity
    return res_f1
  elsif res_f1.verum? || res_f2.verum? #anihilator
    return DpllSolver::Formulas::Verum
  elsif res_f1 == res_f2 #idempotence
    return res_f1
  else
    return self.class.new(res_f1, res_f2)
  end
end
to_s() click to toggle source
# File lib/dpll_solver/formulas/or.rb, line 4
def to_s
  "(#{@f1.to_s} OR #{@f2.to_s})"
end
variable?()
Alias for: verum?
verum?() click to toggle source
# File lib/dpll_solver/formulas/or.rb, line 22
def verum?
  false
end
Also aliased as: falsum?, not?, and?, variable?