1 /*-----------------------------------------------------------------------
2
3 File : cte_signature.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Functions implementing the signature functionality.
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> Sun Sep 21 19:27:54 MET DST 1997
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "cte_signature.h"
25
26
27
28 /*---------------------------------------------------------------------*/
29 /* Global Variables */
30 /*---------------------------------------------------------------------*/
31
32 bool SigSupportLists = false;
33
34 /*---------------------------------------------------------------------*/
35 /* Forward Declarations */
36 /*---------------------------------------------------------------------*/
37
38
39 /*---------------------------------------------------------------------*/
40 /* Internal Functions */
41 /*---------------------------------------------------------------------*/
42
43
44
45 /*-----------------------------------------------------------------------
46 //
47 // Function: sig_print_operator()
48 //
49 // Print a single operator
50 //
51 // Global Variables: -
52 //
53 // Side Effects : Output
54 //
55 /----------------------------------------------------------------------*/
56
sig_print_operator(FILE * out,Sig_p sig,FunCode op,bool comments)57 static void sig_print_operator(FILE* out, Sig_p sig, FunCode op, bool comments)
58 {
59 if(comments)
60 {
61 fprintf(out, " %-13s : %2d # %2ld %2d \n",
62 sig->f_info[op].name, sig->f_info[op].arity, op,
63 sig->f_info[op].properties);
64 }
65 else
66 {
67 fprintf(out, " %-13s : %2d\n",
68 sig->f_info[op].name, sig->f_info[op].arity);
69 }
70 }
71
72 /*-----------------------------------------------------------------------
73 //
74 // Function: sig_compute_alpha_ranks()
75 //
76 // For all symbols in sig compute the alpha-rank of the symbol.
77 //
78 // Global Variables: -
79 //
80 // Side Effects : Memory operations, changes the ranks in sig.
81 //
82 /----------------------------------------------------------------------*/
83
sig_compute_alpha_ranks(Sig_p sig)84 static void sig_compute_alpha_ranks(Sig_p sig)
85 {
86 PStack_p stack;
87 long count = 0;
88 StrTree_p handle;
89
90 stack = StrTreeTraverseInit(sig->f_index);
91
92 while((handle = StrTreeTraverseNext(stack)))
93 {
94 sig->f_info[handle->val1.i_val].alpha_rank = count++;
95 }
96 StrTreeTraverseExit(stack);
97
98 sig->alpha_ranks_valid = true;
99 }
100
101
102 /*---------------------------------------------------------------------*/
103 /* Exported Functions */
104 /*---------------------------------------------------------------------*/
105
106 /*-----------------------------------------------------------------------
107 //
108 // Function: SigAlloc()
109 //
110 // Allocate a initialized signature cell. Also initializes a type table.
111 //
112 // Global Variables: -
113 //
114 // Side Effects : Memory operations
115 //
116 /----------------------------------------------------------------------*/
117
SigAlloc(SortTable_p sort_table)118 Sig_p SigAlloc(SortTable_p sort_table)
119 {
120 Sig_p handle;
121
122 handle = SigCellAlloc();
123
124 handle->alpha_ranks_valid = false;
125 handle->size = DEFAULT_SIGNATURE_SIZE;
126 handle->f_count = 0;
127 handle->f_info =
128 SecureMalloc(sizeof(FuncCell)*DEFAULT_SIGNATURE_SIZE);
129 handle->f_index = NULL;
130 handle->ac_axioms = PStackAlloc();
131
132 handle->sort_table = sort_table;
133 handle->type_table = TypeTableAlloc(sort_table);
134
135 SigInsertId(handle, "$true", 0, true);
136 assert(SigFindFCode(handle, "$true")==SIG_TRUE_CODE);
137 SigSetFuncProp(handle, SIG_TRUE_CODE, FPInterpreted);
138 SigDeclareType(handle, SIG_TRUE_CODE, TypeNewConstant(handle->type_table, STBool));
139 SigInsertId(handle, "$false", 0, true);
140 assert(SigFindFCode(handle, "$false")==SIG_FALSE_CODE);
141 SigSetFuncProp(handle, SIG_FALSE_CODE, FPInterpreted);
142 SigDeclareType(handle, SIG_FALSE_CODE, TypeNewConstant(handle->type_table, STBool));
143
144 if(SigSupportLists)
145 {
146 SigInsertId(handle, "$nil", 0, true);
147 assert(SigFindFCode(handle, "$nil")==SIG_NIL_CODE);
148 SigInsertId(handle, "$cons", 2, true);
149 assert(SigFindFCode(handle, "$cons")==SIG_CONS_CODE);
150 }
151
152
153 handle->internal_symbols = handle->f_count;
154
155 handle->eqn_code = 0;
156 handle->neqn_code = 0;
157 handle->cnil_code = 0;
158 handle->orn_codes = NULL;
159
160 handle->or_code = 0;
161 handle->not_code = 0;
162 handle->qex_code = 0;
163 handle->qall_code = 0;
164 handle->and_code = 0;
165 handle->or_code = 0;
166 handle->impl_code = 0;
167 handle->equiv_code = 0;
168 handle->nand_code = 0;
169 handle->nor_code = 0;
170 handle->bimpl_code = 0;
171 handle->xor_code = 0;
172 handle->answer_code = 0;
173
174 handle->skolem_count = 0;
175 handle->newpred_count = 0;
176
177 handle->distinct_props = FPDistinctProp;
178 return handle;
179 }
180
181
182
183
184 /*-----------------------------------------------------------------------
185 //
186 // Function: SigInitInternalCodes()
187 //
188 // Put all the FOF operators as function symbols into sig. Sig
189 // should be empty, so that sig->internal symbols can be properly
190 // initialized. Note that this will be used for plain term
191 // signatures. It reuses some equivalent fields of signatures used
192 // for patterns, but morphs the f_codes into internal symbols.
193 //
194 // Global Variables: -
195 //
196 // Side Effects : Changes sig...
197 //
198 /----------------------------------------------------------------------*/
199
SigInsertInternalCodes(Sig_p sig)200 void SigInsertInternalCodes(Sig_p sig)
201 {
202 int i_sort = STIndividuals;
203
204 assert((SigSupportLists && sig->internal_symbols == SIG_CONS_CODE) ||
205 (!SigSupportLists && sig->internal_symbols == SIG_FALSE_CODE));
206
207 sig->eqn_code = SigInsertId(sig, "$eq", 2, true);
208 SigSetPolymorphic(sig, sig->eqn_code, true);
209
210 sig->neqn_code = SigInsertId(sig, "$neq", 2, true);
211 SigSetPolymorphic(sig, sig->eqn_code, true);
212
213 sig->qex_code = SigInsertId(sig, "$qex", 2, true);
214 sig->qall_code = SigInsertId(sig, "$qall", 2, true);
215 SigSetPolymorphic(sig, sig->qex_code, true);
216 SigSetPolymorphic(sig, sig->qall_code, true);
217
218 sig->not_code = SigInsertFOFOp(sig, "$not", 1);
219 sig->and_code = SigInsertFOFOp(sig, "$and", 2);
220 sig->or_code = SigInsertFOFOp(sig, "$or", 2);
221 sig->impl_code = SigInsertFOFOp(sig, "$impl", 2);
222 sig->equiv_code = SigInsertFOFOp(sig, "$equiv", 2);
223 sig->nand_code = SigInsertFOFOp(sig, "$nand", 2);
224 sig->nor_code = SigInsertFOFOp(sig, "$nor", 2);
225 sig->bimpl_code = SigInsertFOFOp(sig, "$bimpl", 2);
226 sig->xor_code = SigInsertFOFOp(sig, "$xor", 2);
227
228 sig->xor_code = SigInsertFOFOp(sig, "$xor", 2);
229
230 sig->answer_code = SigInsertId(sig, "$answer", 1, true);
231 SigSetFuncProp(sig, sig->answer_code, FPInterpreted|FPPseudoPred);
232 SigDeclareFinalType(sig, sig->answer_code,
233 TypeNewFunction(sig->type_table, STBool, 1, &i_sort));
234
235 sig->internal_symbols = sig->f_count;
236 }
237
238
239
240 /*-----------------------------------------------------------------------
241 //
242 // Function: SigFree()
243 //
244 // Free signature.
245 //
246 // Global Variables: -
247 //
248 // Side Effects : Memory operations
249 //
250 /----------------------------------------------------------------------*/
251
SigFree(Sig_p junk)252 void SigFree(Sig_p junk)
253 {
254 assert(junk);
255 assert(junk->f_info);
256
257 /* names are shared with junk->f_index and are free()ed by the
258 StrTreeFree() call below! */
259 FREE(junk->f_info);
260 StrTreeFree(junk->f_index);
261 PStackFree(junk->ac_axioms);
262 if(junk->orn_codes)
263 {
264 PDArrayFree(junk->orn_codes);
265 }
266 TypeTableFree(junk->type_table);
267
268 SigCellFree(junk);
269 }
270
271
272 /*-----------------------------------------------------------------------
273 //
274 // Function: SigFindFCode()
275 //
276 // Return the index of the entry name in sig, or 0 if name is not in
277 // sig.
278 //
279 // Global Variables: -
280 //
281 // Side Effects : -
282 //
283 /----------------------------------------------------------------------*/
284
SigFindFCode(Sig_p sig,const char * name)285 FunCode SigFindFCode(Sig_p sig, const char* name)
286 {
287 StrTree_p entry;
288
289 entry = StrTreeFind(&(sig->f_index), name);
290
291 if(entry)
292 {
293 return entry->val1.i_val;
294 }
295 return 0;
296 }
297
298
299 /*-----------------------------------------------------------------------
300 //
301 // Function: SigIsPredicate()
302 //
303 // Returns true if the symbol is known to be a predicate
304 //
305 // Global Variables: -
306 //
307 // Side Effects : -
308 //
309 /----------------------------------------------------------------------*/
310
SigIsPredicate(Sig_p sig,FunCode f_code)311 bool SigIsPredicate(Sig_p sig, FunCode f_code)
312 {
313 Type_p type;
314
315 assert(f_code > 0);
316 assert(f_code <= sig->f_count);
317
318 if(FuncQueryProp(&(sig->f_info[f_code]), FPTypePoly))
319 {
320 return true;
321 }
322
323 type = SigGetType(sig, f_code);
324 return type && type->domain_sort == STBool;
325 }
326
327
328 /*-----------------------------------------------------------------------
329 //
330 // Function: SigIsFunction()
331 //
332 // Return the value of the Function field for a function symbol.
333 //
334 // Global Variables: -
335 //
336 // Side Effects : -
337 //
338 /----------------------------------------------------------------------*/
339
SigIsFunction(Sig_p sig,FunCode f_code)340 bool SigIsFunction(Sig_p sig, FunCode f_code)
341 {
342 Type_p type;
343
344 assert(f_code > 0);
345 assert(f_code <= sig->f_count);
346
347 if(!FuncQueryProp(&(sig->f_info[f_code]), FPTypeFixed))
348 {
349 return false;
350 }
351
352 type = SigGetType(sig, f_code);
353 return type && type->domain_sort != STBool;
354 }
355
356
357 /*-----------------------------------------------------------------------
358 //
359 // Function: SigIsFixedType
360 //
361 // check whether we are sure of the type of this function
362 //
363 // Global Variables: -
364 //
365 // Side Effects : -
366 //
367 /----------------------------------------------------------------------*/
SigIsFixedType(Sig_p sig,FunCode f_code)368 bool SigIsFixedType(Sig_p sig, FunCode f_code)
369 {
370 assert(f_code > 0);
371 assert(f_code <= sig->f_count);
372
373 return FuncQueryProp(&(sig->f_info[f_code]), FPTypeFixed);
374 }
375
376
377 /*-----------------------------------------------------------------------
378 //
379 // Function: SigFixType
380 //
381 // Fix the type of the function, because we are sure the type is the
382 // right one (no ambiguity).
383 //
384 // Global Variables: -
385 //
386 // Side Effects : Modifiy signature
387 //
388 /----------------------------------------------------------------------*/
SigFixType(Sig_p sig,FunCode f_code)389 void SigFixType(Sig_p sig, FunCode f_code)
390 {
391 assert(f_code > 0);
392 assert(f_code <= sig->f_count);
393
394 FuncSetProp(&(sig->f_info[f_code]), FPTypeFixed);
395 }
396
397 /*-----------------------------------------------------------------------
398 //
399 // Function: SigIsPolymorphic
400 //
401 // Checks whether the symbol is Ad-hoc polymorphic
402 //
403 // Global Variables: -
404 //
405 // Side Effects : -
406 //
407 /----------------------------------------------------------------------*/
SigIsPolymorphic(Sig_p sig,FunCode f_code)408 bool SigIsPolymorphic(Sig_p sig, FunCode f_code)
409 {
410 assert(f_code > 0);
411 assert(f_code <= sig->f_count);
412
413 return FuncQueryProp(&(sig->f_info[f_code]), FPTypePoly);
414 }
415
416 /*-----------------------------------------------------------------------
417 //
418 // Function: SigSetPolymorphic
419 //
420 // Declare that this symbol is polymorphic
421 //
422 // Global Variables: -
423 //
424 // Side Effects : modifies the signature
425 //
426 /----------------------------------------------------------------------*/
SigSetPolymorphic(Sig_p sig,FunCode f_code,bool value)427 void SigSetPolymorphic(Sig_p sig, FunCode f_code, bool value)
428 {
429 assert(f_code > 0);
430 assert(f_code <= sig->f_count);
431
432 FuncSetProp(&(sig->f_info[f_code]), FPTypePoly);
433 }
434
435
436 /*-----------------------------------------------------------------------
437 //
438 // Function: SigQueryProp
439 // Checks whether a symbol has all the given properties
440 //
441 //
442 // Global Variables: -
443 //
444 // Side Effects : -
445 //
446 /----------------------------------------------------------------------*/
SigQueryProp(Sig_p sig,FunCode f_code,FunctionProperties prop)447 bool SigQueryProp(Sig_p sig, FunCode f_code, FunctionProperties prop)
448 {
449 assert(f_code > 0);
450 assert(f_code <= sig->f_count);
451
452 return FuncQueryProp(&(sig->f_info[f_code]), prop);
453 }
454
455 /*-----------------------------------------------------------------------
456 //
457 // Function: SigSetSpecial()
458 //
459 // Set the value of the special field for a function symbol.
460 //
461 // Global Variables: -
462 //
463 // Side Effects : -
464 //
465 /----------------------------------------------------------------------*/
466
SigSetSpecial(Sig_p sig,FunCode f_code,bool value)467 void SigSetSpecial(Sig_p sig, FunCode f_code, bool value)
468 {
469 assert(f_code > 0);
470 assert(f_code <= sig->f_count);
471
472 if(value)
473 {
474 SigSetFuncProp(sig,f_code,FPSpecial);
475 }
476 else
477 {
478 SigDelFuncProp(sig,f_code,FPSpecial);
479 }
480 }
481
482
483
484 /*-----------------------------------------------------------------------
485 //
486 // Function: SigIsSpecial()
487 //
488 // Return the value of the special field for a function symbol.
489 //
490 // Global Variables: -
491 //
492 // Side Effects : -
493 //
494 /----------------------------------------------------------------------*/
495
SigIsSpecial(Sig_p sig,FunCode f_code)496 bool SigIsSpecial(Sig_p sig, FunCode f_code)
497 {
498 assert(f_code > 0);
499 assert(f_code <= sig->f_count);
500
501 return FuncQueryProp(&(sig->f_info[f_code]), FPSpecial);
502 }
503
504
505 /*-----------------------------------------------------------------------
506 //
507 // Function: SigGetAlphaRank()
508 //
509 // Given a signature and an function symbol code, return the symbols
510 // alpha-rank.
511 //
512 // Global Variables: -
513 //
514 // Side Effects : -
515 //
516 /----------------------------------------------------------------------*/
517
SigGetAlphaRank(Sig_p sig,FunCode f_code)518 int SigGetAlphaRank(Sig_p sig, FunCode f_code)
519 {
520 assert(f_code > 0);
521 assert(f_code <= sig->f_count);
522
523 if(!sig->alpha_ranks_valid)
524 {
525 sig_compute_alpha_ranks(sig);
526 }
527 assert(sig->alpha_ranks_valid);
528
529 return (sig->f_info[f_code]).alpha_rank;
530 }
531
532
533 /*-----------------------------------------------------------------------
534 //
535 // Function: SigSetAllSpecial()
536 //
537 // Set the special value of all symbols in sig.
538 //
539 // Global Variables: -
540 //
541 // Side Effects : -
542 //
543 /----------------------------------------------------------------------*/
544
SigSetAllSpecial(Sig_p sig,bool value)545 void SigSetAllSpecial(Sig_p sig, bool value)
546 {
547 FunCode i;
548
549 for(i=1; i<=sig->f_count; i++)
550 {
551 SigSetSpecial(sig, i, value);
552 }
553 }
554
555 /*-----------------------------------------------------------------------
556 //
557 // Function: SigInsertId()
558 //
559 // Insert the symbol name with arity into the signature. Return the
560 // f_code assigned to the name or 0 if the same name has already
561 // been used with a different arity.
562 //
563 // Global Variables: -
564 //
565 // Side Effects : Potential memory operations.
566 //
567 /----------------------------------------------------------------------*/
568
SigInsertId(Sig_p sig,const char * name,int arity,bool special_id)569 FunCode SigInsertId(Sig_p sig, const char* name, int arity, bool special_id)
570 {
571 long pos;
572 StrTree_p new, test;
573
574 pos = SigFindFCode(sig, name);
575
576 if(pos) /* name is already known */
577 {
578 if(sig->f_info[pos].arity != arity)
579 {
580 printf("Problem: %s %d != %d\n", name, arity, sig->f_info[pos].arity);
581 return 0; /* ...but incompatible */
582 }
583 if(special_id)
584 {
585 SigSetSpecial(sig, pos, true);
586 }
587 return pos; /* all is fine... */
588 }
589 /* Now insert the new name...ensure that there is space */
590 if(sig->f_count == sig->size-1)
591 {
592 /* sig->size+= DEFAULT_SIGNATURE_SIZE; */
593 sig->size *= DEFAULT_SIGNATURE_GROW;
594 sig->f_info = SecureRealloc(sig->f_info,
595 sizeof(FuncCell)*sig->size);
596 }
597
598 /* Insert the element in f_index and f_info */
599 sig->f_count++;
600 sig->f_info[sig->f_count].name
601 = SecureStrdup(name);
602 sig->f_info[sig->f_count].arity = arity;
603 sig->f_info[sig->f_count].properties = FPIgnoreProps;
604 sig->f_info[sig->f_count].type = NULL;
605 new = StrTreeCellAllocEmpty();
606 new->key = sig->f_info[sig->f_count].name;
607 new->val1.i_val = sig->f_count;
608
609 test = StrTreeInsert(&(sig->f_index), new);
610 UNUSED(test); assert(test == NULL);
611 SigSetSpecial(sig,sig->f_count,special_id);
612 sig->alpha_ranks_valid = false;
613
614 return sig->f_count;
615 }
616
617 /*-----------------------------------------------------------------------
618 //
619 // Function: SigInsertFOFOp()
620 //
621 // Insert a special function symbol used to encode a first-order
622 // operator.
623 //
624 // Global Variables: -
625 //
626 // Side Effects : -
627 //
628 /----------------------------------------------------------------------*/
629
SigInsertFOFOp(Sig_p sig,const char * name,int arity)630 FunCode SigInsertFOFOp(Sig_p sig, const char* name, int arity)
631 {
632 FunCode res = SigInsertId(sig, name, arity, true);
633
634 SigSetFuncProp(sig, res, FPFOFOp);
635 return res;
636 }
637
638 /*-----------------------------------------------------------------------
639 //
640 // Function: SigPrint()
641 //
642 // Print the signature in external representation, with comments
643 // showing internal structure.
644 //
645 // Global Variables: -
646 //
647 // Side Effects : Output
648 //
649 /----------------------------------------------------------------------*/
650
SigPrint(FILE * out,Sig_p sig)651 void SigPrint(FILE* out, Sig_p sig)
652 {
653 FunCode i;
654
655 fprintf(out, "# Signature (%2ld symbols out of %2ld allocated):\n",
656 sig->f_count, sig->size);
657 fprintf(out, "# -Symbol- -Arity- -Encoding-\n");
658
659 for(i=1; i<=sig->f_count; i++)
660 {
661 sig_print_operator(out, sig, i, true);
662 }
663 }
664
665
666 /*-----------------------------------------------------------------------
667 //
668 // Function: SigPrintSpecial()
669 //
670 // Print the external special symbols from sig.
671 //
672 // Global Variables: -
673 //
674 // Side Effects : Output
675 //
676 /----------------------------------------------------------------------*/
677
SigPrintSpecial(FILE * out,Sig_p sig)678 void SigPrintSpecial(FILE* out, Sig_p sig)
679 {
680 FunCode i;
681
682 fputs("# Special symbols:\n", out);
683 for(i=1; i<=sig->f_count; i++)
684 {
685 if(SigIsSpecial(sig, i))
686 {
687 sig_print_operator(out, sig, i, true);
688 }
689 }
690 }
691
692 /*-----------------------------------------------------------------------
693 //
694 // Function: SigPrintACStatus()
695 //
696 // For each function symbol which is A, C, or AC, print its status
697 // as a comment.
698 //
699 // Global Variables: -
700 //
701 // Side Effects : Output
702 //
703 /----------------------------------------------------------------------*/
704
SigPrintACStatus(FILE * out,Sig_p sig)705 void SigPrintACStatus(FILE* out, Sig_p sig)
706 {
707 FunCode i;
708
709 for(i=1; i<=sig->f_count; i++)
710 {
711 if(SigQueryFuncProp(sig, i, FPIsAC))
712 {
713 fprintf(out, "# %s is AC\n", sig->f_info[i].name);
714 continue;
715 }
716 if(SigQueryFuncProp(sig, i, FPAssociative))
717 {
718 fprintf(out, "# %s is associative\n", sig->f_info[i].name);
719 continue;
720 }
721 if(SigQueryFuncProp(sig, i, FPCommutative))
722 {
723 fprintf(out, "# %s is commutative\n", sig->f_info[i].name);
724 continue;
725 }
726 }
727 }
728
729
730
731 /*-----------------------------------------------------------------------
732 //
733 // Function: SigParseKnownOperator()
734 //
735 // Parse an operator, return its FunCode. Error, if operator is not
736 // in sig.
737 //
738 // Global Variables: -
739 //
740 // Side Effects : Reads input, memory operations
741 //
742 /----------------------------------------------------------------------*/
743
SigParseKnownOperator(Scanner_p in,Sig_p sig)744 FunCode SigParseKnownOperator(Scanner_p in, Sig_p sig)
745 {
746 FunCode res;
747 int line, column;
748 DStr_p id, source_name, errpos;
749 StreamType type;
750
751 line = AktToken(in)->line;
752 column = AktToken(in)->column;
753 source_name = DStrGetRef(AktToken(in)->source);
754 type = AktToken(in)->stream_type;
755
756 id = DStrAlloc();
757 FuncSymbParse(in, id);
758
759 res = SigFindFCode(sig, DStrView(id));
760
761 if(!res)
762 {
763 errpos = DStrAlloc();
764
765 DStrAppendStr(errpos, PosRep(type, source_name, line, column));
766 DStrAppendChar(errpos, ' ');
767 DStrAppendStr(errpos, DStrView(id));
768 DStrAppendStr(errpos, " undeclared!");
769 Error(DStrView(errpos), SYNTAX_ERROR);
770 DStrFree(errpos);
771 }
772 DStrReleaseRef(source_name);
773 DStrFree(id);
774
775 return res;
776 }
777
778
779 /*-----------------------------------------------------------------------
780 //
781 // Function: SigParseSymbolDeclaration()
782 //
783 // Parse a single symbol declaration (f:3) and insert it into sig.
784 //
785 // Global Variables: -
786 //
787 // Side Effects : Changes sig, reads input, may cause error
788 //
789 /----------------------------------------------------------------------*/
790
SigParseSymbolDeclaration(Scanner_p in,Sig_p sig,bool special_id)791 FunCode SigParseSymbolDeclaration(Scanner_p in, Sig_p sig, bool special_id)
792 {
793 int arity, line, column;
794 DStr_p id = DStrAlloc(), source_name, errpos;
795 FunCode res;
796 StreamType type;
797
798 line = AktToken(in)->line;
799 column = AktToken(in)->column;
800 source_name = DStrGetRef(AktToken(in)->source);
801 type = AktToken(in)->stream_type;
802
803 FuncSymbParse(in, id);
804 AcceptInpTok(in, Colon);
805 arity = AktToken(in)->numval;
806 AcceptInpTok(in, PosInt);
807
808 res = SigInsertId(sig, DStrView(id), arity, special_id);
809 if(!res)
810 {
811 errpos = DStrAlloc();
812
813 DStrAppendStr(errpos, PosRep(type, source_name, line, column));
814 DStrAppendChar(errpos, ' ');
815 DStrAppendStr(errpos, DStrView(id));
816 DStrAppendStr(errpos, " declared with arity ");
817 DStrAppendInt(errpos, (long)arity);
818 DStrAppendStr(errpos, " but registered with arity ");
819 DStrAppendInt(errpos,
820 (long)SigFindArity(sig, SigFindFCode(sig, DStrView(id))));
821 Error(DStrView(errpos), SYNTAX_ERROR);
822 DStrFree(errpos);
823 }
824 DStrReleaseRef(source_name);
825 DStrFree(id);
826
827 return res;
828 }
829
830
831 /*-----------------------------------------------------------------------
832 //
833 // Function: SigParse()
834 //
835 // Parse a list of declarations into a signature.
836 //
837 // Global Variables: -
838 //
839 // Side Effects : -
840 //
841 /----------------------------------------------------------------------*/
842
SigParse(Scanner_p in,Sig_p sig,bool special_ids)843 FunCode SigParse(Scanner_p in, Sig_p sig, bool special_ids)
844 {
845 FunCode res = 0;
846
847 /* FIXME: Cannot handle complex symbols here! */
848 while(TestInpTok(in, FuncSymbToken) &&
849 TestTok(LookToken(in, 1), Colon))
850 {
851 res = SigParseSymbolDeclaration(in, sig, special_ids);
852 }
853 return res;
854 }
855
856
857 /*-----------------------------------------------------------------------
858 //
859 // Function: SigFindMaxUsedArity()
860 //
861 // Return the largest arity of any function symbol used in the
862 // signature.
863 //
864 // Global Variables: -
865 //
866 // Side Effects : -
867 //
868 /----------------------------------------------------------------------*/
869
SigFindMaxUsedArity(Sig_p sig)870 int SigFindMaxUsedArity(Sig_p sig)
871 {
872 int res = 0;
873 FunCode i;
874
875 for(i=1; i<=sig->f_count; i++)
876 {
877 res = MAX(res, SigFindArity(sig, i));
878 }
879 return res;
880 }
881
882
883 /*-----------------------------------------------------------------------
884 //
885 // Function: SigFindMaxPredicateArity()
886 //
887 // Return the largest arity of any predicate function symbol used in
888 // the signature.
889 //
890 // Global Variables: -
891 //
892 // Side Effects : -
893 //
894 /----------------------------------------------------------------------*/
895
SigFindMaxPredicateArity(Sig_p sig)896 int SigFindMaxPredicateArity(Sig_p sig)
897 {
898 FunCode i;
899 int res=0, arity;
900
901 for(i=sig->internal_symbols+1; i<=sig->f_count; i++)
902 {
903 if(SigIsPredicate(sig, i) &&
904 !SigQueryFuncProp(sig, i, FPSpecial))
905 {
906 arity = SigFindArity(sig,i);
907 res = MAX(res,arity);
908 }
909 }
910 return res;
911 }
912
913
914 /*-----------------------------------------------------------------------
915 //
916 // Function: SigFindMinPredicateArity()
917 //
918 // Return the smallest arity of any predicate function symbol used in
919 // the signature.
920 //
921 // Global Variables: -
922 //
923 // Side Effects : -
924 //
925 /----------------------------------------------------------------------*/
926
SigFindMinPredicateArity(Sig_p sig)927 int SigFindMinPredicateArity(Sig_p sig)
928 {
929 FunCode i;
930 int res=INT_MAX, arity;
931
932 for(i=sig->internal_symbols+1; i<=sig->f_count; i++)
933 {
934 if(SigIsPredicate(sig, i) &&
935 !SigQueryFuncProp(sig, i, FPSpecial))
936 {
937 arity = SigFindArity(sig,i);
938 res = MIN(res,arity);
939 }
940 }
941 return res;
942 }
943
944
945 /*-----------------------------------------------------------------------
946 //
947 // Function: SigFindMaxFunctionArity()
948 //
949 // Return the largest arity of any real function symbol used in the
950 // signature.
951 //
952 // Global Variables: -
953 //
954 // Side Effects : -
955 //
956 /----------------------------------------------------------------------*/
957
SigFindMaxFunctionArity(Sig_p sig)958 int SigFindMaxFunctionArity(Sig_p sig)
959 {
960 FunCode i;
961 int res=0, arity;
962
963 for(i=sig->internal_symbols+1; i<=sig->f_count; i++)
964 {
965 if(!SigIsPredicate(sig, i) && !SigQueryFuncProp(sig, i, FPSpecial))
966 {
967 arity = SigFindArity(sig,i);
968 res = MAX(res,arity);
969 }
970 }
971 return res;
972 }
973
974
975 /*-----------------------------------------------------------------------
976 //
977 // Function: SigFindMinFunctionArity()
978 //
979 // Return the smallest arity of any real function symbol used in the
980 // signature.
981 //
982 // Global Variables: -
983 //
984 // Side Effects : -
985 //
986 /----------------------------------------------------------------------*/
987
SigFindMinFunctionArity(Sig_p sig)988 int SigFindMinFunctionArity(Sig_p sig)
989 {
990 FunCode i;
991 int res=INT_MAX, arity;
992
993 for(i=sig->internal_symbols+1; i<=sig->f_count; i++)
994 {
995 if(!SigIsPredicate(sig, i) && !SigQueryFuncProp(sig, i, FPSpecial))
996 {
997 arity = SigFindArity(sig,i);
998 res = MIN(res,arity);
999 }
1000 }
1001 return res;
1002 }
1003
1004
1005 /*-----------------------------------------------------------------------
1006 //
1007 // Function: SigCountAritySymbols()
1008 //
1009 // Count number of symbols with a given arity. If predictates is
1010 // true, count predicates, otherwise count function symbols.
1011 //
1012 // Global Variables: -
1013 //
1014 // Side Effects : -
1015 //
1016 /----------------------------------------------------------------------*/
1017
SigCountAritySymbols(Sig_p sig,int arity,bool predicates)1018 int SigCountAritySymbols(Sig_p sig, int arity, bool predicates)
1019 {
1020 FunCode i;
1021 int res=0, tmp_arity;
1022
1023 for(i=sig->internal_symbols+1; i<=sig->f_count; i++)
1024 {
1025 if(EQUIV(SigIsPredicate(sig, i), predicates)
1026 &&(!SigIsSpecial(sig,i)))
1027 {
1028 tmp_arity = SigFindArity(sig,i);
1029 if(tmp_arity==arity)
1030 {
1031 res++;
1032 }
1033 }
1034 }
1035 return res;
1036 }
1037
1038
1039 /*-----------------------------------------------------------------------
1040 //
1041 // Function: SigCountSymbols()
1042 //
1043 // Count number of symbols. If predictates is
1044 // true, count predicates, otherwise count function symbols.
1045 //
1046 // Global Variables: -
1047 //
1048 // Side Effects : -
1049 //
1050 /----------------------------------------------------------------------*/
1051
SigCountSymbols(Sig_p sig,bool predicates)1052 int SigCountSymbols(Sig_p sig, bool predicates)
1053 {
1054 FunCode i;
1055 int res=0;
1056
1057 for(i=sig->internal_symbols+1; i<=sig->f_count; i++)
1058 {
1059 if(!SigIsSpecial(sig,i))
1060 {
1061 if(predicates && SigIsPredicate(sig, i))
1062 {
1063 res++;
1064 }
1065 else if(!predicates && SigIsFunction(sig, i))
1066 {
1067 res++;
1068 }
1069 }
1070 }
1071 return res;
1072 }
1073
1074
1075
1076 /*-----------------------------------------------------------------------
1077 //
1078 // Function: SigAddSymbolArities()
1079 //
1080 // Count the occurences of symbols of a given arity (by adding one
1081 // for each symbol to the corresponding entry in distrib). If
1082 // predicates is true, count predicate symbols only, otherwise count
1083 // function symbols only. Only looks at symbols where select[symbol]
1084 // is true. Return maximal arity of relevant symbols.
1085 //
1086 // Global Variables: -
1087 //
1088 // Side Effects : -
1089 //
1090 /----------------------------------------------------------------------*/
1091
SigAddSymbolArities(Sig_p sig,PDArray_p distrib,bool predicates,long selection[])1092 int SigAddSymbolArities(Sig_p sig, PDArray_p distrib, bool predicates,
1093 long selection[])
1094 {
1095 FunCode i;
1096 int max_arity = -1, arity;
1097
1098 for(i = 1; i<=sig->f_count; i++)
1099 {
1100 if(EQUIV(SigIsPredicate(sig, i), predicates) &&
1101 selection[i])
1102 {
1103 arity = SigFindArity(sig, i);
1104 max_arity = MAX(arity, max_arity);
1105 PDArrayElementIncInt(distrib, arity, 1);
1106 }
1107 }
1108 return max_arity;
1109 }
1110
1111
1112 /*-----------------------------------------------------------------------
1113 //
1114 // Function: SigGetOrNCode()
1115 //
1116 // Return FunCode for $orn, create them if non-existant.
1117 //
1118 // Global Variables: -
1119 //
1120 // Side Effects : May change sig
1121 //
1122 /----------------------------------------------------------------------*/
1123
SigGetOrNCode(Sig_p sig,int arity)1124 FunCode SigGetOrNCode(Sig_p sig, int arity)
1125 {
1126 FunCode res;
1127
1128 assert(sig);
1129
1130 if(!sig->orn_codes)
1131 {
1132 sig->orn_codes = PDArrayAlloc(10,10);
1133 }
1134 res = PDArrayElementInt(sig->orn_codes, arity);
1135
1136 if(res)
1137 {
1138 return res;
1139 }
1140 {
1141 char tmp_str[16]; /* large enough for "or" + digits of INT_MAX */
1142
1143 sprintf(tmp_str, "$or%d", arity);
1144 res = SigInsertId(sig, tmp_str, arity, true);
1145 assert(res);
1146 PDArrayAssignInt(sig->orn_codes, arity, res);
1147 return res;
1148 }
1149 }
1150
1151
1152 /*-----------------------------------------------------------------------
1153 //
1154 // Function: SigGetOtherEqnCode()
1155 //
1156 // If eqn_code is passed in, return neqn_code, and vice
1157 // versa. Assumes FOF-initialized signature.
1158 //
1159 // Global Variables: -
1160 //
1161 // Side Effects : -
1162 //
1163 /----------------------------------------------------------------------*/
1164
SigGetOtherEqnCode(Sig_p sig,FunCode f_code)1165 FunCode SigGetOtherEqnCode(Sig_p sig, FunCode f_code)
1166 {
1167 if(f_code == sig->eqn_code)
1168 {
1169 return sig->neqn_code;
1170 }
1171 assert(f_code == sig->neqn_code);
1172 return sig->eqn_code;
1173 }
1174
1175
1176
1177 /*-----------------------------------------------------------------------
1178 //
1179 // Function: SigGetNewSkolemCode()
1180 //
1181 // Return a new skolem symbol with arity n. The symbol will be of
1182 // the form esk<count>_<ar>, and is guaranteed to be new to sig.
1183 //
1184 // Global Variables: -
1185 //
1186 // Side Effects : Extends signature
1187 //
1188 /----------------------------------------------------------------------*/
1189
SigGetNewSkolemCode(Sig_p sig,int arity)1190 FunCode SigGetNewSkolemCode(Sig_p sig, int arity)
1191 {
1192 FunCode res;
1193 char new_symbol[24];
1194
1195 sig->skolem_count++;
1196 sprintf(new_symbol,"esk%ld_%d",sig->skolem_count,arity);
1197 while(SigFindFCode(sig,new_symbol))
1198 {
1199 sig->skolem_count++;
1200 sprintf(new_symbol,"esk%ld_%d",sig->skolem_count,arity);
1201 }
1202 res = SigInsertId(sig, new_symbol, arity, false);
1203 return res;
1204 }
1205
1206
1207 /*-----------------------------------------------------------------------
1208 //
1209 // Function: SigGetNewPredicateCode()
1210 //
1211 // Return a new predicate symbol with arity n. The symbol will be of
1212 // the form epred<count>_<ar>, and is guaranteed to be new to sig.
1213 //
1214 // Global Variables: -
1215 //
1216 // Side Effects : Extends signature
1217 //
1218 /----------------------------------------------------------------------*/
1219
SigGetNewPredicateCode(Sig_p sig,int arity)1220 FunCode SigGetNewPredicateCode(Sig_p sig, int arity)
1221 {
1222 FunCode res;
1223 char new_symbol[26];
1224
1225 sig->newpred_count++;
1226 sprintf(new_symbol,"epred%ld_%d",sig->newpred_count,arity);
1227 while(SigFindFCode(sig,new_symbol))
1228 {
1229 sig->newpred_count++;
1230 sprintf(new_symbol,"epred%ld_%d",sig->newpred_count,arity);
1231 }
1232 res = SigInsertId(sig, new_symbol, arity, false);
1233
1234 return res;
1235 }
1236
1237
1238 /*-----------------------------------------------------------------------
1239 //
1240 // Function: SigDeclareType()
1241 //
1242 // Declare the type of the given function. Will fail (and crash) if
1243 // the type is already declared and is fixed.
1244 //
1245 // Global Variables: -
1246 //
1247 // Side Effects : Modifies the signature
1248 //
1249 /----------------------------------------------------------------------*/
1250
SigDeclareType(Sig_p sig,FunCode f,Type_p type)1251 void SigDeclareType(Sig_p sig, FunCode f, Type_p type)
1252 {
1253 Func_p fun;
1254
1255 fun = &sig->f_info[f];
1256 if(fun->type)
1257 {
1258 /* type already declared, check it's the same */
1259 if(!TypeEqual(fun->type, type))
1260 {
1261 if(SigIsFixedType(sig, f))
1262 {
1263 if(Verbose>=3)
1264 {
1265 fprintf(stderr, "# Type conflict for %s between ",
1266 SigFindName(sig, f));
1267 TypePrintTSTP(stderr, sig->type_table, fun->type);
1268 fprintf(stderr, " and ");
1269 TypePrintTSTP(stderr, sig->type_table, type);
1270 fprintf(stderr, "\n");
1271 }
1272 Error("type error", INPUT_SEMANTIC_ERROR);
1273 }
1274 else
1275 {
1276 if(Verbose >= 2)
1277 {
1278 fprintf(stderr, "# type re-declaration %s: ", SigFindName(sig, f));
1279 TypePrintTSTP(stderr, sig->type_table, type);
1280 fprintf(stderr, "\n");
1281 }
1282 fun->type = type;
1283 }
1284 }
1285 }
1286 else
1287 {
1288 if(Verbose >= 2)
1289 {
1290 fprintf(stderr, "# type declaration %s: ", SigFindName(sig, f));
1291 TypePrintTSTP(stderr, sig->type_table, type);
1292 fprintf(stderr, "\n");
1293 }
1294 fun->type = type;
1295 }
1296 }
1297
1298
1299 /*-----------------------------------------------------------------------
1300 //
1301 // Function: SigDeclareFinalType()
1302 //
1303 // Declare the type of the symbol, and fix it (cannot be changed)
1304 //
1305 // Global Variables: -
1306 //
1307 // Side Effects : Modifies the type table
1308 //
1309 /----------------------------------------------------------------------*/
1310
SigDeclareFinalType(Sig_p sig,FunCode f_code,Type_p type)1311 void SigDeclareFinalType(Sig_p sig, FunCode f_code, Type_p type)
1312 {
1313 SigDeclareType(sig, f_code, type);
1314 SigFixType(sig, f_code);
1315 }
1316
1317
1318 /*-----------------------------------------------------------------------
1319 //
1320 // Function: SigDeclareIsFunction()
1321 //
1322 // This symbol occurs in a function position (in an equation, as
1323 // a subterm...).
1324 //
1325 // Global Variables: -
1326 //
1327 // Side Effects : Modifies signature (may change the type)
1328 //
1329 /----------------------------------------------------------------------*/
1330
SigDeclareIsFunction(Sig_p sig,FunCode f_code)1331 void SigDeclareIsFunction(Sig_p sig, FunCode f_code)
1332 {
1333 Type_p type, new_type;
1334
1335 if(SigIsPolymorphic(sig, f_code))
1336 {
1337 return;
1338 }
1339
1340 type = SigGetType(sig, f_code);
1341 assert(type->domain_sort != STNoSort);
1342
1343 /* must update type */
1344 if(type->domain_sort == STBool)
1345 {
1346 new_type = TypeCopyWithReturn(sig->type_table, type, SigDefaultSort(sig));
1347 SigDeclareFinalType(sig, f_code, new_type);
1348 }
1349 else
1350 {
1351 SigFixType(sig, f_code);
1352 }
1353 }
1354
1355
1356 /*-----------------------------------------------------------------------
1357 //
1358 // Function: SigDeclareIsPredicate()
1359 //
1360 // This symbol occurs as a predicate, without ambiguity.
1361 //
1362 // Global Variables: -
1363 //
1364 // Side Effects : Modifies signature
1365 //
1366 /----------------------------------------------------------------------*/
SigDeclareIsPredicate(Sig_p sig,FunCode f_code)1367 void SigDeclareIsPredicate(Sig_p sig, FunCode f_code)
1368 {
1369 Type_p type, new_type;
1370
1371 if(SigIsPolymorphic(sig, f_code))
1372 {
1373 return;
1374 }
1375
1376 type = SigGetType(sig, f_code);
1377 assert(type->domain_sort != STNoSort);
1378
1379 /* must update type */
1380 if(type->domain_sort != STBool)
1381 {
1382 new_type = TypeCopyWithReturn(sig->type_table, type, STBool);
1383 SigDeclareFinalType(sig, f_code, new_type);
1384 }
1385 else
1386 {
1387 SigFixType(sig, f_code);
1388 }
1389 }
1390
1391
1392 /*-----------------------------------------------------------------------
1393 //
1394 // Function: SigPrintTypes()
1395 //
1396 // Prints symbols with their type to the given file descriptor.
1397 //
1398 //
1399 // Global Variables: -
1400 //
1401 // Side Effects : IO on the file descriptor
1402 //
1403 /----------------------------------------------------------------------*/
1404
SigPrintTypes(FILE * out,Sig_p sig)1405 void SigPrintTypes(FILE* out, Sig_p sig)
1406 {
1407 FunCode i;
1408 Func_p fun;
1409
1410 for(i=1; i <= sig->f_count; i++)
1411 {
1412 if (i > 1)
1413 {
1414 fputs(", ", out);
1415 }
1416
1417 fun = &sig->f_info[i];
1418 fprintf(out, "%s:", fun->name);
1419 if (!fun->type)
1420 {
1421 fputs("<no type>", out);
1422 }
1423 else
1424 {
1425 TypePrintTSTP(out, sig->type_table, fun->type);
1426 }
1427 }
1428 }
1429
1430
1431 /*-----------------------------------------------------------------------
1432 //
1433 // Function: SigParseTFFTypeDeclaration()
1434 //
1435 // Parses a type declaration, and update the signature if it is a
1436 // symbol declaration (ignores type declarations)
1437 //
1438 // Global Variables: -
1439 //
1440 // Side Effects : Reads from scanner, may raise an error
1441 //
1442 /----------------------------------------------------------------------*/
1443
SigParseTFFTypeDeclaration(Scanner_p in,Sig_p sig)1444 void SigParseTFFTypeDeclaration(Scanner_p in, Sig_p sig)
1445 {
1446 DStr_p id;
1447 FuncSymbType symbtype;
1448 FunCode f;
1449 Type_p type;
1450 bool within_paren = false;
1451
1452 id = DStrAlloc();
1453
1454 if(TestInpTok(in, OpenBracket))
1455 {
1456 NextToken(in);
1457 within_paren = true;
1458 }
1459
1460 /* parse symbol */
1461 symbtype = FuncSymbParse(in, id);
1462 if(symbtype == FSIdentVar || symbtype == FSNone)
1463 {
1464 Error("expected symbol in type declaration", OTHER_ERROR);
1465 }
1466
1467 /* parse type */
1468 AcceptInpTok(in, Colon);
1469 type = TypeParseTSTP(in, sig->type_table);
1470
1471 if(within_paren)
1472 {
1473 AcceptInpTok(in, CloseBracket);
1474 }
1475
1476 /* we only keep declarations of symbols, not declaration of types */
1477 if(type->domain_sort != STKind)
1478 {
1479 f = SigInsertId(sig, DStrView(id), type->arity, false);
1480 SigDeclareType(sig, f, type);
1481 SigFixType(sig, f);
1482 }
1483
1484 DStrFree(id);
1485 }
1486
1487
1488 /*---------------------------------------------------------------------*/
1489 /* End of File */
1490 /*---------------------------------------------------------------------*/
1491