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 * Variable renaming for substitutions
21 */
22
23 #include <assert.h>
24
25 #include "terms/renaming_context.h"
26
27 /*
28 * Initialization:
29 * - ttbl = attached term table
30 * - n = initial size of the substitution table
31 * if n=0, the default size (defined in subst_context.h) is used.
32 */
init_renaming_ctx(renaming_ctx_t * ctx,term_table_t * ttbl,uint32_t n)33 void init_renaming_ctx(renaming_ctx_t *ctx, term_table_t *ttbl, uint32_t n) {
34 init_subst_ctx(&ctx->subst, n);
35 init_renaming(&ctx->rename, ttbl);
36 ctx->hash = NULL;
37 }
38
39
40 /*
41 * Deletion
42 */
delete_renaming_ctx(renaming_ctx_t * ctx)43 void delete_renaming_ctx(renaming_ctx_t *ctx) {
44 delete_subst_ctx(&ctx->subst);
45 delete_renaming(&ctx->rename);
46 ctx->hash = NULL;
47 }
48
49
50 /*
51 * Full reset
52 */
reset_renaming_ctx(renaming_ctx_t * ctx)53 void reset_renaming_ctx(renaming_ctx_t *ctx) {
54 reset_subst_ctx(&ctx->subst, true);
55 reset_renaming(&ctx->rename);
56 ctx->hash = NULL;
57 }
58
59
60 /*
61 * Extend the renaming:
62 * - replace variables in v[0 ... n-1] by n fresh variables.
63 */
renaming_ctx_push_vars(renaming_ctx_t * ctx,uint32_t n,term_t * v)64 void renaming_ctx_push_vars(renaming_ctx_t *ctx, uint32_t n, term_t *v) {
65 uint32_t i;
66 term_t x, y;
67
68 for (i=0; i<n; i++) {
69 x = v[i];
70 y = get_var_renaming(&ctx->rename, x); // x is now renamed to y
71 subst_ctx_push_binding(&ctx->subst, x, y);
72 }
73
74 ctx->hash = NULL;
75 }
76
77
78 /*
79 * Remove the last n variable renamings
80 */
renaming_ctx_pop_vars(renaming_ctx_t * ctx,uint32_t n)81 void renaming_ctx_pop_vars(renaming_ctx_t *ctx, uint32_t n) {
82 ctx_binding_t *b;
83 uint32_t i, m;
84
85 assert(n <= ctx->subst.nelems);
86
87 // clear the last n variable renamings in ctx->renaming
88 b = ctx->subst.data;
89 i = ctx->subst.nelems;
90 m = i - n;
91 while (i > m) {
92 i --;
93 clear_var_renaming(&ctx->rename, b[i].var);
94 }
95
96 // remove the last n bindings in ctx->subst
97 subst_ctx_pop_bindings(&ctx->subst, n);
98
99 ctx->hash = NULL;
100 }
101
102
103 /*
104 * Hash code of the current renaming
105 */
renaming_ctx_hash(renaming_ctx_t * ctx)106 harray_t *renaming_ctx_hash(renaming_ctx_t *ctx) {
107 harray_t *tmp;
108
109 tmp = ctx->hash;
110 if (tmp == NULL) {
111 tmp = subst_ctx_hash(&ctx->subst);
112 ctx->hash = tmp;
113 }
114
115 return tmp;
116 }
117