1 /*-----------------------------------------------------------------------
2
3 File : cte_termtypes.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Declarations for the basic term type and primitive functions, mainly
10 on single term cells. This module mostly provides only
11 infrastructure for higher level modules.
12
13
14 Copyright 1998, 1999 by the author.
15 This code is released under the GNU General Public Licence and
16 the GNU Lesser General Public License.
17 See the file COPYING in the main E directory for details..
18 Run "eprover -h" for contact information.
19
20 Created: Tue Feb 24 02:17:11 MET 1998 - Split from cte_terms.c
21
22 -----------------------------------------------------------------------*/
23
24 #include "cte_termtypes.h"
25
26
27 /*---------------------------------------------------------------------*/
28 /* Global Variables */
29 /*---------------------------------------------------------------------*/
30
31
32 /*---------------------------------------------------------------------*/
33 /* Forward Declarations */
34 /*---------------------------------------------------------------------*/
35
36
37 /*---------------------------------------------------------------------*/
38 /* Internal Functions */
39 /*---------------------------------------------------------------------*/
40
41
42 /*---------------------------------------------------------------------*/
43 /* Exported Functions */
44 /*---------------------------------------------------------------------*/
45
46
47 /*-----------------------------------------------------------------------
48 //
49 // Function: TermTopFree()
50 //
51 // Return term cell and arg array (if it exists).
52 //
53 // Global Variables: -
54 //
55 // Side Effects : Memory operations
56 //
57 /----------------------------------------------------------------------*/
58
TermTopFree(Term_p junk)59 void TermTopFree(Term_p junk)
60 {
61 if(junk->arity)
62 {
63 assert(junk->args);
64 TermArgArrayFree(junk->args, junk->arity);
65 }
66 else
67 {
68 assert(!junk->args);
69 }
70 TermCellFree(junk);
71 }
72
73 /*-----------------------------------------------------------------------
74 //
75 // Function: TermFree()
76 //
77 // Return the memory taken by an (unshared) term. Does not free the
78 // variable cells, which belong to a VarBank.
79 //
80 // Global Variables: -
81 //
82 // Side Effects : Memory operations
83 //
84 /----------------------------------------------------------------------*/
85
TermFree(Term_p junk)86 void TermFree(Term_p junk)
87 {
88 assert(junk);
89 if(!TermIsVar(junk))
90 {
91 assert(!TermCellQueryProp(junk, TPIsShared));
92 if(junk->arity)
93 {
94 int i;
95
96 assert(junk->args);
97 for(i=0; i<junk->arity; i++)
98 {
99 TermFree(junk->args[i]);
100 }
101 }
102 else
103 {
104 assert(!junk->args);
105 }
106 TermTopFree(junk);
107 }
108 }
109
110
111 /*-----------------------------------------------------------------------
112 //
113 // Function: TermNewSkolemTerm()
114 //
115 // Create a new Skolem term (or renaming atom) with the named
116 // variables as arguments.
117 //
118 // Global Variables: -
119 //
120 // Side Effects : Memory operations, creates new Skolem function in
121 // sig.
122 //
123 /----------------------------------------------------------------------*/
124
TermAllocNewSkolem(Sig_p sig,PStack_p variables,SortType sort)125 Term_p TermAllocNewSkolem(Sig_p sig, PStack_p variables, SortType sort)
126 {
127 Term_p handle = TermDefaultCellAlloc();
128 PStackPointer arity = PStackGetSP(variables), i;
129 Type_p type;
130 SortType *type_args;
131
132 if(sort == STNoSort)
133 {
134 sort = SigDefaultSort(sig);
135 }
136
137 if(sort != STBool)
138 {
139 handle->f_code = SigGetNewSkolemCode(sig, arity);
140 }
141 else
142 {
143 handle->f_code = SigGetNewPredicateCode(sig, arity);
144 }
145
146 // declare type
147 if(arity)
148 {
149 handle->arity = arity;
150 handle->args = TermArgArrayAlloc(arity);
151 type_args = TypeArgumentAlloc(arity);
152 for(i=0; i<arity; i++)
153 {
154 handle->args[i] = PStackElementP(variables, i);
155 type_args[i] = handle->args[i]->sort;
156 assert(type_args[i] != STNoSort);
157 }
158 type = TypeNewFunction(sig->type_table, sort, arity, type_args);
159 TypeArgumentFree(type_args, arity);
160 }
161 else
162 {
163 type = TypeNewConstant(sig->type_table, sort);
164 }
165 SigDeclareType(sig, handle->f_code, type);
166 handle->sort = sort;
167
168 return handle;
169 }
170
171
172 /*-----------------------------------------------------------------------
173 //
174 // Function: TermSetProp()
175 //
176 // Set the properties in all term cells belonging to term.
177 //
178 // Global Variables: -
179 //
180 // Side Effects : Changes properties (even in shared terms! Beware!)
181 //
182 /----------------------------------------------------------------------*/
183
TermSetProp(Term_p term,DerefType deref,TermProperties prop)184 void TermSetProp(Term_p term, DerefType deref, TermProperties prop)
185 {
186 PStack_p stack = PStackAlloc();
187 int i;
188
189 PStackPushP(stack, term);
190 PStackPushInt(stack, deref);
191
192 while(!PStackEmpty(stack))
193 {
194 deref = PStackPopInt(stack);
195 term = PStackPopP(stack);
196 term = TermDeref(term, &deref);
197 TermCellSetProp(term, prop);
198 for(i=0; i<term->arity; i++)
199 {
200 PStackPushP(stack, term->args[i]);
201 PStackPushInt(stack, deref);
202 }
203 }
204 PStackFree(stack);
205 }
206
207
208 /*-----------------------------------------------------------------------
209 //
210 // Function: TermSearchProp()
211 //
212 // If prop is set in any subterm of term, return true, otherwise
213 // false.
214 //
215 // Global Variables: -
216 //
217 // Side Effects : -
218 //
219 /----------------------------------------------------------------------*/
220
TermSearchProp(Term_p term,DerefType deref,TermProperties prop)221 bool TermSearchProp(Term_p term, DerefType deref, TermProperties prop)
222 {
223 PStack_p stack = PStackAlloc();
224 int i;
225 bool res = false;
226
227 PStackPushP(stack, term);
228 PStackPushInt(stack, deref);
229
230 while(!PStackEmpty(stack))
231 {
232 deref = PStackPopInt(stack);
233 term = PStackPopP(stack);
234 term = TermDeref(term, &deref);
235 if(TermCellQueryProp(term, prop))
236 {
237 res = true;
238 break;
239 }
240 for(i=0; i<term->arity; i++)
241 {
242 PStackPushP(stack, term->args[i]);
243 PStackPushInt(stack, deref);
244 }
245 }
246 PStackFree(stack);
247 return res;
248 }
249
250
251 /*-----------------------------------------------------------------------
252 //
253 // Function: TermVerifyProp()
254 //
255 // If prop has the expected value in all subterms of term, return
256 // true.
257 //
258 // Global Variables: -
259 //
260 // Side Effects : -
261 //
262 /----------------------------------------------------------------------*/
263
TermVerifyProp(Term_p term,DerefType deref,TermProperties prop,TermProperties expected)264 bool TermVerifyProp(Term_p term, DerefType deref, TermProperties prop,
265 TermProperties expected)
266 {
267 PStack_p stack = PStackAlloc();
268 int i;
269 bool res = true;
270
271 PStackPushP(stack, term);
272 PStackPushInt(stack, deref);
273
274 while(!PStackEmpty(stack))
275 {
276 deref = PStackPopInt(stack);
277 term = PStackPopP(stack);
278 term = TermDeref(term, &deref);
279 if(TermCellGiveProps(term, prop)!=expected)
280 {
281 res = false;
282 break;
283 }
284 for(i=0; i<term->arity; i++)
285 {
286 PStackPushP(stack, term->args[i]);
287 PStackPushInt(stack, deref);
288 }
289 }
290 PStackFree(stack);
291 return res;
292 }
293
294
295 /*-----------------------------------------------------------------------
296 //
297 // Function: TermDelProp()
298 //
299 // Delete the properties in all term cells belonging to term.
300 //
301 // Global Variables: -
302 //
303 // Side Effects : Changes properties (even in shared terms! Beware!)
304 //
305 /----------------------------------------------------------------------*/
306
TermDelProp(Term_p term,DerefType deref,TermProperties prop)307 void TermDelProp(Term_p term, DerefType deref, TermProperties prop)
308 {
309 PStack_p stack = PStackAlloc();
310 int i;
311
312 PStackPushP(stack, term);
313 PStackPushInt(stack, deref);
314
315 while(!PStackEmpty(stack))
316 {
317 deref = PStackPopInt(stack);
318 term = PStackPopP(stack);
319 term = TermDeref(term, &deref);
320 TermCellDelProp(term, prop);
321 for(i=0; i<term->arity; i++)
322 {
323 PStackPushP(stack, term->args[i]);
324 PStackPushInt(stack, deref);
325 }
326 }
327 PStackFree(stack);
328 }
329
330
331 /*-----------------------------------------------------------------------
332 //
333 // Function: TermDelPropOpt()
334 //
335 // Delete the properties in all term cells belonging to term.
336 //
337 // Global Variables: -
338 //
339 // Side Effects : Changes properties (even in shared terms! Beware!)
340 //
341 /----------------------------------------------------------------------*/
342
TermDelPropOpt(Term_p term,TermProperties prop)343 void TermDelPropOpt(Term_p term, TermProperties prop)
344 {
345 PStack_p stack = PStackAlloc();
346 int i;
347
348 PStackPushP(stack, term);
349
350 while(!PStackEmpty(stack))
351 {
352 term = PStackPopP(stack);
353 TermCellDelProp(term, prop);
354 for(i=0; i<term->arity; i++)
355 {
356 PStackPushP(stack, term->args[i]);
357 }
358 }
359 PStackFree(stack);
360 }
361
362
363
364
365 /*-----------------------------------------------------------------------
366 //
367 // Function: TermVarSetProp()
368 //
369 // Set the properties in all variable cells belonging to term.
370 //
371 // Global Variables: -
372 //
373 // Side Effects : Changes properties (even in shared terms! Beware!)
374 //
375 /----------------------------------------------------------------------*/
376
TermVarSetProp(Term_p term,DerefType deref,TermProperties prop)377 void TermVarSetProp(Term_p term, DerefType deref, TermProperties prop)
378 {
379 PStack_p stack = PStackAlloc();
380 int i;
381
382 PStackPushP(stack, term);
383 PStackPushInt(stack, deref);
384
385 while(!PStackEmpty(stack))
386 {
387 deref = PStackPopInt(stack);
388 term = PStackPopP(stack);
389 term = TermDeref(term, &deref);
390 if(TermIsVar(term))
391 {
392 TermCellSetProp(term, prop);
393 }
394 for(i=0; i<term->arity; i++)
395 {
396 PStackPushP(stack, term->args[i]);
397 PStackPushInt(stack, deref);
398 }
399 }
400 PStackFree(stack);
401 }
402
403
404 /*-----------------------------------------------------------------------
405 //
406 // Function: TermHasInterpretedSymbol()
407 //
408 // Return true if the term has at least one symbol from an
409 // interpreted sort (currently the arithmetic sorts,
410 //
411 // Global Variables:
412 //
413 // Side Effects :
414 //
415 /----------------------------------------------------------------------*/
416
TermHasInterpretedSymbol(Term_p term)417 bool TermHasInterpretedSymbol(Term_p term)
418 {
419 PStack_p stack = PStackAlloc();
420 int i;
421 bool res = false;
422
423 PStackPushP(stack, term);
424
425 while(!PStackEmpty(stack))
426 {
427 term = PStackPopP(stack);
428 /* printf("#Fcode: %ld Sort: %d\n", term->f_code, term->sort); */
429 if(SortIsInterpreted(term->sort))
430 {
431 res = true;
432 break;
433 }
434 for(i=0; i<term->arity; i++)
435 {
436 PStackPushP(stack, term->args[i]);
437 }
438 }
439 PStackFree(stack);
440
441 return res;
442 }
443
444
445
446 /*-----------------------------------------------------------------------
447 //
448 // Function: TermVarSearchProp()
449 //
450 // If prop is set in any variable cell in term, return true, otherwise
451 // false.
452 //
453 // Global Variables: -
454 //
455 // Side Effects : -
456 //
457 /----------------------------------------------------------------------*/
458
TermVarSearchProp(Term_p term,DerefType deref,TermProperties prop)459 bool TermVarSearchProp(Term_p term, DerefType deref, TermProperties prop)
460 {
461 PStack_p stack = PStackAlloc();
462 int i;
463 bool res = false;
464
465 PStackPushP(stack, term);
466 PStackPushInt(stack, deref);
467
468 while(!PStackEmpty(stack))
469 {
470 deref = PStackPopInt(stack);
471 term = PStackPopP(stack);
472 term = TermDeref(term, &deref);
473 if(TermIsVar(term) && TermCellQueryProp(term, prop))
474 {
475 res = true;
476 break;
477 }
478 for(i=0; i<term->arity; i++)
479 {
480 PStackPushP(stack, term->args[i]);
481 PStackPushInt(stack, deref);
482 }
483 }
484 PStackFree(stack);
485 return res;
486 }
487
488
489 /*-----------------------------------------------------------------------
490 //
491 // Function: TermVarDelProp()
492 //
493 // Delete the properties in all variable cells belonging to term.
494 //
495 // Global Variables: -
496 //
497 // Side Effects : Changes properties (even in shared terms! Beware!)
498 //
499 /----------------------------------------------------------------------*/
500
TermVarDelProp(Term_p term,DerefType deref,TermProperties prop)501 void TermVarDelProp(Term_p term, DerefType deref, TermProperties prop)
502 {
503 PStack_p stack = PStackAlloc();
504 int i;
505
506 PStackPushP(stack, term);
507 PStackPushInt(stack, deref);
508
509 while(!PStackEmpty(stack))
510 {
511 deref = PStackPopInt(stack);
512 term = PStackPopP(stack);
513 term = TermDeref(term, &deref);
514 if(TermIsVar(term))
515 {
516 TermCellDelProp(term, prop);
517 }
518 for(i=0; i<term->arity; i++)
519 {
520 PStackPushP(stack, term->args[i]);
521 PStackPushInt(stack, deref);
522 }
523 }
524 PStackFree(stack);
525 }
526
527
528 /*-----------------------------------------------------------------------
529 //
530 // Function: TermStackSetProps()
531 //
532 // Set the given properties in all term cells on the stack.
533 //
534 // Global Variables: -
535 //
536 // Side Effects : -
537 //
538 /----------------------------------------------------------------------*/
539
TermStackSetProps(PStack_p stack,TermProperties prop)540 void TermStackSetProps(PStack_p stack, TermProperties prop)
541 {
542 PStackPointer i;
543 Term_p term;
544
545 for(i=0; i<PStackGetSP(stack); i++)
546 {
547 term = PStackElementP(stack, i);
548 TermCellSetProp(term, prop);
549 }
550 }
551
552
553 /*-----------------------------------------------------------------------
554 //
555 // Function: TermStackDelProps()
556 //
557 // Delete the given properties in all term cells on the stack.
558 //
559 // Global Variables: -
560 //
561 // Side Effects : -
562 //
563 /----------------------------------------------------------------------*/
564
TermStackDelProps(PStack_p stack,TermProperties prop)565 void TermStackDelProps(PStack_p stack, TermProperties prop)
566 {
567 PStackPointer i;
568 Term_p term;
569
570 for(i=0; i<PStackGetSP(stack); i++)
571 {
572 term = PStackElementP(stack, i);
573 TermCellDelProp(term, prop);
574 }
575 }
576
577
578
579 /*---------------------------------------------------------------------*/
580 /* End of File */
581 /*---------------------------------------------------------------------*/
582