Skip to content

Bitwuzla: Avoid using exception to get a list of supported options #624

@daniel-raffler

Description

@daniel-raffler

Hello,

We're currently using a loop to probe all available solver options for Bitwuzla. Once the last option is reached an IllegalArgumentException is thrown, which we then have to catch:

  /**
   * Returns a listing of all options supported by Bitwuzla. The listing contains name and
   * option-object.
   */
  private static Map<String, Option> getAllAvailableOptions() {
    ImmutableMap.Builder<String, Option> allOptions = ImmutableMap.builder();
    // Options start at index 0, and go up to about 50, lets count further to be future-proof.
    // We could also use 'true' as upper limit, as we expect to break with exception at index ~50.
    // See Option-class at swigValues-length.
    for (int i = 0; i < 100; i++) {
      try {
        Option option = Option.swigToEnum(i);
        allOptions.put(option.toString(), option);
      } catch (IllegalArgumentException exception) { // exception is expected at index ~50
        break;
      }
    }
    return allOptions.buildOrThrow();
  }

While this works, it can cause issues while debugging as we may want to set a break point for IllegalArgumentException. The break point is then triggered whenever a new Bitwuzla context is created, which can happen quite a lot for some of our parametrized tests

We should therefore try to find another way to get the list of options. Note that SIWG should be able to generate a proper Java enum when given the right options, see here. We should then be able to simply use Options.values() to get a list of all options

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions