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.