Class: ModelUtils

Inherits:
Object
  • Object
show all
Defined in:
lib/solver-lib.rb

Class Method Summary collapse

Class Method Details

.foreach_field_in_model_str(str, const_info, &block) ⇒ Object 



540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
 
# File 'lib/solver-lib.rb', line 540

def self.foreach_field_in_model_str(str, const_info, &block)
  unless str =~ /^\((.*)\)$/m
    raise RuntimeError.new("could not parse model: #{str.inspect}")
  end
  str = $1

  while str.size() > 0 do
    line = Z3Solver.find_matching_bracket(str)
    str = str[line.size()..]
    unless line =~ /\(([^\ ]*)\ (.*)\)/
      raise RuntimeError.new("could not parse model line: #{line.inspect}")
    end
    varname = $1
    value = $2
    if value =~ /\(-\ (\d+)\)/ then
      simplified = "-#{$1}"
      value = simplified
    end
    info = const_info[varname]

    block.call(varname, value, info)
  end

  return nil
end

.handleSolverError(progress, session, options, result) ⇒ Object

Raises:

  • (RuntimeError) 


566
567
568
569
 
# File 'lib/solver-lib.rb', line 566

def self.handleSolverError(progress, session, options, result)
  session.writeProtocolToFile(progress, options[:solverLog])
  raise RuntimeError.new("Solver Error: Solver returned '#{result}', for more information see #{options[:solverLog]}")
end