class Z3::Model

Attributes

entries[RW]
map_table[RW]

Public Class Methods

new(file) click to toggle source
# File lib/z3/model.rb, line 34
def initialize(file)
  lines = File.read(file).lines
  start = lines.rindex{|l| l =~ /\*\*\* MODEL/}
  @entries = ModelParser.new.parse(lines.drop(start || 0).join)
  collect_map_values!
  resolve!
end

Public Instance Methods

collect_map_values!() click to toggle source
# File lib/z3/model.rb, line 72
def collect_map_values!
  @map_table = {}

  @@map_maps.each do |mm|
    @entries[mm].each do |keys,val|
      next unless keys
      keys = keys.map{|key| lookup key, false}
      @map_table[keys[0]] ||= {map: true}
      @map_table[keys[0]][keys[1]] = lookup(val, false)
    end if @entries.include? mm
  end

  @entries.select{|k,_| k =~ /^k!\d+$/}.each do |k,vs|
    next unless vs.is_a?(Hash)
    k = lookup(k,false)
    @map_table[k] = {map: true}
    vs.each do |v,vv|
      @map_table[k][v] = lookup(vv,false)
    end
  end
end
constants() click to toggle source
# File lib/z3/model.rb, line 59
def constants
  @entries.select do |sym,val|
    visible(sym) && sym !~ variable_pattern &&
    (!val.is_a?(Hash) || val.include?(:map))
  end
end
functions() click to toggle source
# File lib/z3/model.rb, line 65
def functions
  @entries.select do |sym,val|
    visible(sym) && sym !~ variable_pattern &&
    val.is_a?(Hash) && !val.include?(:map)
  end
end
ident_pattern() click to toggle source
# File lib/z3/model.rb, line 49
def ident_pattern; /[a-zA-Z_.$\#'`~^\\?][\w.$\#'`~^\\?]*/ end
lookup(value, use_map_table = true) click to toggle source
# File lib/z3/model.rb, line 110
def lookup(value, use_map_table = true)
  result = @entries[@@u2b] && @entries[@@u2b][value]
  return result unless result.nil? # result could be false!

  return @entries[@@u2i] && @entries[@@u2i][value] ||
  use_map_table && @map_table[value] ||
  use_map_table && value.to_s =~ /as-array/ &&
  @map_table[value.to_s.match(/as-array\[(k!\d+)\]/){|m| m[1].to_sym}] ||
  value unless value.nil?
end
resolve(value) click to toggle source
# File lib/z3/model.rb, line 100
def resolve value
  case value
  when Array; value.map{|v| resolve(v)}
  when Hash; value.map{|k,v| [resolve(k), resolve(v)]}.to_h
  else
    new_value = lookup(value)
    new_value.is_a?(Hash) ? resolve(new_value) : new_value
  end
end
resolve!() click to toggle source
# File lib/z3/model.rb, line 94
def resolve!
  @entries.each do |symbol,value|
    @entries[symbol] = resolve(value)
  end
end
to_s() click to toggle source
# File lib/z3/model.rb, line 42
def to_s
  @entries.select{|sym,_| visible(sym)}.map do |sym,val|
    "#{sym} = #{val}"
  end.sort * "\n"
end
variable_pattern(idx = nil) click to toggle source
# File lib/z3/model.rb, line 50
def variable_pattern(idx = nil); /^(#{ident_pattern})@#{idx || /[0-9]+/}$/ end
variables(idx = nil) click to toggle source
# File lib/z3/model.rb, line 52
def variables(idx = nil)
  @entries.select do |sym,_|
    visible(sym) && sym =~ variable_pattern(idx)
  end.map do |sym,val|
    idx ? [variable_pattern.match(sym){|m| m[1]}, val] : [sym,val]
  end.to_h
end
visible(sym) click to toggle source
# File lib/z3/model.rb, line 48
def visible(sym) sym !~ @@blacklist end