class DpllSolver::Formulas::Clause

Attributes

literals[RW]

Public Class Methods

new(*args) click to toggle source
# File lib/dpll_solver/formulas/clause.rb, line 5
def initialize(*args)
  @literals = Set.new(args)
end

Public Instance Methods

==(other) click to toggle source
# File lib/dpll_solver/formulas/clause.rb, line 42
def ==(other)
  other.class == self.class && other.literals == @literals
end
Also aliased as: eql?
add(literal) click to toggle source
# File lib/dpll_solver/formulas/clause.rb, line 9
def add(literal)
  @literals.add(literal)
  self
end
delete(literal) click to toggle source
# File lib/dpll_solver/formulas/clause.rb, line 14
def delete(literal)
  literal_array = @literals.to_a
  literal_array.delete(literal)
  @literals = Set.new(literal_array)
  self
end
empty?() click to toggle source
# File lib/dpll_solver/formulas/clause.rb, line 25
def empty?
  @literals.empty?
end
eql?(other)
Alias for: ==
get_unit_literal() click to toggle source
# File lib/dpll_solver/formulas/clause.rb, line 38
def get_unit_literal
  @literals.first if unit?
end
include?(literal) click to toggle source
# File lib/dpll_solver/formulas/clause.rb, line 29
def include?(literal)
  @literals.to_a.include?(literal)
end
to_s() click to toggle source
# File lib/dpll_solver/formulas/clause.rb, line 46
def to_s
  "{#{@literals.to_a.map(&:to_s).join(', ')}}"
end
union(other) click to toggle source
# File lib/dpll_solver/formulas/clause.rb, line 33
def union(other)
  @literals = @literals + other.literals
  self
end
unit?() click to toggle source
# File lib/dpll_solver/formulas/clause.rb, line 21
def unit?
  @literals.count == 1
end