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