Class: SolverSession

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

Instance Method Summary collapse

Constructor Details

#initialize(solverFactory, logFileName) ⇒ SolverSession

Returns a new instance of SolverSession.



8
9
10
11
12
13
14
15
16
 
# File 'lib/solver-lib.rb', line 8

def initialize(solverFactory, logFileName)
  @solverFactory = solverFactory
  @solver = @solverFactory.new_solver()
  @protocol_filename = logFileName
  @protocol = File.open(@protocol_filename, "w")
  @assertCounter = -1
  @associations = {}
  @consts = {}
end

Instance Method Details

#associateAssertionIDWith(assertionID, hash) ⇒ Object 



142
143
144
145
146
147
 
# File 'lib/solver-lib.rb', line 142

def associateAssertionIDWith(assertionID, hash)
  if @associations.has_key?(assertionID) then
    raise RuntimeError.new("AssertionID #{assertionID.inspect} already has info associated with it!")
  end
  @associations[assertionID] = hash
end

#checkLineForSolverError(line, progress) ⇒ Object 



84
85
86
87
88
 
# File 'lib/solver-lib.rb', line 84

def checkLineForSolverError(line, progress)
  if line =~ /\(error \"(.*)\"\)/ then
    progress.print_line("WARN: Solver reported ERROR: #{$1}")
  end
end

#declare_const(progress, name, type, info) ⇒ Object 



53
54
55
56
57
 
# File 'lib/solver-lib.rb', line 53

def declare_const(progress, name, type, info)
  info[:type] = type
  @consts[name] = info
  to_solver(progress, "(declare-const #{name} #{type})")
end

#emptyReadBuffer(progress) ⇒ Object 



31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
 
# File 'lib/solver-lib.rb', line 31

def emptyReadBuffer(progress)
  empty = false
  while !empty do
    begin
      c = ""
      @solver.z3outAndErr.read_nonblock(1, c)
      line = c + @solver.z3outAndErr.gets
      checkLineForSolverError(line, progress)
      @protocol.puts("; Solver Response: #{line}")
    rescue Errno::EWOULDBLOCK
      # there is nothing to read -> just continue
      empty = true
    rescue Errno::EAGAIN
      # there is nothing to read -> just continue
      empty = true
    rescue EOFError
      # there is nothing to read -> just continue
      empty = true
    end
  end
end

#for_each_const(&block) ⇒ Object 



153
154
155
156
157
 
# File 'lib/solver-lib.rb', line 153

def for_each_const(&block)
  @consts.each do |key, value|
    block.call(key, value)
  end
end

#from_solver(progress) ⇒ Object 



91
92
93
94
95
96
 
# File 'lib/solver-lib.rb', line 91

def from_solver(progress)
  result = @solver.z3outAndErr.gets(chomp: true)
  checkLineForSolverError(result, progress)
  @protocol.puts("; Solver Response: #{result}")
  return result
end

#generateNextAssertionIDAndAssociateWith(hash) ⇒ Object 



136
137
138
139
140
 
# File 'lib/solver-lib.rb', line 136

def generateNextAssertionIDAndAssociateWith(hash)
  nextAssertionID = "a#{@assertCounter += 1}"
  @associations[nextAssertionID] = hash
  return nextAssertionID
end

#get_const_info(name) ⇒ Object 



159
160
161
 
# File 'lib/solver-lib.rb', line 159

def get_const_info(name)
  @consts[name]
end

#getAssociationForAssertionID(assertionID) ⇒ Object 



149
150
151
 
# File 'lib/solver-lib.rb', line 149

def getAssociationForAssertionID(assertionID)
  return @associations[assertionID]
end

#handleSolverError(progress, options, result) ⇒ Object 



167
168
169
 
# File 'lib/solver-lib.rb', line 167

def handleSolverError(progress, options, result)
  @solver.handleSolverError(progress, self, options, result)
end

#parse_unsat_core(unsat_core) ⇒ Object 



163
164
165
 
# File 'lib/solver-lib.rb', line 163

def parse_unsat_core(unsat_core)
  @solver.parse_unsat_core(unsat_core, self)
end

#read_multiline_from_solver ⇒ Object 



102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
 
# File 'lib/solver-lib.rb', line 102

def read_multiline_from_solver()
  result = ""
  for_counting = ""
  @protocol.puts
  @protocol.puts("; BEGIN Multiline Solver Response:")
  line = @solver.z3outAndErr.gets(chomp: true)
  result += line
  for_counting = replace_strings(line)
  @protocol.puts("; #{line}")
  
  num_opening = for_counting.count("(")
  num_closing = for_counting.count(")")
  while num_opening > num_closing && line != nil do
    line = @solver.z3outAndErr.gets(chomp: true)
    if line
      result += line
      for_counting = replace_strings(line)
      @protocol.puts("; #{line}")
      
      num_opening += for_counting.count("(")
      num_closing += for_counting.count(")")
    end
  end
  @protocol.puts("; END Multiline Solver Response")
  return result
end

#replace_strings(line) ⇒ Object 



98
99
100
 
# File 'lib/solver-lib.rb', line 98

def replace_strings(line)
  line.gsub(/"[^"]*"/, "")
end

#switch_solver(progress) ⇒ Object 



18
19
20
21
22
23
24
25
26
27
28
29
 
# File 'lib/solver-lib.rb', line 18

def switch_solver(progress)
  @solver.close()
  @solver = @solverFactory.new_solver()
  # re-feed the session protocol into the new solver to get it up-to-date
  @protocol.close()
  File.open(@protocol_filename, "r") do |protocol|
    protocol.each_line do |line|
      to_solver(progress, line)
    end
  end
  @protocol = File.open(@protocol_filename, "a")
end

#to_solver(progress, line) ⇒ Object 



59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
 
# File 'lib/solver-lib.rb', line 59

def to_solver(progress, line)
  emptyReadBuffer(progress);
  success = false
  while (!success) do
    begin
      @solver.z3in.puts(line)
      success = true
    rescue Errno::EINVAL => e
      progress.print_line("DEBUG: Invalid argument to puts(): #{line.inspect}")
      progress.print_line("An Error occured: #{e.message}")
      e.backtrace.each { |stline| progress.print_line(stline) }
      progress.print_line("=> Switching Solver")
      switch_solver(progress)
      progress.print_line("=> Switch successful. Trying again.")
    rescue Errno::EPIPE => e
      progress.print_line("An Error occured: #{e.message}")
      e.backtrace.each { |stline| progress.print_line(stline) }
      progress.print_line("=> Switching Solver")
      switch_solver(progress)
      progress.print_line("=> Switch successful. Trying again.")
    end
  end
  @protocol.puts(line)
end

#writeProtocolToFile(progress, filename) ⇒ Object 



129
130
131
132
133
134
 
# File 'lib/solver-lib.rb', line 129

def writeProtocolToFile(progress, filename)
  dir = File.dirname(filename)
  FileUtils.mkdir_p(dir) unless Dir.exist?(dir)
  FileUtils.cp(@protocol_filename, filename) unless @protocol_filename == filename
  progress.print_line "Solver protocol written to file #{filename}"
end