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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
/***
* 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;
}
|
