Class: Z3Solver

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

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(progress, z3path) ⇒ Z3Solver

Returns a new instance of Z3Solver.



382
383
384
385
386
387
388
 
# File 'lib/solver-lib.rb', line 382

def initialize(progress, z3path)
    @progress = progress
    @z3in, @z3outAndErr, @z3thr = Open3.popen2e(z3path, '-in', '-smt2')
    Process.detach(@z3thr.pid)
    @z3in.sync = true
    @sessionIdCounter = 0
end

Instance Attribute Details

#z3in ⇒ Object (readonly)

Returns the value of attribute z3in.



380
381
382
 
# File 'lib/solver-lib.rb', line 380

def z3in
  @z3in
end

#z3outAndErr ⇒ Object (readonly)

Returns the value of attribute z3outAndErr.



380
381
382
 
# File 'lib/solver-lib.rb', line 380

def z3outAndErr
  @z3outAndErr
end

Class Method Details

.find_matching_bracket(str) ⇒ Object 



455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
 
# File 'lib/solver-lib.rb', line 455

def self.find_matching_bracket(str)
  i = 0
  open = 0
  in_str = false
  while open <= 0 do
    if str[i] == '(' and !in_str then
      open += 1
    elsif str[i] == '"' then
      in_str = !in_str
    end
    i += 1    
  end
  while open > 0 do
    if str[i] == '(' && !in_str then
      open += 1
    elsif str[i] == ')' && !in_str then
      open -= 1
    elsif str[i] == '"' then
      in_str = !in_str
    end
    i += 1
  end
  str[0,i]
end

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



480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
 
# File 'lib/solver-lib.rb', line 480

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

Instance Method Details

#close ⇒ Object 



390
391
392
393
394
395
396
397
398
399
400
 
# File 'lib/solver-lib.rb', line 390

def close()
  begin
    @z3in.close() unless @z3in.closed?
  rescue Errno::EINVAL
  end
  begin
    @z3outAndErr.close() unless @z3outAndErr.closed?
  rescue Errno::EINVAL
  end
  Thread.kill(@z3thr)
end

#display_assertion(assertion, session) ⇒ Object 



402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
 
# File 'lib/solver-lib.rb', line 402

def display_assertion(assertion, session)
  if assertion =~ /validation_rule_(.*)_instance_(.*)/ then
    return "Validation rule #{$1} of structure #{$2.gsub("_", "/")}"
  else
    info = session.getAssociationForAssertionID(assertion)
    if info then
      if info[:assertion_type] == :doc_field_filled then
        return "Field #{info[:xpath]} contains value #{info[:value].inspect} in document"
      elsif info[:assertion_type] == :doc_field_empty then
        return "Field #{info[:xpath]} is empty in document"
      elsif info[:assertion_type] == :doc_structure_exists then
        return "Structure #{info[:xpath]} exists in document"
      elsif info[:assertion_type] == :doc_structure_not_exists then
        return "Structure #{info[:xpath]} does not exist in document"
      elsif info[:assertion_type] == :constraint then
        if info[:constraint_type] == :min then
          return "Field #{info[:xpath]} has a minimum value of #{info[:value]}."
        elsif info[:constraint_type] == :max then
          return "Field #{info[:xpath]} has a maximum value of #{info[:value]}."
        elsif info[:constraint_type] == :required then
          return "Field #{info[:xpath]} is required."
        else
          p info
          raise RuntimeError.new("encountered unknown :constraint_type #{info[:constraint_type].inspect} for assertionID #{assertion.inspect}")
        end
      else
        raise RuntimeError.new("encountered unknown :assertion_type #{info[:assertion_type].inspect} for assertionID #{assertion.inspect}")
      end
    else
      return assertion
    end
  end
end

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

Raises:

  • (RuntimeError) 


506
507
508
509
 
# File 'lib/solver-lib.rb', line 506

def 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

#parse_unsat_core(unsat_core, session) ⇒ Object 



436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
 
# File 'lib/solver-lib.rb', line 436

def parse_unsat_core(unsat_core, session)
  unless unsat_core =~ /\((.*)\)/ then
    raise RuntimeError.new("could not parse unsat core: #{unsat_core.inspect}")
  end
  list = $1.split(" ")

  result = "EXPLANATION:\n"
  result += "The following values\n"

  list.filter{|a| a.start_with?("doc-")}.each do |assertion|
    result += "- #{display_assertion(assertion, session)} (#{assertion})\n"
  end
  result += "\nviolate the following constraints\n"
  list.filter{|a| !a.start_with?("doc-")}.each do |assertion|
    result += "- #{display_assertion(assertion, session)} (#{assertion})\n"
  end
  return result
end