Class: Ravensat::DimacsEncoder

Inherits:
Object
  • Object
show all
Defined in:
lib/ravensat/dimacs/dimacs_encoder.rb

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize ⇒ DimacsEncoder

Returns a new instance of DimacsEncoder.



4
5
6
 
# File 'lib/ravensat/dimacs/dimacs_encoder.rb', line 4

def initialize
  @name_table = {}
end

Instance Attribute Details

#name_table ⇒ Object (readonly)

Returns the value of attribute name_table.



3
4
5
 
# File 'lib/ravensat/dimacs/dimacs_encoder.rb', line 3

def name_table
  @name_table
end

Instance Method Details

#create_table(formula) ⇒ Object 



27
28
29
 
# File 'lib/ravensat/dimacs/dimacs_encoder.rb', line 27

def create_table(formula)
  @name_table = formula.vars.zip((1..formula.vars.size).map(&:to_s)).to_h
end

#to_dimacs(formula) ⇒ Object 



8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
 
# File 'lib/ravensat/dimacs/dimacs_encoder.rb', line 8

def to_dimacs(formula)
  return nil unless formula.cnf?

  dimacs_header = "p cnf #{formula.vars_size} #{formula.clauses_size}\n"
  dimacs_body = ""
  create_table(formula)
  formula.each do |node|
    case node
    when AndNode then dimacs_body << " 0\n"
    when OrNode then dimacs_body << " "
    when NotNode then dimacs_body << "-"
    when VarNode then dimacs_body << @name_table[node]
    end
  end
  dimacs_body << " 0\n"

  dimacs_header + dimacs_body
end