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