1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #ifdef _WINDOWS
8 #include "api/z3.h"
9 #include "api/z3_private.h"
10 #include <iostream>
11 #include "util/util.h"
12 #include "util/trace.h"
13 #include <map>
14 #include "util/trace.h"
15
test_apps()16 void test_apps() {
17 Z3_config cfg = Z3_mk_config();
18 Z3_set_param_value(cfg,"MODEL","true");
19 Z3_context ctx = Z3_mk_context(cfg);
20 Z3_solver s = Z3_mk_solver(ctx);
21 Z3_solver_inc_ref(ctx, s);
22 Z3_symbol A = Z3_mk_string_symbol(ctx, "A");
23 Z3_symbol F = Z3_mk_string_symbol(ctx, "f");
24 Z3_sort SA = Z3_mk_uninterpreted_sort(ctx, A);
25 Z3_func_decl f = Z3_mk_func_decl(ctx, F, 1, &SA, SA);
26 Z3_symbol X = Z3_mk_string_symbol(ctx, "x");
27 Z3_ast x = Z3_mk_const(ctx, X, SA);
28 Z3_ast fx = Z3_mk_app(ctx, f, 1, &x);
29 Z3_ast ffx = Z3_mk_app(ctx, f, 1, &fx);
30 Z3_ast fffx = Z3_mk_app(ctx, f, 1, &ffx);
31 Z3_ast ffffx = Z3_mk_app(ctx, f, 1, &fffx);
32 Z3_ast fffffx = Z3_mk_app(ctx, f, 1, &ffffx);
33
34 Z3_ast fml = Z3_mk_not(ctx, Z3_mk_eq(ctx, x, fffffx));
35
36 Z3_solver_assert(ctx, s, fml);
37 Z3_lbool r = Z3_solver_check(ctx, s);
38 std::cout << r << "\n";
39 Z3_solver_dec_ref(ctx, s);
40 Z3_del_config(cfg);
41 Z3_del_context(ctx);
42 }
43
test_bvneg()44 void test_bvneg() {
45 Z3_config cfg = Z3_mk_config();
46 Z3_set_param_value(cfg,"MODEL","true");
47 Z3_context ctx = Z3_mk_context(cfg);
48 Z3_solver s = Z3_mk_solver(ctx);
49 Z3_solver_inc_ref(ctx, s);
50
51 {
52 Z3_sort bv30 = Z3_mk_bv_sort(ctx, 30);
53 Z3_ast x30 = Z3_mk_fresh_const(ctx, "x", bv30);
54 Z3_ast fml = Z3_mk_eq(ctx, Z3_mk_int(ctx, -1, bv30),
55 Z3_mk_bvadd(ctx, Z3_mk_int(ctx, 0, bv30),
56 x30));
57 Z3_solver_assert(ctx, s, fml);
58 Z3_lbool r = Z3_solver_check(ctx, s);
59 std::cout << r << "\n";
60 }
61
62 {
63 Z3_sort bv31 = Z3_mk_bv_sort(ctx, 31);
64 Z3_ast x31 = Z3_mk_fresh_const(ctx, "x", bv31);
65 Z3_ast fml = Z3_mk_eq(ctx, Z3_mk_int(ctx, -1, bv31),
66 Z3_mk_bvadd(ctx, Z3_mk_int(ctx, 0, bv31),
67 x31));
68 Z3_solver_assert(ctx, s, fml);
69 Z3_lbool r = Z3_solver_check(ctx, s);
70 std::cout << r << "\n";
71 }
72
73 {
74 Z3_sort bv32 = Z3_mk_bv_sort(ctx, 32);
75 Z3_ast x32 = Z3_mk_fresh_const(ctx, "x", bv32);
76 Z3_ast fml = Z3_mk_eq(ctx,
77 Z3_mk_int(ctx,-1, bv32),
78 Z3_mk_bvadd(ctx, Z3_mk_int(ctx, 0, bv32),
79 x32));
80 Z3_solver_assert(ctx, s, fml);
81 Z3_lbool r = Z3_solver_check(ctx, s);
82 std::cout << r << "\n";
83 }
84
85 Z3_solver_dec_ref(ctx, s);
86 Z3_del_config(cfg);
87 Z3_del_context(ctx);
88 }
89
90 static bool cb_called = false;
my_cb(Z3_context,Z3_error_code)91 static void my_cb(Z3_context, Z3_error_code) {
92 cb_called = true;
93 }
94
test_mk_distinct()95 static void test_mk_distinct() {
96 Z3_config cfg = Z3_mk_config();
97 Z3_context ctx = Z3_mk_context(cfg);
98 Z3_set_error_handler(ctx, my_cb);
99
100 Z3_sort bv8 = Z3_mk_bv_sort(ctx, 8);
101 Z3_sort bv32 = Z3_mk_bv_sort(ctx, 32);
102 Z3_ast args[] = { Z3_mk_int64(ctx, 0, bv8), Z3_mk_int64(ctx, 0, bv32) };
103 Z3_ast d = Z3_mk_distinct(ctx, 2, args);
104 ENSURE(cb_called);
105 Z3_del_config(cfg);
106 Z3_del_context(ctx);
107
108 }
109
tst_api()110 void tst_api() {
111 test_apps();
112 test_bvneg();
113 test_mk_distinct();
114 }
115 #else
tst_api()116 void tst_api() {
117 }
118 #endif
119