class DpllSolver::Parsers::Parser

Public Class Methods

formula_to_clause(formula) click to toggle source
# File lib/dpll_solver/parsers/parser.rb, line 26
def self.formula_to_clause(formula)
  f_cnf = formula.simplify.cnf
  if f_cnf.verum?
    return Set.new
  elsif f_cnf.falsum?
    return Set.new([DpllSolver::Formulas::Clause.new])
  elsif f_cnf.variable?
    literal = DpllSolver::Formulas::Literal.new(f_cnf, true)
    return Set.new([DpllSolver::Formulas::Clause.new(literal)])
  elsif f_cnf.not?
    literal = DpllSolver::Formulas::Literal.new(f_cnf.f, false)
    return Set.new([DpllSolver::Formulas::Clause.new(literal)])
  elsif f_cnf.and?
    c1 = self.formula_to_clause(f_cnf.f1)
    c2 = self.formula_to_clause(f_cnf.f2)
    return c1 + c2
  elsif f_cnf.or?
    c1 = self.formula_to_clause(f_cnf.f1)
    c2 = self.formula_to_clause(f_cnf.f2)
    return Set.new([c1.first.union(c2.first)])
  else
    raise TypeError, "Formula has to be one of these classes: Verum, Falsum, Variable, And, Or, Not"
  end
end