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
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