1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
###
# 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}')
|
