Class: Bparity::Formal::Deductive::Runner

Inherits:
Object
  • Object
show all
Defined in:
lib/bparity/formal/deductive.rb

Instance Method Summary collapse

Constructor Details

#initialize(old_translation:, new_translation:, old_callable:, new_callable:, validation_inputs:, assumptions: %i[h1 h3],, solver: Z3.new, validation_scope: nil) ⇒ Runner

Returns a new instance of Runner.



373
374
375
376
377
378
379
380
381
382
383
384
385
 
# File 'lib/bparity/formal/deductive.rb', line 373

def initialize(old_translation:, new_translation:, old_callable:, new_callable:, validation_inputs:,
               assumptions: %i[h1 h3], solver: Z3.new, validation_scope: nil)
  @old_translation = old_translation
  @new_translation = new_translation
  @old_callable = old_callable
  @new_callable = new_callable
  @validation_inputs = validation_inputs
  @assumptions = assumptions
  @solver = solver
  @validation_scope = validation_scope || { "cases" => validation_inputs.length,
                                            "exhaustive" => true,
                                            "domain" => "provided bounded validation inputs" }
end

Instance Method Details

#run ⇒ Object 



387
388
389
390
391
392
393
394
395
396
397
398
 
# File 'lib/bparity/formal/deductive.rb', line 387

def run
  validations = validate_translations
  return result(:inconclusive, validations, "translation validation failed") unless validations.all?(&:valid)
  return result(:inconclusive, validations, "z3 executable not found") unless @solver.available?

  solved = @solver.solve(ProductProgram.call(@old_translation, @new_translation))
  case solved[:verdict]
  when :unsat then result(:no_difference_found, validations, "Z3 returned unsat")
  when :sat then result(:difference_found, validations, "Z3 returned sat", counterexample(solved[:output]))
  else result(:inconclusive, validations, "Z3 returned unknown", solved[:output])
  end
end