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
falsum?()
Alias for: verum?
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
not?()
Alias for: verum?
or?()
Alias for: verum?
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
variable?()
Alias for: verum?
verum?() click to toggle source
# File lib/dpll_solver/formulas/and.rb, line 24
def verum?
  false
end
Also aliased as: falsum?, not?, or?, variable?