hets/prove/szs_parser.rb

9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainenmodule Hets
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen  module Prove
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen    class SZSParser
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen      attr_reader :prover, :output
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen      def initialize(prover, output)
9ddd3d7d8651985e373a6c48e0ddc76b8a4ef1c7Timo Sirainen        @prover = prover
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen        @output = output
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen      end
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen      def call
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen        prover_specific_parser =
9137c55411aa39d41c1e705ddc34d5bd26c65021Timo Sirainen          :"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