class Ravensat::PropLogic

Attributes

formula[R]
name_table[R]

Public Class Methods

new( init_formula ) click to toggle source
# File lib/ravensat/prop_logic.rb, line 6
def initialize( init_formula )
  @formula = init_formula
     # (a | b) & (~a | b) & (a | ~b) & (~a | ~b)

     # [:and,
     #    [:or, a, b],
     #    [:or, [:not, a], b],
     #    [:or, a, [:not, b]],
     #    [:or, [:not, a], [:not, b]]
     # ]
end

Public Instance Methods

&( object ) click to toggle source
# File lib/ravensat/prop_logic.rb, line 60
def &( object )
  if @formula.first == :and
    @formula.append object.formula
  else
    @formula = [:and, @formula, object.formula]
  end
  self
  # Ravensat::PropLogic.new [:and, @formula, object]
  # formulaがcnfである前提の実装
  # @formula & other_formula
end
to_cnf() click to toggle source
# File lib/ravensat/prop_logic.rb, line 18
def to_cnf

end
to_dimacs() click to toggle source
# File lib/ravensat/prop_logic.rb, line 22
def to_dimacs
  cnf_text = String.new
  tmp_name_table = @formula.flatten.uniq.reject{|e| e.class == Symbol}
  @name_table = tmp_name_table.zip((1..tmp_name_table.size).to_a.map{|e| e.to_s}).to_h

  nr_vars = tmp_name_table.size
  nr_clses = @formula.size - 1
  cnf_header = 'p cnf ' << nr_vars.to_s << ' ' << nr_clses.to_s << "\n"
  # @formula.is_cnf?
  @formula.each do |clause|
    # next if clause.first != :and
    case clause
    when Symbol
      next
    when Array
      case clause.first
      when :or
        clause.each do |literal|
          case literal
          when Symbol
            next
          when Ravensat::PropVar
            cnf_text << @name_table[literal] << ' '
          when Array #&& literal.first == :not
            cnf_text << '-' << @name_table[literal.last] << ' '
          end
        end
      when :not
        cnf_text << '-' << @name_table[clause.last] << ' '
      end
    when Ravensat::PropVar
      cnf_text << @name_table[clause] << ' '
    end
    cnf_text << '0' << "\n"
  end
  cnf_header + cnf_text
end
|( object ) click to toggle source
# File lib/ravensat/prop_logic.rb, line 72
def |( object )
  if @formula.first == :or
    @formula.append object.formula
  else
    @formula = [:or, @formula, object.formula]
  end
  self
  # Ravensat::PropLogic.new [:or, @formula, object]
  # 木構造に落とすのが難しそう,実装見送り
  # @formula | other_formula
end