Options

A bitwuzla.Bitwuzla instance is created from a configuration options bitwuzla.Options 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.

Bitwuzla supports three kinds of options: Boolean options, numeric options and options with option modes. The kind of an option can be queried via bitwuzla.Options.is_bool(), bitwuzla.Options.is_numeric(), and bitwuzla.Options.is_mode().

All options are configured via bitwuzla.Options.set(). Additionally, it is also possible to configure options in batch via bitwuzla.Options.set_args(), where the given arguments are each a command line option configuration string, e.g., set_args("-i", "--produce-models=true", "--produce-unsat-cores true").

The configured value of options can be queried via bitwuzla.Options.get().

The short name of an option can be queried via bitwuzla.Options.shrt(), its long name via bitwuzla.Options.lng(), its description via bitwuzla.Options.description(), and, if given option is an option with modes, its modes can be queried via bitwuzla.Options.modes().

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

Example

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

###
# Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
#
# Copyright (C) 2023 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
##

from bitwuzla import *

if __name__ == '__main__':

    # First, create a Bitwuzla options instance.
    options = Options()

    # Enable model generation, which expects a boolean configuration value.
    options.set(Option.PRODUCE_MODELS, True)

    # Increase the verbosity level, which expects an integer value.
    print(f'Previous verbosity level: {options.get(Option.VERBOSITY)}')
    options.set(Option.VERBOSITY, 2)
    print(f'Current verbosity level: {options.get(Option.VERBOSITY)}')

    # Now configure an option that has modes (a choice of configuration values).
    # First, query which bit-vector solver engine is set.
    print(f'Default bv solver: {options.get(Option.BV_SOLVER)}')
    # Then, select the propagation-based local search engine as solver engine.
    options.set(Option.BV_SOLVER, 'prop')
    print(f'Current engine: {options.get(Option.BV_SOLVER)}')

    # Now, create a Bitwuzla instance.
    tm = TermManager()
    bitwuzla = Bitwuzla(tm, options)
    # Check sat (nothing to solve, input formula is empty).
    result = bitwuzla.check_sat()
    print('Expect: sat')
    print(f'Bitwuzla: {result}')