1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include "api/z3.h"
8 #include "util/trace.h"
9 #include "util/debug.h"
10
mk_var(Z3_context ctx,char const * name,Z3_sort s)11 static Z3_ast mk_var(Z3_context ctx, char const* name, Z3_sort s) {
12 return Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, name), s);
13 }
14
mk_int_var(Z3_context ctx,char const * name)15 static Z3_ast mk_int_var(Z3_context ctx, char const* name) {
16 return mk_var(ctx, name, Z3_mk_int_sort(ctx));
17 }
18
19
20
tst_get_implied_equalities1()21 static void tst_get_implied_equalities1() {
22 Z3_config cfg = Z3_mk_config();
23 Z3_context ctx = Z3_mk_context(cfg);
24 Z3_del_config(cfg);
25 Z3_sort int_ty = Z3_mk_int_sort(ctx);
26 Z3_ast a = mk_int_var(ctx,"a");
27 Z3_ast b = mk_int_var(ctx,"b");
28 Z3_ast c = mk_int_var(ctx,"c");
29 Z3_ast d = mk_int_var(ctx,"d");
30 Z3_func_decl f = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx,"f"), 1, &int_ty, int_ty);
31 Z3_ast fa = Z3_mk_app(ctx, f, 1, &a);
32 Z3_ast fb = Z3_mk_app(ctx, f, 1, &b);
33 Z3_ast fc = Z3_mk_app(ctx, f, 1, &c);
34 unsigned const num_terms = 7;
35 unsigned i;
36 Z3_ast terms[7] = { a, b, c, d, fa, fb, fc };
37 unsigned class_ids[7] = { 0, 0, 0, 0, 0, 0, 0 };
38 Z3_solver solver = Z3_mk_simple_solver(ctx);
39 Z3_solver_inc_ref(ctx, solver);
40
41 Z3_solver_assert(ctx, solver, Z3_mk_eq(ctx, a, b));
42 Z3_solver_assert(ctx, solver, Z3_mk_eq(ctx, b, d));
43 Z3_solver_assert(ctx, solver, Z3_mk_le(ctx, fa, fc));
44 Z3_solver_assert(ctx, solver, Z3_mk_le(ctx, fc, d));
45
46 Z3_get_implied_equalities(ctx, solver, num_terms, terms, class_ids);
47 for (i = 0; i < num_terms; ++i) {
48 printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]);
49 }
50 ENSURE(class_ids[1] == class_ids[0]);
51 ENSURE(class_ids[2] != class_ids[0]);
52 ENSURE(class_ids[3] == class_ids[0]);
53 ENSURE(class_ids[4] != class_ids[0]);
54 ENSURE(class_ids[5] != class_ids[0]);
55 ENSURE(class_ids[6] != class_ids[0]);
56 ENSURE(class_ids[4] == class_ids[5]);
57
58 printf("asserting b <= f(a)\n");
59 Z3_solver_assert(ctx, solver, Z3_mk_le(ctx, b, fa));
60 Z3_get_implied_equalities(ctx, solver, num_terms, terms, class_ids);
61 for (i = 0; i < num_terms; ++i) {
62 printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]);
63 }
64 ENSURE(class_ids[1] == class_ids[0]);
65 ENSURE(class_ids[2] != class_ids[0]);
66 ENSURE(class_ids[3] == class_ids[0]);
67 ENSURE(class_ids[4] == class_ids[0]);
68 ENSURE(class_ids[5] == class_ids[0]);
69 ENSURE(class_ids[6] == class_ids[0]);
70
71
72 Z3_solver_dec_ref(ctx, solver);
73 /* delete logical context */
74 Z3_del_context(ctx);
75 }
76
tst_get_implied_equalities2()77 static void tst_get_implied_equalities2() {
78 //enable_trace("after_search");
79 //enable_trace("get_implied_equalities");
80 //enable_trace("implied_equalities");
81 Z3_config cfg = Z3_mk_config();
82 Z3_context ctx = Z3_mk_context(cfg);
83 Z3_del_config(cfg);
84 Z3_solver solver = Z3_mk_simple_solver(ctx);
85 Z3_solver_inc_ref(ctx, solver);
86 Z3_sort int_ty = Z3_mk_int_sort(ctx);
87 Z3_ast a = mk_int_var(ctx,"a");
88 Z3_ast b = mk_int_var(ctx,"b");
89 Z3_ast one = Z3_mk_numeral(ctx, "1", int_ty);
90 Z3_ast two = Z3_mk_numeral(ctx, "2", int_ty);
91 Z3_ast x = Z3_mk_const_array(ctx, int_ty, one);
92 Z3_ast y = Z3_mk_store(ctx, x, one, a);
93 Z3_ast z = Z3_mk_store(ctx, y, two , b);
94 Z3_ast u = Z3_mk_store(ctx, x, two , b);
95 Z3_ast v = Z3_mk_store(ctx, u, one , a);
96 unsigned const num_terms = 5;
97 unsigned i;
98 Z3_ast terms[5] = { x, y, z, u, v};
99 unsigned class_ids[5] = { 0, 0, 0, 0, 0};
100
101 Z3_get_implied_equalities(ctx, solver, num_terms, terms, class_ids);
102 for (i = 0; i < num_terms; ++i) {
103 printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]);
104 }
105
106 ENSURE(class_ids[1] != class_ids[0]);
107 ENSURE(class_ids[2] != class_ids[0]);
108 ENSURE(class_ids[3] != class_ids[0]);
109 ENSURE(class_ids[4] != class_ids[0]);
110 ENSURE(class_ids[4] == class_ids[2]);
111 ENSURE(class_ids[2] != class_ids[1]);
112 ENSURE(class_ids[3] != class_ids[1]);
113 ENSURE(class_ids[4] != class_ids[1]);
114 ENSURE(class_ids[3] != class_ids[2]);
115
116 /* delete logical context */
117 Z3_solver_dec_ref(ctx, solver);
118 Z3_del_context(ctx);
119 }
120
tst_get_implied_equalities()121 void tst_get_implied_equalities() {
122 tst_get_implied_equalities1();
123 tst_get_implied_equalities2();
124 }
125