class DpllSolver::Formulas::And
Public Instance Methods
and?()
click to toggle source
# File lib/dpll_solver/formulas/and.rb, line 20 def and? true end
clause?()
click to toggle source
# File lib/dpll_solver/formulas/and.rb, line 8 def clause? false end
cnf()
click to toggle source
# File lib/dpll_solver/formulas/and.rb, line 48 def cnf nnf? ? self.class.new(@f1.cnf, @f2.cnf) : nnf.cnf end
cnf?()
click to toggle source
# File lib/dpll_solver/formulas/and.rb, line 16 def cnf? @f1.cnf? && @f2.cnf? end
min_term?()
click to toggle source
# File lib/dpll_solver/formulas/and.rb, line 12 def min_term? @f1.min_term? && @f2.min_term? end
simplify()
click to toggle source
# File lib/dpll_solver/formulas/and.rb, line 32 def simplify res_f1 = @f1.simplify res_f2 = @f2.simplify if res_f1.verum? #identity return res_f2 elsif res_f2.verum? #identity return res_f1 elsif res_f1.falsum? || res_f2.falsum? #anihilator return DpllSolver::Formulas::Falsum 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/and.rb, line 4 def to_s "(#{@f1.to_s} AND #{@f2.to_s})" end