Class: Lernen::Equiv::CombinedOracle

Inherits:
Oracle
  • Object
show all
Defined in:
lib/lernen/equiv/combined_oracle.rb

Overview

CombinedOracle provides an implementation of equivalence query that find a counterexample by combining multiple oracles.

This takes two oracle. If the first oracle finds a counterexample, then this oracle returns it. Otherwise, it tries the second and other oracles.

Instance Attribute Summary collapse

Attributes inherited from Oracle

#sul

Instance Method Summary collapse

Methods inherited from Oracle

#+

Constructor Details

#initialize(oracles) ⇒ CombinedOracle

Returns a new instance of CombinedOracle.

Raises:

  • (ArgumentError) 


17
18
19
20
21
22
23
24
25
26
27
 
# File 'lib/lernen/equiv/combined_oracle.rb', line 17

def initialize(oracles)
  first_oracle = oracles.first
  raise ArgumentError, "CombinedOracle nedds at least one oracle" unless first_oracle

  sul = oracles.first.sul
  oracles.each { |oracle| raise ArgumentError, "SUL of oracles must be the same" unless sul == oracle.sul }

  super(sul)

  @oracles = oracles
end

Instance Attribute Details

#oracles ⇒ Object (readonly)

: Array[Oracle[In, Out]]



29
30
31
 
# File 'lib/lernen/equiv/combined_oracle.rb', line 29

def oracles
  @oracles
end

Instance Method Details

#find_cex(hypothesis) ⇒ Object 



32
33
34
35
36
37
38
39
40
41
 
# File 'lib/lernen/equiv/combined_oracle.rb', line 32

def find_cex(hypothesis)
  super

  oracles.each do |oracle|
    cex = oracle.find_cex(hypothesis)
    return cex if cex
  end

  nil
end

#stats ⇒ Object 



44
45
46
47
48
49
50
51
52
53
54
 
# File 'lib/lernen/equiv/combined_oracle.rb', line 44

def stats
  num_queries = 0
  num_steps = 0
  oracles.each do |oracle|
    stats = oracle.stats
    num_queries += stats[:num_queries]
    num_steps += stats[:num_steps]
  end

  { num_calls: @num_calls, num_queries:, num_steps: }
end