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
56
57
58
59
60
61
62
63
64
65
66
67
|
/***
* Bitwuzla: Satisfiability Modulo Theories (SMT) solver.
*
* Copyright (C) 2024 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 <stdio.h>
#include <assert.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();
bitwuzla_set_option(options, BITWUZLA_OPT_PRODUCE_MODELS, 1);
// Then, create a Bitwuzla instance.
Bitwuzla *bitwuzla = bitwuzla_new(tm, options);
BitwuzlaSort sortb = bitwuzla_mk_bool_sort(tm);
BitwuzlaTerm a = bitwuzla_mk_const(tm, sortb, "a");
BitwuzlaTerm b = bitwuzla_mk_const(tm, sortb, "b");
// Release sort reference.
bitwuzla_sort_release(sortb);
BitwuzlaTerm dis = bitwuzla_mk_term2(tm, BITWUZLA_KIND_DISTINCT, a, b);
bitwuzla_assert(bitwuzla, dis);
bitwuzla_check_sat(bitwuzla);
// Release term reference.
bitwuzla_term_release(dis);
BitwuzlaTerm val_a = bitwuzla_get_value(bitwuzla, a);
BitwuzlaTerm val_b = bitwuzla_get_value(bitwuzla, b);
assert(val_a != val_b);
printf("value a: %s\n", bitwuzla_term_to_string(val_a));
printf("value b: %s\n", bitwuzla_term_to_string(val_b));
// Release remaining term references.
bitwuzla_term_release(val_a);
bitwuzla_term_release(val_b);
bitwuzla_term_release(a);
bitwuzla_term_release(b);
// At this point all sort and term references have been released. If all sort
// and term references should be released at once we can also use the
// following function.
bitwuzla_term_manager_release(tm);
// Finally, delete the Bitwuzla solver, options, and term manager instances.
bitwuzla_delete(bitwuzla);
bitwuzla_options_delete(options);
// Note: All sorts and terms not released until now will be released when
// deleting the term manager.
bitwuzla_term_manager_delete(tm);
return 0;
}
|
