Class: DpllSolver::Formulas::Not

Inherits:
Object
  • Object
show all
Defined in:
lib/dpll_solver/formulas/not.rb

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(f) ⇒ Not

Returns a new instance of Not.



6
7
8
 
# File 'lib/dpll_solver/formulas/not.rb', line 6

def initialize(f)
  @f = f
end

Instance Attribute Details

#f ⇒ Object

Returns the value of attribute f.



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

def f
  @f
end

Instance Method Details

#==(other) ⇒ Object Also known as: eql? 



10
11
12
 
# File 'lib/dpll_solver/formulas/not.rb', line 10

def ==(other)
  other.class == self.class && other.f == @f
end

#apply_DeMorgan ⇒ Object 



73
74
75
76
77
78
79
80
81
 
# File 'lib/dpll_solver/formulas/not.rb', line 73

def apply_DeMorgan
  if @f.and?
    return DpllSolver::Formulas::Or.new(self.class.new(@f.f1), self.class.new(@f.f2))
  elsif @f.or?
    return DpllSolver::Formulas::And.new(self.class.new(@f.f1), self.class.new(@f.f2))
  else
    raise ArgumentError, 'DeMorgan can not be applied unless @f is either AND or OR'
  end
end

#atomic_formula? ⇒ Boolean

Returns:

  • (Boolean) 


24
25
26
 
# File 'lib/dpll_solver/formulas/not.rb', line 24

def atomic_formula?
  false
end

#cnf ⇒ Object 



69
70
71
 
# File 'lib/dpll_solver/formulas/not.rb', line 69

def cnf
  nnf? ? self : nnf.cnf
end

#literal? ⇒ Boolean Also known as: nnf?, clause?, min_term?

Returns:

  • (Boolean) 


20
21
22
 
# File 'lib/dpll_solver/formulas/not.rb', line 20

def literal?
  @f.atomic_formula?
end

#nnf ⇒ Object 



59
60
61
62
63
64
65
66
67
 
# File 'lib/dpll_solver/formulas/not.rb', line 59

def nnf
  if @f.and? || @f.or?
    return apply_DeMorgan.nnf
  elsif @f.not?
    return @f.f.nnf
  else
    return self
  end
end

#not? ⇒ Boolean

Returns:

  • (Boolean) 


33
34
35
 
# File 'lib/dpll_solver/formulas/not.rb', line 33

def not?
  true
end

#simplify ⇒ Object 



45
46
47
48
49
50
51
52
53
54
55
56
57
 
# File 'lib/dpll_solver/formulas/not.rb', line 45

def simplify
  result = @f.simplify
  if result.not?
    result = result.f.simplify
  elsif result.verum?
    result = DpllSolver::Formulas::Falsum
  elsif result.falsum?
    result = DpllSolver::Formulas::Verum
  else
    result = self.class.new(result)
  end
  result
end

#to_s ⇒ Object 



16
17
18
 
# File 'lib/dpll_solver/formulas/not.rb', line 16

def to_s
  "-#{@f.to_s}"
end

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

Returns:

  • (Boolean) 


37
38
39
 
# File 'lib/dpll_solver/formulas/not.rb', line 37

def verum?
  false
end