1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * Renaming context
21 */
22
23 #include <assert.h>
24 #include <stdio.h>
25 #include <stdint.h>
26 #include <inttypes.h>
27
28 #include "terms/pprod_table.h"
29 #include "terms/renaming_context.h"
30 #include "terms/terms.h"
31 #include "terms/types.h"
32
33
34 /*
35 * Global variables
36 */
37 static type_table_t types;
38 static pprod_table_t pprods;
39 static term_table_t terms;
40 static renaming_ctx_t ctx;
41
42 // array of variables
43 #define NVARS 10
44 static term_t var[NVARS];
45
46
47 /*
48 * Initialize all
49 */
init(void)50 static void init(void) {
51 init_type_table(&types, 10);
52 init_pprod_table(&pprods, 0);
53 init_term_table(&terms, 20, &types, &pprods);
54 init_renaming_ctx(&ctx, &terms, 1);
55 }
56
57
58 /*
59 * Delete all
60 */
delete(void)61 static void delete(void) {
62 delete_renaming_ctx(&ctx);
63 delete_term_table(&terms);
64 delete_pprod_table(&pprods);
65 delete_type_table(&types);
66 }
67
68
69 /*
70 * Initialize the variable array
71 */
init_variables(void)72 static void init_variables(void) {
73 type_t tau;
74 uint32_t i;
75
76 tau = int_type(&types);
77 for (i=0; i<NVARS; i++) {
78 var[i] = new_variable(&terms, tau);
79 }
80 }
81
82
83 /*
84 * Display the current renaming + harray and hash code
85 */
show_renaming(void)86 static void show_renaming(void) {
87 harray_t *h;
88 uint32_t i;
89 int32_t x, y;
90
91 printf("renaming:\n");
92 for (i=0; i<NVARS; i++) {
93 x = var[i];
94 y = renaming_ctx_lookup(&ctx, x);
95 if (y >= 0) {
96 printf("x_%"PRId32" --> x_%"PRId32"\n", x, y);
97 }
98 }
99
100 h = renaming_ctx_hash(&ctx);
101 printf("hash: %p\n", h);
102 for (i=0; i<h->nelems; i += 2) {
103 x = h->data[i];
104 y = h->data[i+1];
105 printf("x_%"PRId32" --> x_%"PRId32"\n", x, y);
106 }
107
108 printf("---\n");
109 }
110
111
112 /*
113 * Test: add renaming for vars[i] to var[i+n-1]
114 */
test_add(uint32_t i,uint32_t n)115 static void test_add(uint32_t i, uint32_t n) {
116 uint32_t j;
117 term_t x;
118
119 assert(i + n <= NVARS && n>0);
120
121 printf("Test renaming:");
122 for (j=i; j<i+n; j++) {
123 x = var[j];
124 printf(" x_%"PRId32, x);
125 }
126 printf("\n");
127
128 renaming_ctx_push_vars(&ctx, n, var + i);
129 show_renaming();
130 printf("\n");
131 }
132
133
134 /*
135 * Test: remove last n renamings
136 */
test_remove(uint32_t n)137 static void test_remove(uint32_t n) {
138 printf("Test pop last %"PRIu32" renamings\n", n);
139 renaming_ctx_pop_vars(&ctx, n);
140 show_renaming();
141 printf("\n");
142 }
143
main(void)144 int main(void) {
145 uint32_t n;
146
147 init();
148 init_variables();
149
150 printf("Initial context\n");
151 show_renaming();
152 printf("\n");
153
154 for (n=0; n<NVARS-5; n++) {
155 test_add(n, 5);
156 }
157 for (n=0; n<NVARS-5; n++) {
158 test_remove(5);
159 }
160
161 for (n=0; n<NVARS-5; n++) {
162 test_add(n, 5);
163 }
164 for (n=0; n<NVARS-5; n++) {
165 test_remove(5);
166 }
167
168
169 delete();
170
171 return 0;
172 }
173