Class: DpllSolver::Formulas::Or

Inherits:
BinaryFormula show all
Defined in:
lib/dpll_solver/formulas/or.rb

Instance Attribute Summary

Attributes inherited from BinaryFormula

#f1, #f2

Instance Method Summary collapse

Methods inherited from BinaryFormula

#==, #atomic_formula?, #dnf?, #initialize, #literal?, #nnf, #nnf?

Constructor Details

This class inherits a constructor from BinaryFormula

Instance Method Details

#clause? ⇒ Boolean Also known as: cnf?

Returns:

  • (Boolean) 


8
9
10
 
# File 'lib/dpll_solver/formulas/or.rb', line 8

def clause?
  @f1.clause? && @f2.clause?
end

#cnf ⇒ Object 



46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
 
# 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

#min_term? ⇒ Boolean

Returns:

  • (Boolean) 


12
13
14
 
# File 'lib/dpll_solver/formulas/or.rb', line 12

def min_term?
  false
end

#or? ⇒ Boolean

Returns:

  • (Boolean) 


18
19
20
 
# File 'lib/dpll_solver/formulas/or.rb', line 18

def or?
  true
end

#simplify ⇒ Object 



30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
 
# 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 ⇒ Object 



4
5
6
 
# File 'lib/dpll_solver/formulas/or.rb', line 4

def to_s
  "(#{@f1.to_s} OR #{@f2.to_s})"
end

#verum? ⇒ Boolean Also known as: falsum?, not?, and?, variable?

Returns:

  • (Boolean) 


22
23
24
 
# File 'lib/dpll_solver/formulas/or.rb', line 22

def verum?
  false
end