Module: Bparity::Formal::Deductive::ModelParser

Defined in:

lib/bparity/formal/deductive.rb

Class Method Summary

• .call(output) ⇒ Object
• .find_definitions(value) ⇒ Object
• .parse(tokens) ⇒ Object
• .parse_all(tokens) ⇒ Object
• .ruby_value(sort, value) ⇒ Object

Class Method Details

.call(output) ⇒ Object

# File 'lib/bparity/formal/deductive.rb', line 330

def call(output)
  expressions = parse_all(output.scan(/"(?:[^"]|"")*"|[()]|[^\s()]+/))
  definitions = expressions.flat_map { |expression| find_definitions(expression) }
  definitions.to_h do |definition|
    [definition.fetch(1), ruby_value(definition.fetch(3), definition.fetch(4))]
  end
rescue StandardError
  {}
end

.find_definitions(value) ⇒ Object

# File 'lib/bparity/formal/deductive.rb', line 356

def find_definitions(value)
  return [] unless value.is_a?(Array)

  found = value.first == "define-fun" ? [value] : []
  found + value.flat_map { |child| find_definitions(child) }
end

.parse(tokens) ⇒ Object

# File 'lib/bparity/formal/deductive.rb', line 346

def parse(tokens)
  token = tokens.shift
  return token unless token == "("

  values = []
  values << parse(tokens) until tokens.first == ")" || tokens.empty?
  tokens.shift
  values
end

.parse_all(tokens) ⇒ Object

# File 'lib/bparity/formal/deductive.rb', line 340

def parse_all(tokens)
  values = []
  values << parse(tokens) until tokens.empty?
  values
end

.ruby_value(sort, value) ⇒ Object

# File 'lib/bparity/formal/deductive.rb', line 363

def ruby_value(sort, value)
  case sort
  when "Int" then value.is_a?(Array) ? -Integer(value.fetch(1), 10) : Integer(value, 10)
  when "Bool" then value == "true"
  when "String" then value.delete_prefix('"').delete_suffix('"').gsub('""', '"')
  end
end