Class: Ravensat::Solver

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

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(default_solver_name = "arcteryx") ⇒ Solver

Returns a new instance of Solver.



6
7
8
9
10
11
 
# File 'lib/ravensat/solver.rb', line 6

def initialize( default_solver_name = "arcteryx" )
  @name = default_solver_name
  # @cnf = Array.new
  # @nr_vars
  # @nr_clses
end

Instance Attribute Details

#name ⇒ Object

Returns the value of attribute name.



5
6
7
 
# File 'lib/ravensat/solver.rb', line 5

def name
  @name
end

Instance Method Details

#solve(cnf) ⇒ Object

def <<( clause )

'this is << method'

end



17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
 
# File 'lib/ravensat/solver.rb', line 17

def solve( cnf )
  @input_file = Tempfile.open(["ravensat",".cnf"])
  @output_file = Tempfile.open(["ravensat",".mdl"])

  @input_file.write cnf.to_dimacs
  @input_file.flush

  case @name
  when "arcteryx"
    Arcteryx.solve(@input_file.to_path, @output_file.to_path)
  else
    system("#{@name} #{@input_file.to_path} #{@output_file.to_path}")
  end

  model = @output_file.read.split("\n")

  case model.first
  when "SAT"
    model.last.split.each do |e|
      next if e == '0'
      cnf.name_table.find{|key,value| value == e.to_i.abs.to_s}.first.value = !e.start_with?('-')
    end
    Arcteryx::SAT
  when "UNSAT"
    Arcteryx::UNSAT
  end
end