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
|
/***
* 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
*/
#include <bitwuzla/cpp/bitwuzla.h>
#include <iostream>
using namespace bitwuzla;
int
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.
std::cout << "Previous verbosity level: " << options.get(Option::VERBOSITY)
<< std::endl;
options.set(Option::VERBOSITY, 2);
std::cout << "Current verbosity level: " << options.get(Option::VERBOSITY)
<< std::endl;
// Now configure an option that has modes (a choice of configuration values).
// First, query which bit-vector solver engine is set.
std::cout << "Default bv solver: " << options.get_mode(Option::BV_SOLVER)
<< std::endl;
// Then, select the propagation-based local search engine as solver engine.
options.set(Option::BV_SOLVER, "prop");
std::cout << "Current engine: " << options.get_mode(Option::BV_SOLVER)
<< std::endl;
// Now, create a Bitwuzla instance with a new term manager.
TermManager tm;
Bitwuzla bitwuzla(tm, options);
// Check sat (nothing to solve, input formula is empty).
Result result = bitwuzla.check_sat();
std::cout << "Expect: sat" << std::endl;
std::cout << "Bitwuzla: " << result << std::endl;
return 0;
}
|
