Class: Bparity::Formal::Deductive::Z3

Inherits:
Object
  • Object
show all
Defined in:
lib/bparity/formal/deductive.rb

Instance Method Summary collapse

Constructor Details

#initialize(timeout: 300, executable: ENV.fetch("BPARITY_Z3", "z3")) ⇒ Z3

Returns a new instance of Z3.



291
292
293
294
 
# File 'lib/bparity/formal/deductive.rb', line 291

def initialize(timeout: 300, executable: ENV.fetch("BPARITY_Z3", "z3"))
  @timeout = timeout
  @executable = executable
end

Instance Method Details

#available? ⇒ Boolean

Returns:

  • (Boolean) 


296
297
298
299
300
301
 
# File 'lib/bparity/formal/deductive.rb', line 296

def available?
  _out, _err, status = Open3.capture3(@executable, "--version")
  status.success?
rescue Errno::ENOENT
  false
end

#solve(script) ⇒ Object 



303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
 
# File 'lib/bparity/formal/deductive.rb', line 303

def solve(script)
  output = error = status = nil
  Open3.popen3(@executable, "-in") do |stdin, stdout, stderr, wait|
    stdin.write(script)
    stdin.close
    Timeout.timeout(@timeout) do
      output = stdout.read
      error = stderr.read
      status = wait.value
    end
  rescue Timeout::Error
    Process.kill("TERM", wait.pid) unless wait.join(0.1)
    return { verdict: :unknown, output: "z3 timed out after #{@timeout} seconds" }
  end
  first = output.lines.first&.strip
  verdict = { "unsat" => :unsat, "sat" => :sat }.fetch(first, :unknown)
  return { verdict:, output: output } unless verdict == :unknown

  { verdict: :unknown, output: status.success? ? output : error }
rescue Errno::ENOENT
  { verdict: :unavailable, output: "z3 executable not found" }
end