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.



438
439
440
441
442
443
444
 
# File 'lib/solver-lib.rb', line 438

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.



436
437
438
 
# File 'lib/solver-lib.rb', line 436

def z3in
  @z3in
end

#z3outAndErr ⇒ Object (readonly)

Returns the value of attribute z3outAndErr.



436
437
438
 
# File 'lib/solver-lib.rb', line 436

def z3outAndErr
  @z3outAndErr
end

Class Method Details

.find_matching_bracket(str) ⇒ Object 



511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
 
# File 'lib/solver-lib.rb', line 511

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

Instance Method Details

#close ⇒ Object 



446
447
448
449
450
451
452
453
454
455
456
 
# File 'lib/solver-lib.rb', line 446

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 



458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
 
# File 'lib/solver-lib.rb', line 458

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

#parse_unsat_core(unsat_core, session) ⇒ Object 



492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
 
# File 'lib/solver-lib.rb', line 492

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