Class: SolverSession

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

Instance Method Summary collapse

Constructor Details

#initialize(z3in, z3outAndErr, logFileName) ⇒ SolverSession

Returns a new instance of SolverSession.



16
17
18
19
20
21
22
23
24
 
# File 'lib/solver-lib.rb', line 16

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

Instance Method Details

#checkLineForSolverError(line, progress) ⇒ Object 



68
69
70
71
72
 
# File 'lib/solver-lib.rb', line 68

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 



48
49
50
51
52
 
# File 'lib/solver-lib.rb', line 48

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

#emptyReadBuffer(progress) ⇒ Object 



26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
 
# File 'lib/solver-lib.rb', line 26

def emptyReadBuffer(progress)
  empty = false
  while !empty do
    begin
      c = ""
      @z3outAndErr.read_nonblock(1, c)
      line = c + @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 



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

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

#from_solver(progress) ⇒ Object 



75
76
77
78
79
80
 
# File 'lib/solver-lib.rb', line 75

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

#generateNextAssertionIDAndAssociateWith(hash) ⇒ Object 



118
119
120
121
122
 
# File 'lib/solver-lib.rb', line 118

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

#get_const_info(name) ⇒ Object 



134
135
136
 
# File 'lib/solver-lib.rb', line 134

def get_const_info(name)
  @consts[name]
end

#getAssociationForAssertionID(assertionID) ⇒ Object 



124
125
126
 
# File 'lib/solver-lib.rb', line 124

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

#read_multiline_from_solver ⇒ Object 



86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
 
# File 'lib/solver-lib.rb', line 86

def read_multiline_from_solver()
  result = ""
  for_counting = ""
  @protocol.puts
  @protocol.puts("; BEGIN Multiline Solver Response:")
  line = @z3outAndErr.gets
  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 do
    line = @z3outAndErr.gets
    result += line
    for_counting += replace_strings(line)
    @protocol.puts("; #{line}")

    num_opening = for_counting.count("(")
    num_closing = for_counting.count(")")
  end
  @protocol.puts("; END Multiline Solver Response")
  return result
end

#replace_strings(line) ⇒ Object 



82
83
84
 
# File 'lib/solver-lib.rb', line 82

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

#to_solver(progress, line) ⇒ Object 



54
55
56
57
58
59
60
61
62
63
64
65
66
 
# File 'lib/solver-lib.rb', line 54

def to_solver(progress, line)
  emptyReadBuffer(progress);
  @protocol.puts(line)
  begin
    @z3in.puts(line)
  rescue Errno::EINVAL
    progress.print_line "ERROR: could not write the line #{line.inspect} to the solver."
    writeProtocolToFile("failure.smt2")
  rescue Errno::EPIPE
    writeProtocolToFile("failure.smt2")
    throw RuntimeError.new("Broken Pipe")
  end
end

#writeProtocolToFile(progress, filename) ⇒ Object 



111
112
113
114
115
116
 
# File 'lib/solver-lib.rb', line 111

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