1 /*-----------------------------------------------------------------------
2
3 File : cte_signature.h
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Definitions for dealing with signatures, i.e. data structures
10 storing information about function symbols and their properties.
11
12 Copyright 1998, 1999 by the author.
13 This code is released under the GNU General Public Licence and
14 the GNU Lesser General Public License.
15 See the file COPYING in the main E directory for details..
16 Run "eprover -h" for contact information.
17
18 Changes
19
20 <1> Thu Sep 18 16:54:31 MET DST 1997
21 New
22
23 -----------------------------------------------------------------------*/
24
25 #ifndef CTE_SIGNATURE
26
27 #define CTE_SIGNATURE
28
29 #include <clb_stringtrees.h>
30 #include <clb_pdarrays.h>
31 #include <clb_properties.h>
32 #include <cte_functypes.h>
33 #include <cte_simpletypes.h>
34
35 /*---------------------------------------------------------------------*/
36 /* Data type declarations */
37 /*---------------------------------------------------------------------*/
38
39
40 typedef enum
41 {
42 FPIgnoreProps = 0, /* No properties, mask everything out */
43 FPTypeFixed = 1, /* We are sure about the type of the symbol */
44 FPTypePoly = 2, /* Ad-hoc polymorphic predicate type */
45 FPFOFOp = 4, /* Symbol is encoded first order operator */
46 FPSpecial = 8, /* Symbol is a special symbol introduced internally */
47 FPAssociative = 16, /* Function symbol is binary and associative */
48 FPCommutative = 32, /* Function symbol is binary and commutates */
49 FPIsAC = FPAssociative|FPCommutative,
50 FPInterpreted = 64, /* Interpreted symbol $ident */
51 FPIsInteger = 128, /* Sequence of digits, may be semi-interpreted */
52 FPIsRational = 256, /* [-]a/b */
53 FPIsFloat = 512, /* Floating point number */
54 FPIsObject = 1024, /* ""-enclosed string, by definition denotes
55 unique object." */
56 FPDistinctProp = FPIsObject | FPIsInteger | FPIsRational | FPIsFloat,
57 FPOpFlag = 2048, /* Used for temporary oerations, by
58 * defintion off if not in use! */
59 FPClSplitDef = 4096, /* Predicate is a clause split defined
60 * symbol. */
61 FPPseudoPred = 8192 /* Pseudo-predicate used for side effects
62 * only, does not conceptually contribute to
63 * truth of clause */
64 }FunctionProperties;
65
66
67 /* Keep information about function symbols: Access external name and
68 arity (and possibly additional information at a later time) by
69 internal numerical code for function symbol. */
70
71 typedef struct funccell
72 {
73 /* f_code is implicit by position in the array */
74 char* name;
75 int arity;
76 int alpha_rank; /* We sometimes need an arbitrary but stable
77 order on symbols and use alphabetic. */
78 Type_p type; /* Simple type of the symbol */
79 FunctionProperties properties;
80 }FuncCell, *Func_p;
81
82
83 /* A signature contains information about function symbols with
84 direct access by internal code (f_info is organized as a array,
85 with f_info[f_code] being the information associated with f_code)
86 and efficient access by external name (via the f_index array).
87
88 Function codes are integers starting at 1, while variables are
89 encoded by negative integers. 0 is unused and can thus express
90 error conditions when accessing some things f_code. f_info[0] is
91 unused. */
92
93 #define DEFAULT_SIGNATURE_SIZE 20
94 #define DEFAULT_SIGNATURE_GROW 2
95
96 typedef struct sigcell
97 {
98 bool alpha_ranks_valid; /* The alpha-ranks are up to date */
99 long size; /* Size the array */
100 FunCode f_count; /* Largest used f_code */
101 FunCode internal_symbols; /* Largest auto-inserted internal symbol */
102 Func_p f_info; /* The array */
103 StrTree_p f_index; /* Back-assoc: Given a symbol, get the index */
104 PStack_p ac_axioms; /* All recognized AC axioms */
105 /* The following are special symbols needed for pattern
106 manipulation. We want very efficient access to them! Also
107 resused in FOF parsing. */
108 FunCode eqn_code;
109 FunCode neqn_code;
110 FunCode cnil_code;
111 PDArray_p orn_codes;
112
113 /* The following is for encoding first order formulae as terms. I
114 do like to reuse the robust sharing infrastructure for
115 CNFization and formula rewriting (inspired by Tommi Juntilla's
116 reuse of the same in MathSAT). */
117 FunCode not_code;
118 FunCode qex_code;
119 FunCode qall_code;
120 FunCode and_code;
121 FunCode or_code;
122 FunCode impl_code;
123 FunCode equiv_code;
124 FunCode nand_code;
125 FunCode nor_code;
126 FunCode bimpl_code;
127 FunCode xor_code;
128 /* And here are codes for interpreted symbols */
129 FunCode answer_code; /* For answer literals */
130
131 /* Sort and type banks (type => sort, but a shortcut is useful) */
132 SortTable_p sort_table;
133 TypeTable_p type_table;
134
135 /* Counters for generating new symbols */
136 long skolem_count;
137 long newpred_count;
138 /* Which properties are used for recognizing implicit distinctness?*/
139 FunctionProperties distinct_props;
140 }SigCell, *Sig_p;
141
142
143
144
145 /*---------------------------------------------------------------------*/
146 /* Exported Functions and Variables */
147 /*---------------------------------------------------------------------*/
148
149 /* Special constant for internal operations */
150
151 #define SIG_TRUE_CODE 1
152 #define SIG_FALSE_CODE 2
153 #define SIG_NIL_CODE 3
154 #define SIG_CONS_CODE 4
155
156 /* Handle properties */
157
158 #define FuncSetProp(symb, prop) SetProp((symb), (prop))
159 #define FuncDelProp(symb, prop) DelProp((symb), (prop))
160
161 /* Are _all_ properties in prop set for symb? */
162 #define FuncQueryProp(symb, prop) QueryProp((symb), (prop))
163
164 /* Are any properties in prop set in term? */
165 #define FuncIsAnyPropSet(symb, prop) IsAnyPropSet((symb), (prop))
166
167 /* With a more convenient external interface: */
168
169 #define SigSetFuncProp(sig, symb, prop) \
170 FuncSetProp(&(sig->f_info[(symb)]), (prop))
171 #define SigDelFuncProp(sig, symb, prop) \
172 FuncDelProp(&(sig->f_info[(symb)]), (prop))
173 #define SigQueryFuncProp(sig, symb, prop) \
174 FuncQueryProp(&(sig->f_info[(symb)]), (prop))
175 #define SigIsAnyFuncPropSet(sig, symb, prop) \
176 FuncIsAnyPropSet(&(sig->f_info[(symb)]), (prop))
177
178 extern bool SigSupportLists; /* Auto-Insert special symbols
179 $nil=3, $cons=4 for list
180 representations */
181 #define SigCellAlloc() (SigCell*)SizeMalloc(sizeof(SigCell))
182 #define SigCellFree(junk) SizeFree(junk, sizeof(SigCell))
183
184 Sig_p SigAlloc(SortTable_p sort_table);
185 void SigInsertInternalCodes(Sig_p sig);
186 void SigFree(Sig_p junk);
187 #define SigExternalSymbols(sig) \
188 ((sig)->f_count-(sig)->internal_symbols)
189
190 #define SigInterpreteNumbers(sig) ((sig)->null_code)
191
192 FunCode SigFindFCode(Sig_p sig, const char* name);
193 static __inline__ int SigFindArity(Sig_p sig, FunCode f_code);
194
195 static __inline__ char* SigFindName(Sig_p sig, FunCode f_code);
196 bool SigIsPredicate(Sig_p sig, FunCode f_code);
197 bool SigIsFunction(Sig_p sig, FunCode f_code);
198 bool SigIsFixedType(Sig_p sig, FunCode f_code);
199 void SigFixType(Sig_p sig, FunCode f_code);
200 bool SigIsPolymorphic(Sig_p sig, FunCode f_code);
201 void SigSetPolymorphic(Sig_p sig, FunCode f_code, bool value);
202 bool SigQueryProp(Sig_p sig, FunCode f, FunctionProperties prop);
203
204 #define SigIsFunConst(sig, f_code) (SigFindArity((sig), (f_code))==0&&\
205 SigIsPredicate((sig),(f_code)))
206 #define SigIsSimpleAnswerPred(sig, f_code) \
207 ((f_code)==(sig)->answer_code)
208
209 void SigSetSpecial(Sig_p sig, FunCode f_code, bool value);
210 void SigSetAllSpecial(Sig_p sig, bool value);
211 bool SigIsSpecial(Sig_p sig, FunCode f_code);
212 int SigGetAlphaRank(Sig_p sig, FunCode f_code);
213
214 FunCode SigInsertId(Sig_p sig, const char* name, int arity, bool
215 special_id);
216 FunCode SigInsertFOFOp(Sig_p sig, const char* name, int arity);
217 void SigPrint(FILE* out, Sig_p sig);
218 void SigPrintSpecial(FILE* out, Sig_p sig);
219 void SigPrintACStatus(FILE* out, Sig_p sig);
220 FunCode SigParseKnownOperator(Scanner_p in, Sig_p sig);
221 FunCode SigParseSymbolDeclaration(Scanner_p in, Sig_p sig, bool special_id);
222 FunCode SigParse(Scanner_p in, Sig_p sig, bool special_ids);
223 int SigFindMaxUsedArity(Sig_p sig);
224 int SigFindMaxPredicateArity(Sig_p sig);
225 int SigFindMinPredicateArity(Sig_p sig);
226 int SigFindMaxFunctionArity(Sig_p sig);
227 int SigFindMinFunctionArity(Sig_p sig);
228 int SigCountAritySymbols(Sig_p sig, int arity, bool predicates);
229 int SigCountSymbols(Sig_p sig, bool predicates);
230 int SigAddSymbolArities(Sig_p sig, PDArray_p distrib, bool
231 predicates, long selection[]);
232
233 /* Special functions for dealing with special symbols */
234
235 static __inline__ FunCode SigGetEqnCode(Sig_p sig, bool positive);
236 FunCode SigGetOtherEqnCode(Sig_p sig, FunCode f_code);
237 static __inline__ FunCode SigGetOrCode(Sig_p sig);
238 static __inline__ FunCode SigGetCNilCode(Sig_p sig);
239 FunCode SigGetOrNCode(Sig_p sig, int arity);
240 FunCode SigGetNewSkolemCode(Sig_p sig, int arity);
241 FunCode SigGetNewPredicateCode(Sig_p sig, int arity);
242
243 /* Types */
244 #define SigDefaultSort(sig) ((sig)->sort_table->default_type)
245 #define SigGetType(sig, f) ((sig)->f_info[(f)].type)
246 void SigDeclareType(Sig_p sig, FunCode f, Type_p type);
247 void SigDeclareFinalType(Sig_p sig, FunCode f, Type_p type);
248 void SigDeclareIsFunction(Sig_p sig, FunCode f);
249 void SigDeclareIsPredicate(Sig_p sig, FunCode f);
250 void SigPrintTypes(FILE* out, Sig_p sig);
251 void SigParseTFFTypeDeclaration(Scanner_p in, Sig_p sig);
252
253 /*---------------------------------------------------------------------*/
254 /* Inline functions */
255 /*---------------------------------------------------------------------*/
256
257
258 /*-----------------------------------------------------------------------
259 //
260 // Function: SigFindArity()
261 //
262 // Given signature and a function symbol code, return the arity of
263 // the symbol.
264 //
265 // Global Variables: -
266 //
267 // Side Effects : Abort if illegal f_code
268 //
269 /----------------------------------------------------------------------*/
270
SigFindArity(Sig_p sig,FunCode f_code)271 static __inline__ int SigFindArity(Sig_p sig, FunCode f_code)
272 {
273 assert(f_code > 0);
274 assert(f_code <= sig->f_count);
275
276 return (sig->f_info[f_code]).arity;
277 }
278
279
280 /*-----------------------------------------------------------------------
281 //
282 // Function: SigFindName()
283 //
284 // Given signature and a function symbol code, return a pointer to
285 // the name. This pointer is only valid as long as the signature
286 // exists!
287 //
288 // Global Variables: -
289 //
290 // Side Effects : Abort if illegal f_code
291 //
292 /----------------------------------------------------------------------*/
293
SigFindName(Sig_p sig,FunCode f_code)294 static __inline__ char* SigFindName(Sig_p sig, FunCode f_code)
295 {
296 assert(f_code > 0);
297 assert(f_code <= sig->f_count);
298
299 return (sig->f_info[f_code]).name;
300 }
301
302
303 /*-----------------------------------------------------------------------
304 //
305 // Function: SigGetEqnCode()
306 //
307 // Return the FunCode for $eq or $neq, create them if non-existant.
308 //
309 // Global Variables: -
310 //
311 // Side Effects : May change sig
312 //
313 /----------------------------------------------------------------------*/
314
SigGetEqnCode(Sig_p sig,bool positive)315 static __inline__ FunCode SigGetEqnCode(Sig_p sig, bool positive)
316 {
317 assert(sig);
318
319 if(positive)
320 {
321 if(sig->eqn_code)
322 {
323 return sig->eqn_code;
324 }
325 sig->eqn_code = SigInsertId(sig, "$eq", 2, true);
326 assert(sig->eqn_code);
327 SigSetFuncProp(sig, sig->eqn_code, FPFOFOp | FPTypePoly);
328 return sig->eqn_code;
329 }
330 else
331 {
332 if(sig->neqn_code)
333 {
334 return sig->neqn_code;
335 }
336 sig->neqn_code = SigInsertId(sig, "$neq", 2, true);
337 assert(sig->neqn_code);
338 SigSetFuncProp(sig, sig->eqn_code, FPFOFOp | FPTypePoly);
339 return sig->neqn_code;
340 }
341 }
342
343
344 /*-----------------------------------------------------------------------
345 //
346 // Function: SigGetOrCode()
347 //
348 // As above, for $or
349 //
350 // Global Variables: -
351 //
352 // Side Effects : May change sig
353 //
354 /----------------------------------------------------------------------*/
355
SigGetOrCode(Sig_p sig)356 static __inline__ FunCode SigGetOrCode(Sig_p sig)
357 {
358 assert(sig);
359
360 if(sig->or_code)
361 {
362 return sig->or_code;
363 }
364 sig->or_code = SigInsertId(sig, "$or", 2, true);
365 assert(sig->or_code);
366 return sig->or_code;
367 }
368
369
370 /*-----------------------------------------------------------------------
371 //
372 // Function: SigGetCNilCode()
373 //
374 // As above, for $cnil
375 //
376 // Global Variables: -
377 //
378 // Side Effects : May change sig
379 //
380 /----------------------------------------------------------------------*/
381
SigGetCNilCode(Sig_p sig)382 static __inline__ FunCode SigGetCNilCode(Sig_p sig)
383 {
384 assert(sig);
385
386 if(sig->cnil_code)
387 {
388 return sig->cnil_code;
389 }
390 sig->cnil_code = SigInsertId(sig, "$cnil", 0, true);
391 assert(sig->cnil_code);
392 return sig->cnil_code;
393 }
394
395
396 #endif
397
398 /*---------------------------------------------------------------------*/
399 /* End of File */
400 /*---------------------------------------------------------------------*/
401
402
403
404
405
406