1 /*-----------------------------------------------------------------------
2
3 File : cte_subst.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 General functions for substitutions.
10
11 Copyright 1998, 1999 by the author.
12 This code is released under the GNU General Public Licence and
13 the GNU Lesser General Public License.
14 See the file COPYING in the main E directory for details..
15 Run "eprover -h" for contact information.
16
17 Changes
18
19 <1> Thu Mar 5 00:22:28 MET 1998
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "cte_subst.h"
25 #include "clb_plocalstacks.h"
26
27
28
29 /*---------------------------------------------------------------------*/
30 /* Global Variables */
31 /*---------------------------------------------------------------------*/
32
33
34 /*---------------------------------------------------------------------*/
35 /* Forward Declarations */
36 /*---------------------------------------------------------------------*/
37
38
39 /*---------------------------------------------------------------------*/
40 /* Internal Functions */
41 /*---------------------------------------------------------------------*/
42
43
44
45 /*---------------------------------------------------------------------*/
46 /* Exported Functions */
47 /*---------------------------------------------------------------------*/
48
49 /*-----------------------------------------------------------------------
50 //
51 // Function: SubstBacktrackSingle()
52 //
53 // Backtrack a single binding and remove it from the substitution
54 /// (if possible). Return true if successful, false if the
55 // substitutuion is empty.
56 //
57 // Global Variables: -
58 //
59 // Side Effects : As SubstAddBinding()
60 //
61 /----------------------------------------------------------------------*/
62
SubstBacktrackSingle(Subst_p subst)63 bool SubstBacktrackSingle(Subst_p subst)
64 {
65 Term_p handle;
66
67 assert(subst);
68
69 if(PStackEmpty(subst))
70 {
71 return false;
72 }
73 handle = PStackPopP(subst);
74 handle->binding = NULL;
75
76 return true;
77 }
78
79 /*-----------------------------------------------------------------------
80 //
81 // Function: SubstBacktrackToPos()
82 //
83 // Backtrack variable bindings up to (down to?) a given stack
84 // pointer position.
85 //
86 // Global Variables: -
87 //
88 // Side Effects :
89 //
90 /----------------------------------------------------------------------*/
91
SubstBacktrackToPos(Subst_p subst,PStackPointer pos)92 int SubstBacktrackToPos(Subst_p subst, PStackPointer pos)
93 {
94 int ret = 0;
95
96 while(PStackGetSP(subst) > pos)
97 {
98 SubstBacktrackSingle(subst);
99 ret++;
100 }
101 return ret;
102 }
103
104 /*-----------------------------------------------------------------------
105 //
106 // Function: SubstBacktrack()
107 //
108 // Undo all stored variable binding in subst.
109 //
110 // Global Variables: -
111 //
112 // Side Effects : As noted...
113 //
114 /----------------------------------------------------------------------*/
115
SubstBacktrack(Subst_p subst)116 int SubstBacktrack(Subst_p subst)
117 {
118 int ret = 0;
119
120 while(SubstBacktrackSingle(subst))
121 {
122 ret++;
123 }
124 return ret;
125 }
126
127
128 /*-----------------------------------------------------------------------
129 //
130 // Function: SubstNormTerm()
131 //
132 // Instatiate all variables in term with fresh variables from the
133 // VarBank. Return the current position of the substitution stack, so that
134 // SubstBacktrackToPos() can be used to backtrack the
135 // instantiations term by term. New variables are marked by
136 // TPSpecialFlag, if other variables are marked thus the effect is
137 // unpredictable.
138 //
139 // Warning: As variables may be shared, other terms may be affected!
140 // Take care...your best bet is to norm all terms you need with a
141 // single substitution. If you need independendly normed terms, you
142 // need to work with copy/backtrack operations (it's still better
143 // than working with unshared terms).
144 //
145 // Global Variables: -
146 //
147 // Side Effects : Instantiates variables
148 //
149 /----------------------------------------------------------------------*/
150
SubstNormTerm(Term_p term,Subst_p subst,VarBank_p vars)151 PStackPointer SubstNormTerm(Term_p term, Subst_p subst, VarBank_p vars)
152 {
153 PStackPointer ret = PStackGetSP(subst);
154 PLocalStackInit(stack);
155 PLocalStackPush(stack, term);
156
157 while(!PLocalStackEmpty(stack))
158 {
159 term = TermDerefAlways(PLocalStackPop(stack));
160 if(TermIsVar(term))
161 {
162 if(!TermCellQueryProp(term, TPSpecialFlag))
163 {
164 Term_p newvar = VarBankGetFreshVar(vars, term->sort);
165 TermCellSetProp(newvar, TPSpecialFlag);
166 SubstAddBinding(subst, term, newvar);
167 }
168 }
169 else
170 {
171 PLocalStackPushTermArgsReversed(stack, term);
172 }
173 }
174
175 PLocalStackFree(stack);
176 return ret;
177 }
178
179
180 /*-----------------------------------------------------------------------
181 //
182 // Function: SubstBindingPrint()
183 //
184 // Print a variable and its binding as x<-binding. Return true if
185 // variable is bound. See comments on SubstPrint()!
186 //
187 // Global Variables: -
188 //
189 // Side Effects : Output
190 //
191 /----------------------------------------------------------------------*/
192
SubstBindingPrint(FILE * out,Term_p var,Sig_p sig,DerefType deref)193 bool SubstBindingPrint(FILE* out, Term_p var, Sig_p sig, DerefType
194 deref)
195 {
196 TermPrint(out, var, sig, DEREF_NEVER);
197 fprintf(out, "<-");
198 if(var->binding)
199 {
200 TermPrint(out, var->binding, sig, deref);
201 return true;
202 }
203 TermPrint(out, var, sig, DEREF_NEVER);
204 return false;
205 }
206
207
208 /*-----------------------------------------------------------------------
209 //
210 // Function: SubstPrint()
211 //
212 // Print a substitution. Note: Due to the different interpretations
213 // of terms (follow/ignore bindings) and share variable, printing
214 // substitutions with deref=DEREF_ALWAYS may lead to
215 // unpredictable behaviour (if e.g. the substitution was generated
216 // by matching x onto f(x)). Returns number of variables in subst
217 // (well, why not...).
218 //
219 // Global Variables: -
220 //
221 // Side Effects : Output
222 //
223 /----------------------------------------------------------------------*/
224
SubstPrint(FILE * out,Subst_p subst,Sig_p sig,DerefType deref)225 long SubstPrint(FILE* out, Subst_p subst, Sig_p sig, DerefType deref)
226 {
227 PStackPointer i, limit;
228
229 limit = PStackGetSP(subst);
230 fprintf(out, "{");
231 if(limit)
232 {
233 SubstBindingPrint(out, PStackElementP(subst,0), sig, deref);
234 {
235 for(i=1; i<limit;i++)
236 {
237 fprintf(out, ", ");
238 SubstBindingPrint(out, PStackElementP(subst,i), sig,
239 deref);
240 }
241 }
242 }
243 fprintf(out, "}");
244
245 return (long)limit;
246 }
247
248
249 /*-----------------------------------------------------------------------
250 //
251 // Function: SubstIsRenaming()
252 //
253 // Return true if subst is just a variable renaming, false
254 // otherwise. A substitution is a renaming if all variables are
255 // instantiated to different variables. Checks only for one level of
256 // instantiaton.
257 //
258 // Global Variables: -
259 //
260 // Side Effects : Changes the TPOpFlag of terms
261 //
262 /----------------------------------------------------------------------*/
263
SubstIsRenaming(Subst_p subst)264 bool SubstIsRenaming(Subst_p subst)
265 {
266 PStackPointer i, size;
267 Term_p var, inst;
268 DerefType deref;
269
270 assert(subst);
271 size = PStackGetSP(subst);
272
273 /* Check that variables are instantiated with variables, reset
274 TPOpFlag of all terms concerned */
275
276 for(i=0; i< size; i++)
277 {
278 var = PStackElementP(subst,i);
279 assert(TermIsVar(var));
280 assert(var->binding);
281 deref=DEREF_ONCE;
282 inst = TermDeref(var, &deref);
283
284 if(!TermIsVar(inst))
285 {
286 return false;
287 }
288 TermCellDelProp(inst, TPOpFlag);
289 }
290
291 /* For each unchecked variable, check wether another variable was
292 already mapped to its instantiation */
293
294 for(i=0; i< size; i++)
295 {
296 var = PStackElementP(subst,i);
297 deref=DEREF_ONCE;
298 inst = TermDeref(var, &deref);
299
300 if(TermCellQueryProp(inst, TPOpFlag))
301 {
302 return false;
303 }
304 TermCellSetProp(inst, TPOpFlag);
305 }
306 return true;
307 }
308
309
310 /*-----------------------------------------------------------------------
311 //
312 // Function: SubstBacktrackSkolem()
313 //
314 // Backtrack a skolem subst, freeing the skolem terms along the way.
315 //
316 // Global Variables: -
317 //
318 // Side Effects : -
319 //
320 /----------------------------------------------------------------------*/
321
SubstBacktrackSkolem(Subst_p subst)322 void SubstBacktrackSkolem(Subst_p subst)
323 {
324 Term_p handle;
325
326 while(!PStackEmpty(subst))
327 {
328 handle = PStackPopP(subst);
329 assert(handle);
330 assert(handle->binding);
331 TermFree(handle->binding);
332 handle->binding = NULL;
333 }
334 }
335
336 /*-----------------------------------------------------------------------
337 //
338 // Function: SubstSkolemize()
339 //
340 // Instantiate all variables in term with new skolem symbols from
341 // sig.
342 //
343 // Global Variables: -
344 //
345 // Side Effects : Changes sig, creates skolem terms.
346 //
347 /----------------------------------------------------------------------*/
348
SubstSkolemizeTerm(Term_p term,Subst_p subst,Sig_p sig)349 void SubstSkolemizeTerm(Term_p term, Subst_p subst, Sig_p sig)
350 {
351 int i;
352
353 assert(term && subst && sig);
354
355 if(TermIsVar(term))
356 {
357 if(!(term->binding))
358 {
359 PStackPushP(subst, term);
360 term->binding =
361 TermConstCellAlloc(SigGetNewSkolemCode(sig,0));
362 }
363 }
364 else
365 {
366 for(i=0;i<term->arity;i++)
367 {
368 SubstSkolemizeTerm(term->args[i], subst, sig);
369 }
370 }
371 }
372
373
374 /*-----------------------------------------------------------------------
375 //
376 // Function: SubstCompleteInstance()
377 //
378 // Add bindings for all free variables in term subst, binding them
379 // to default_term.
380 //
381 // Global Variables: -
382 //
383 // Side Effects : Changes subst.
384 //
385 /----------------------------------------------------------------------*/
386
SubstCompleteInstance(Subst_p subst,Term_p term,Term_p default_binding)387 void SubstCompleteInstance(Subst_p subst, Term_p term,
388 Term_p default_binding)
389 {
390 int i;
391
392 if(TermIsVar(term))
393 {
394 if(!(term->binding))
395 {
396 SubstAddBinding(subst, term, default_binding);
397 }
398 }
399 else
400 {
401 for(i=0;i<term->arity;i++)
402 {
403 SubstCompleteInstance(subst, term->args[i], default_binding);
404 }
405 }
406 }
407
408 /*---------------------------------------------------------------------*/
409 /* End of File */
410 /*---------------------------------------------------------------------*/
411
412
413
414
415