Class: Bparity::Formal::Deductive::RubyToSmt

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

Constant Summary collapse

SORTS =
{ "Integer" => "Int", "Boolean" => "Bool", "String" => "String" }.freeze
OPERATORS =
{ :+ => "+", :- => "-", :* => "*", :== => "=", :!= => "distinct",
:> => ">", :>= => ">=", :< => "<", :<= => "<=" }.freeze

Instance Method Summary collapse

Instance Method Details

#translate_file(path, method_name, parameter_types:) ⇒ Object

Raises:



60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
# File 'lib/bparity/formal/deductive.rb', line 60

def translate_file(path, method_name, parameter_types:)
  result = Prism.parse_file(path)
  raise ConfigurationError, "Cannot parse #{path}. Fix its Ruby syntax." unless result.success?

  method = find_method(result.value, method_name)
  raise ConfigurationError, "Method #{method_name} was not found in #{path}." unless method

  parameters = method.parameters.requireds.map(&:name)
  if parameters.length != parameter_types.length
    message = "Method #{method_name} has #{parameters.length} parameters, " \
              "but #{parameter_types.length} types were given."
    raise ConfigurationError,
          message
  end

  environment = parameters.each_with_index.to_h do |name, index|
    sort = SORTS.fetch(parameter_types[index]) do
      raise ConfigurationError,
            "F4 does not support #{parameter_types[index]}. Use Integer, Boolean, or String."
    end
    [name, Term.new("arg#{index}", sort) { |context| context.fetch(index) }]
  end
  body = translate_statements(method.body, environment)
  Translation.new(parameters: parameter_types.each_with_index.map do |type, index|
    ["arg#{index}", SORTS.fetch(type)]
  end,
                  term: body, source: path, method_name: method_name.to_s)
end