lib/hets/prove/szs_parser.rb
module Hets
module Prove
class SZSParser
attr_reader :prover, :output
def initialize(prover, output)
@prover = prover
@output = output
end
def call
prover_specific_parser =
:"parse_status_#{prover.parameterize.gsub('-', '_')}"
send(prover_specific_parser)
rescue NameError
generic_parse_status
end
private
def generic_parse_status
regex_parse_status(/SZS status (\w+)/)
end
def parse_status_darwin
status = regex_parse_status(/\n\nSZS status (\w+)/)
if status == 'Timeout'
'ResourceOut'
else
status
end
end
def parse_status_darwin_non_fd
parse_status_darwin
end
def parse_status_eprover
regex_parse_status(/\n# SZS status (\w+)/)
end
def parse_status_spass
if match = generic_parse_status
match
elsif output.match(/^SPASS beiseite: Ran out of time.$/)
'ResourceOut'
end
end
def regex_parse_status(regex)
match = output.match(regex)
match[1] if match
end
end
end
end