Module: Ibex::CLICounterexampleOptions

Included in:
CLI
Defined in:
lib/ibex/cli/counterexample_options.rb,
sig/ibex/cli/counterexample_options.rbs

Overview

Counterexample report limits and their command-line validation.

Constant Summary collapse

DEFAULTS =

RBS:

  • @options: cli_options

Returns:

  • (Hash[Symbol, Integer]) 
{
  counterexample_max_tokens: LALR::ConflictSearchLimits::DEFAULT_MAX_TOKENS,
  counterexample_max_configurations: LALR::ConflictSearchLimits::DEFAULT_MAX_CONFIGURATIONS
}.freeze

Instance Method Summary collapse

Instance Method Details

#add_counterexample_options(options) ⇒ void

This method returns an undefined value.

RBS:

  • (OptionParser options) -> void

Parameters:

  • options (OptionParser) 


18
19
20
21
22
23
24
25
26
27
28
29
30
 
# File 'lib/ibex/cli/counterexample_options.rb', line 18

def add_counterexample_options(options)
  options.on("--counterexamples", "include conflict counterexamples in a report") { @options[:verbose] = true }
  options.on("--counterexample-max-tokens=N", Integer, "maximum counterexample search token budget") do |value|
    @options[:counterexample_max_tokens] = positive_counterexample_limit(value, "--counterexample-max-tokens")
  end
  options.on(
    "--counterexample-max-configurations=N", Integer, "maximum counterexample search configuration budget"
  ) do |value|
    @options[:counterexample_max_configurations] = positive_counterexample_limit(
      value, "--counterexample-max-configurations"
    )
  end
end

#positive_counterexample_limit(value, option) ⇒ Integer

RBS:

  • (Integer value, String option) -> Integer

Parameters:

  • value (Integer)
  • option (String)

Returns:

  • (Integer) 


33
34
35
36
37
38
39
40
 
# File 'lib/ibex/cli/counterexample_options.rb', line 33

def positive_counterexample_limit(value, option)
  if value.positive?
    @options[:verbose] = true
    return value
  end

  raise Ibex::Error, "(cli):1:1: #{option} must be positive"
end