Options

A Bitwuzla instance is created from a configuration options BitwuzlaOptions instance. This options instance must be configured before creating the Bitwuzla instance: after the Bitwuzla instance is created, configuration options are fixed and cannot be changed.

Via the C API, Bitwuzla distinguishes two kinds of options: Numeric options (including Boolean options) and options with option modes. The kind of an option can be queried via bitwuzla_option_is_numeric(), and bitwuzla_option_is_mode().

Boolean and numeric options are configured via bitwuzla_set_option(), and options with option modes are configured via bitwuzla_set_option_mode().

The configured value of Boolean and numeric options can be queried via bitwuzla_get_option(), and the value of an option with modes can be queried via bitwuzla_get_option_mode().

The option kind is defined via BitwuzlaKind. A comprehensive list of all configurable options is available here.

Example

The source code for this example can be found at examples/c/options.c.

/***
 * Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
 *
 * Copyright (C) 2021 by the authors listed in the AUTHORS file at
 * https://github.com/bitwuzla/bitwuzla/blob/main/AUTHORS
 *
 * This file is part of Bitwuzla under the MIT license. See COPYING for more
 * information at https://github.com/bitwuzla/bitwuzla/blob/main/COPYING
 */

#include <bitwuzla/c/bitwuzla.h>
#include <inttypes.h>
#include <stdio.h>

int
main()
{
  // First, create a term manager instance.
  BitwuzlaTermManager* tm = bitwuzla_term_manager_new();
  // Create a Bitwuzla options instance.
  BitwuzlaOptions* options = bitwuzla_options_new();

  // Enable model generation, which expects a boolean configuration value.
  bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);

  // Increase the verbosity level, which expects an integer value.
  printf("Previous verbosity level: %" PRIu64 "\n",
         bitwuzla_get_option(options, BITWUZLA_OPT_VERBOSITY));
  bitwuzla_set_option(options, BITWUZLA_OPT_VERBOSITY, 2);
  printf("Current verbosity level: %" PRIu64 "\n",
         bitwuzla_get_option(options, BITWUZLA_OPT_VERBOSITY));

  // Now configure an option that has modes (a choice of configuration values).
  // First, query which bit-vector solver engine is set.
  printf("Default bv solver: %s\n",
         bitwuzla_get_option_mode(options, BITWUZLA_OPT_BV_SOLVER));
  // Then, select the propagation-based local search engine as solver engine.
  bitwuzla_set_option_mode(options, BITWUZLA_OPT_BV_SOLVER, "prop");
  printf("Current engine: %s\n",
         bitwuzla_get_option_mode(options, BITWUZLA_OPT_BV_SOLVER));

  // Now, create a Bitwuzla instance.
  Bitwuzla* bitwuzla = bitwuzla_new(tm, options);
  // Check sat (nothing to solve, input formula is empty).
  BitwuzlaResult result = bitwuzla_check_sat(bitwuzla);
  printf("Expect: sat\n");
  printf("Bitwuzla: %s\n", bitwuzla_result_to_string(result));

  // Finally, delete the Bitwuzla solver, options, and term manager instances.
  bitwuzla_delete(bitwuzla);
  bitwuzla_options_delete(options);
  bitwuzla_term_manager_delete(tm);

  return 0;
}

OptionInfo

Bitwuzla offers a compact way to retrieve all information about a configuration option as a BitwuzlaOptionInfo object via bitwuzla_get_option_info(). This object is created per option and can be queried for any available information, e.g., long and short option names, description, (current, default, minimum and maximum) values for numeric options, and (current, default and available) modes for configuration options with modes.