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 * Stack-based API for building terms and types.
21 * Intended to support parsing.
22 *
23 * The stack contains a nested sequence of frames. Each frame
24 * consists of an operator (term or type constructor) and a sequence
25 * of arguments. The arguments are string (that may denote symbols),
26 * bindings, rationals or bitvector constants, buffers, terms, or types.
27 *
28 * Bindings are pairs <name, term>. They record temporary bindings from
29 * names to terms (for let, forall, exists). The binding of name to term
30 * is erased when the binding is deleted.
31 *
32 * Added May 27, 2013: to support the (as ...) construct in SMTLIB2, we
33 * can also store op codes as arguments.
34 *
35 * To help reporting errors, each element on the stack has location
36 * information.
37 *
38 * Each operation is defined by an op code and implemented by two functions:
39 * - one for checking types and number of arguments
40 * - one for applying the operation to the arguments
41 * Both have the following signature:
42 * - void check_op(tstack_t *stack, stack_elem_t *f, uint32_t n)
43 * - void eval_op(tstack_t *stack, stack_elem_t *f, uint32_t n)
44 * f is the start of a frame in stack->elem
45 * n = the size of the frame = number of arguments
46 *
47 * For example, if the stack contains a frame with operator code MK_AND
48 * and 4 arguments, then the top frame is [MK_AND <arg1> ... <arg4>]
49 *
50 * tstack_eval will invoke eval_mk_and(stack, f, n)
51 * with f pointing to array [<arg1> .... <arg4>] and n = 4
52 *
53 * The check function must raise an exception if the arguments or
54 * frame are incorrect. The eval function must replace the frame
55 * by the result of the operation.
56 *
57 * The module implements basic operations. More can be added.
58 */
59
60 #ifndef __TERM_STACK2_H
61 #define __TERM_STACK2_H
62
63 #include <stdint.h>
64 #include <stdbool.h>
65 #include <setjmp.h>
66
67 #include "frontend/smt2/attribute_values.h"
68 #include "terms/bvlogic_buffers.h"
69 #include "terms/terms.h"
70 #include "utils/arena.h"
71
72
73 /*
74 * Objects on the stack
75 * - tag = identifies the object's type
76 * - val = union type
77 * - loc = location information for error reporting
78 *
79 * For operators, we record an opcode, a multiplicity index (for associative
80 * operators), and the index of the previous operator on the stack.
81 *
82 * Note: an opcode is stored as just an integer (different from TAG_OP)
83 *
84 * Added 2018/05/31: a new tag to record that a term requires special processing.
85 * ----------------
86 * This is used in the SMT2 front-end to handle named assertions and unsat cores.
87 * In a named assertion: (assert (! <term> :named xxx)), we mark <term>
88 * as special so that it is can be treated as an assumption and not as a regular
89 * assertion. The only operation that introduces a SPECIAL_TERM is set_special_term_result.
90 *
91 * Added 2018/06/02: another new tag to handle the check-sat-assuming command.
92 * ----------------
93 * The arguments to check-sat-assuming is a list of assumptions. Each assumption
94 * can be either a SYMBOL or of the form (not SYMBOL). We add TAG_NOT_SYMBOL just
95 * for the latter.
96 */
97 typedef enum tag_enum {
98 TAG_NONE,
99 TAG_OP, // operator
100 TAG_OPCODE, // opcode as argument
101 TAG_SYMBOL, // symbol
102 TAG_NOT_SYMBOL, // negation of a symbol
103 TAG_STRING, // string constant
104 TAG_BV64, // bit-vector constant (1 to 64 bits)
105 TAG_BV, // bit-vector constant (more than 64 bits)
106 TAG_RATIONAL, // rational constant
107 TAG_TERM, // term index + polarity (from the global term table)
108 TAG_SPECIAL_TERM, // a term marked for special processing
109 TAG_TYPE, // type index (from the global type table)
110 TAG_MACRO, // type macro (index in the type table)
111 TAG_ATTRIBUTE, // attribute value (index in an attribute value table)
112 TAG_ARITH_BUFFER, // polynomial buffer (rational coefficients)
113 TAG_BVARITH64_BUFFER, // polynomial buffer (bitvector coefficients, 1 to 64 bits)
114 TAG_BVARITH_BUFFER, // polynomial buffer (bitvector coefficients, more than 64 bits)
115 TAG_BVLOGIC_BUFFER, // array of bits
116 TAG_BINDING, // pair <name, term>
117 TAG_TYPE_BINDING, // pair <name, type>
118 } tag_t;
119
120 #define NUM_TAGS (TAG_TYPE_BINDING+1)
121
122 // operator
123 typedef struct opval_s {
124 int32_t opcode;
125 uint32_t multiplicity;
126 uint32_t prev;
127 } opval_t;
128
129 // binding
130 typedef struct binding_s {
131 term_t term;
132 char *symbol;
133 } binding_t;
134
135 // type binding
136 typedef struct type_binding_s {
137 type_t type;
138 char *symbol;
139 } type_binding_t;
140
141 // location: line + column number
142 typedef struct loc_s {
143 uint32_t line;
144 uint32_t column;
145 } loc_t;
146
147 // two variant representations for bitvector constants
148 // one for bitsize between 1 and 64
149 // one for bitsize > 64
150 typedef struct bv64_s {
151 uint32_t bitsize; // size in bits
152 uint64_t value; // value (padded to 64 bits)
153 } bv64_t;
154
155 typedef struct bv_s {
156 uint32_t bitsize; // size in bits
157 uint32_t *data; // value as an array of 32bit words
158 } bv_t;
159
160
161 // element on the stack
162 typedef struct stack_elem_s {
163 tag_t tag;
164 union {
165 opval_t opval;
166 char *string;
167 bv64_t bv64;
168 bv_t bv;
169 rational_t rational;
170 int32_t op;
171 term_t term;
172 type_t type;
173 int32_t macro;
174 aval_t aval;
175 rba_buffer_t *arith_buffer;
176 bvarith64_buffer_t *bvarith64_buffer;
177 bvarith_buffer_t *bvarith_buffer;
178 bvlogic_buffer_t *bvlogic_buffer;
179 binding_t binding;
180 type_binding_t type_binding;
181 } val;
182 loc_t loc;
183 } stack_elem_t ;
184
185
186 /*
187 * Symbols/negated symbol in the symbol buffer
188 * - polarity true means 'symbol'
189 * - polarity false means 'not symbol'
190 */
191 typedef struct signed_symbol_s {
192 const char *name;
193 bool polarity;
194 } signed_symbol_t;
195
196 #define MAX_SBUFFER_SIZE (UINT32_MAX/sizeof(signed_symbol_t))
197
198 /*
199 * Operator table
200 * - num ops = number of operators
201 * - for each op:
202 * assoc[op] = true if op is to be treated as an associative operator
203 * check[op] = check function
204 * eval[op] = evaluation function
205 * - size = size of arrays assoc, check, and eval
206 */
207 typedef struct tstack_s tstack_t;
208 // type of evaluator and check functions
209 typedef void (*eval_fun_t)(tstack_t *stack, stack_elem_t *f, uint32_t n);
210 typedef eval_fun_t check_fun_t;
211
212 typedef struct op_table_s {
213 uint8_t *assoc;
214 eval_fun_t *eval;
215 check_fun_t *check;
216 uint32_t num_ops;
217 uint32_t size;
218 } op_table_t;
219
220 #define MAX_OP_TABLE_SIZE (UINT32_MAX/sizeof(eval_fun_t))
221
222 /*
223 * Stack:
224 * - array of stack_elements
225 * - top = top of the stack
226 * elements are stored at indices 0 ... top-1
227 * a bottom marker is stored at index 0
228 * - frame = index of the top-frame, element at that index must be an operator
229 * - top_op = opcode of the element at index frame
230 *
231 * - mem = arena for allocation of strings/symbols
232 *
233 * - auxiliary buffers for internal computations
234 * - a global counter for creating fresh variables
235 * - a longjmp buffer for simulating exceptions
236 *
237 * - some operations store a term or type result in
238 * stack->result.term or stack->result.type
239 *
240 * - optional component: if attribute-values are used, then
241 * the stack must have a pointer to the attribute-value table
242 * (for refcounts).
243 *
244 * - diagnosis data for error reporting is stored in
245 * error_loc = loc[i] if error occurred on element i
246 * error_op = operator being evaluated when the error occurred
247 * (or NO_OP if the error occurred on a push operation)
248 * error_string = null-terminated string value if the erroneous
249 * argument is a string (or NULL).
250 */
251 struct tstack_s {
252 stack_elem_t *elem;
253
254 uint32_t top;
255 uint32_t size;
256 uint32_t frame;
257 int32_t top_op;
258
259 // operator table
260 op_table_t op_table;
261
262 // arena
263 arena_t mem;
264
265 // vector to store types or terms
266 int32_t *aux_buffer;
267 uint32_t aux_size;
268
269 // vector to store symbols/negated symbols
270 signed_symbol_t *sbuffer;
271 uint32_t sbuffer_size;
272
273 // buffer to convert stack elements to bitvector constants
274 bvconstant_t bvconst_buffer;
275
276 // dynamically allocated buffers
277 rba_buffer_t *abuffer;
278 bvarith64_buffer_t *bva64buffer;
279 bvarith_buffer_t *bvabuffer;
280 bvlogic_buffer_t *bvlbuffer;
281
282 // counter for type-variable creation
283 uint32_t tvar_id;
284
285 // result of BUILD_TERM/BUILD_TYPE
286 union {
287 term_t term;
288 type_t type;
289 } result;
290
291 // external table (NULL by default)
292 attr_vtbl_t *avtbl;
293
294 // exceptions/errors
295 jmp_buf env;
296 loc_t error_loc;
297 int32_t error_op;
298 char *error_string;
299 };
300
301
302 /*
303 * Default and maximal size
304 */
305 #define DEFAULT_TERM_STACK_SIZE 256
306 #define MAX_TERM_STACK_SIZE (UINT32_MAX/sizeof(stack_elem_t))
307
308 /*
309 * Default and maximal size of the t_aux vector
310 */
311 #define DEFAULT_AUX_SIZE 256
312 #define MAX_AUX_SIZE (UINT32_MAX/4)
313
314
315 /*
316 * Exception handling via setjmp and longjmp:
317 * -----------------------------------------
318 * To set the handler call setjmp(stack->env)
319 * The exception handler is called on any error
320 * via longjmp(stack->env, error_code).
321 *
322 * When an exception is raised, the stack may be in an inconsistent
323 * state. Do not do any operations on the stack without calling
324 * tstack_reset first.
325 */
326
327 /*
328 * Error codes (for Yices and SMT-LIB 1.2)
329 * SMT-LIB 2 adds more exception codes.
330 */
331 typedef enum tstack_error_s {
332 TSTACK_NO_ERROR = 0,
333 TSTACK_INTERNAL_ERROR,
334 TSTACK_OP_NOT_IMPLEMENTED,
335 TSTACK_UNDEF_TERM,
336 TSTACK_UNDEF_TYPE,
337 TSTACK_UNDEF_MACRO,
338 TSTACK_RATIONAL_FORMAT,
339 TSTACK_FLOAT_FORMAT,
340 TSTACK_BVBIN_FORMAT,
341 TSTACK_BVHEX_FORMAT,
342 TSTACK_TYPENAME_REDEF,
343 TSTACK_TERMNAME_REDEF,
344 TSTACK_MACRO_REDEF,
345 TSTACK_DUPLICATE_SCALAR_NAME,
346 TSTACK_DUPLICATE_VAR_NAME,
347 TSTACK_DUPLICATE_TYPE_VAR_NAME,
348 TSTACK_INVALID_OP,
349 TSTACK_INVALID_FRAME,
350 TSTACK_INTEGER_OVERFLOW,
351 TSTACK_NEGATIVE_EXPONENT,
352 TSTACK_NOT_AN_INTEGER,
353 TSTACK_NOT_A_STRING,
354 TSTACK_NOT_A_SYMBOL,
355 TSTACK_NOT_A_RATIONAL,
356 TSTACK_NOT_A_TYPE,
357 TSTACK_ARITH_ERROR,
358 TSTACK_DIVIDE_BY_ZERO,
359 TSTACK_NON_CONSTANT_DIVISOR,
360 TSTACK_NONPOSITIVE_BVSIZE,
361 TSTACK_INCOMPATIBLE_BVSIZES,
362 TSTACK_INVALID_BVCONSTANT,
363 TSTACK_BVARITH_ERROR,
364 TSTACK_BVLOGIC_ERROR,
365 TSTACK_TYPE_ERROR_IN_DEFTERM,
366 TSTACK_STRINGS_ARE_NOT_TERMS, // this can be raised only in the SMT2 lib context
367 TSTACK_YICES_ERROR,
368 } tstack_error_t;
369
370 #define NUM_TSTACK_ERRORS (TSTACK_YICES_ERROR+1)
371
372
373 /*
374 * PREDEFINED OPERATIONS
375 */
376 enum base_opcodes {
377 NO_OP, // used as a marker
378
379 // global definitions
380 DEFINE_TYPE, // [define-type <symbol>] or [define-type <symbol> <type>]
381 DEFINE_TERM, // [define-term <symbol> <type>] or [define-term <symbol> <type> <value> ]
382
383 // bindings
384 BIND, // [bind <symbol> <term> ]
385 DECLARE_VAR, // [declare-var <symbol> <type> ]
386 DECLARE_TYPE_VAR, // [declare-type-var <symbol> ]
387 LET, // [let <binding> ... <binding> <term> ]
388
389 // type constructors
390 MK_BV_TYPE, // [mk-bv-type <rational> ]
391 MK_SCALAR_TYPE, // [mk-scalar-type <symbol> ... <symbol> ]
392 MK_TUPLE_TYPE, // [mk-tuple-type <type> ... <type> ]
393 MK_FUN_TYPE, // [mk-fun-type <type> ... <type> ]
394 MK_APP_TYPE, // [mk-app-type <macro> <type> ... <type> ]
395
396 // basic term constructors
397 MK_APPLY, // [mk-apply <term> ... <term> ]
398 MK_ITE, // [mk-ite <term> <term> <term> ]
399 MK_EQ, // [mk-eq <term> <term> ]
400 MK_DISEQ, // [mk-diseq <term> <term> ]
401 MK_DISTINCT, // [mk-distinct <term> ... <term> ]
402 MK_NOT, // [mk-not <term> ]
403 MK_OR, // [mk-or <term> ... <term> ]
404 MK_AND, // [mk-and <term> ... <term> ]
405 MK_XOR, // [mk-xor <term> ... <term> ]
406 MK_IFF, // [mk-iff <term> <term> ]
407 MK_IMPLIES, // [mk-implies <term> <term> ]
408 MK_TUPLE, // [mk-tuple <term> ... <term> ]
409 MK_SELECT, // [mk-select <term> <rational> ]
410 MK_TUPLE_UPDATE, // [mk-tuple-update <term> <rational> <term> ]
411 MK_UPDATE, // [mk-update <term> <term> .... <term> ]
412 MK_FORALL, // [mk-forall <binding> ... <binding> <term> ]
413 MK_EXISTS, // [mk-exists <binding> ... <binding> <term> ]
414 MK_LAMBDA, // [mk-lambda <binding> ... <binding> <term> ]
415
416 // arithmetic
417 MK_ADD, // [mk-add <arith> ... <arith> ]
418 MK_SUB, // [mk-sub <arith> ... <arith> ]
419 MK_NEG, // [mk-neg <arith> ]
420 MK_MUL, // [mk-mul <arith> ... <arith> ]
421 MK_DIVISION, // [mk-division <arith> <arith> ]
422 MK_POW, // [mk-pow <arith> <integer> ]
423 MK_GE, // [mk-ge <arith> <arith> ]
424 MK_GT, // [mk-gt <arith> <arith> ]
425 MK_LE, // [mk-le <arith> <arith> ]
426 MK_LT, // [mk-lt <arith> <arith> ]
427
428 // bitvector arithmetic
429 MK_BV_CONST, // [mk-bv-const <size> <value> ]
430 MK_BV_ADD, // [mk-bv-add <bv> ... <bv> ]
431 MK_BV_SUB, // [mk-bv-sub <bv> ... <bv> ]
432 MK_BV_MUL, // [mk-bv-mul <bv> ... <bv> ]
433 MK_BV_NEG, // [mk-bv-neg <bv> ]
434 MK_BV_POW, // [mk-bv-pow <bv> <integer> ]
435 MK_BV_DIV, // [mk-bv-div <bv> <bv> ]
436 MK_BV_REM, // [mk-bv-rem <bv> <bv> ]
437 MK_BV_SDIV, // [mk-bv-sdiv <bv> <bv> ]
438 MK_BV_SREM, // [mk-bv-srem <bv> <bv> ]
439 MK_BV_SMOD, // [mk-bv-smod <bv> <bv> ]
440
441 MK_BV_NOT, // [mk-bv-not <bv> ]
442 MK_BV_AND, // [mk-bv-and <bv> ... <bv> ]
443 MK_BV_OR, // [mk-bv-or <bv> ... <bv> ]
444 MK_BV_XOR, // [mk-bv-xor <bv> ... <bv> ]
445 MK_BV_NAND, // [mk-bv-nand <bv> ... <bv> ]
446 MK_BV_NOR, // [mk-bv-nor <bv> ... <bv> ]
447 MK_BV_XNOR, // [mk-bv-xnor <bv> ... <bv> ]
448
449 MK_BV_SHIFT_LEFT0, // [mk-bv-shift-left0 <bv> <integer> ]
450 MK_BV_SHIFT_LEFT1, // [mk-bv-shift-left1 <bv> <integer> ]
451 MK_BV_SHIFT_RIGHT0, // [mk-bv-shift-right0 <bv> <integer> ]
452 MK_BV_SHIFT_RIGHT1, // [mk-bv-shift-right1 <bv> <integer> ]
453 MK_BV_ASHIFT_RIGHT, // [mk-bv-ashift-right <bv> <integer> ]
454 MK_BV_ROTATE_LEFT, // [mk-bv-rotate-left <bv> <rational> ]
455 MK_BV_ROTATE_RIGHT, // [mk-bv-rotate-right <bv> <rational> ]
456
457 MK_BV_SHL, // [mk-bv-shl <bv> <bv> ]
458 MK_BV_LSHR, // [mk-bv-lshr <bv> <bv> ]
459 MK_BV_ASHR, // [mk-bv-ashr <bv> <bv> ]
460
461 MK_BV_EXTRACT, // [mk-bv-extract <rational> <rational> <bv> ]
462 MK_BV_CONCAT, // [mk-bv-concat <bv> ... <bv> ]
463 MK_BV_REPEAT, // [mk-bv-repeat <bv> <rational> ]
464 MK_BV_SIGN_EXTEND, // [mk-bv-sign-extend <bv> <rational> ]
465 MK_BV_ZERO_EXTEND, // [mk-bv-zero-extend <bv> <rational> ]
466
467 MK_BV_REDAND, // [mk-bv-redand <bv> ]
468 MK_BV_REDOR, // [mk-bv-redor <bv> ]
469 MK_BV_COMP, // [mk-bv-comp <bv> <bv> ]
470
471 MK_BV_GE, // [mk-bv-ge <bv> <bv> ]
472 MK_BV_GT, // [mk-bv-gt <bv> <bv> ]
473 MK_BV_LE, // [mk-bv-le <bv> <bv> ]
474 MK_BV_LT, // [mk-bv-lt <bv> <bv> ]
475 MK_BV_SGE, // [mk-bv-sge <bv> <bv> ]
476 MK_BV_SGT, // [mk-bv-sgt <bv> <bv> ]
477 MK_BV_SLE, // [mk-bv-sle <bv> <bv> ]
478 MK_BV_SLT, // [mk-bv-slt <bv> <bv> ]
479
480 MK_BOOL_TO_BV, // [mk-bool-to-bv <bool> .... <bool>]
481 MK_BIT, // [mk-bit <bv> <index>]
482
483 MK_FLOOR, // [mk-floor <arith> ]
484 MK_CEIL, // [mk-ceil <arith> ]
485 MK_ABS, // [mk-abs <arith> ]
486 MK_IDIV, // [mk-idiv <arith> <arith> ]
487 MK_MOD, // [mk-idiv <arith> <arith> ]
488 MK_DIVIDES, // [mk-divides <arith> <arith> ]
489 MK_IS_INT, // [mk-is-int <arith> ]
490
491 // collect result
492 BUILD_TERM, // [build-term <term> ]
493 BUILD_TYPE, // [build-type <type> ]
494 };
495
496
497 #define NUM_BASE_OPCODES (BUILD_TYPE + 1)
498
499
500 /*
501 * Initialization
502 * - n = size of the operator table (must be >= NUM_BASE_OPCODES)
503 * - the op_table is initialized: all default operators are defined
504 */
505 extern void init_tstack(tstack_t *stack, uint32_t n);
506
507
508 /*
509 * Add an attribute-value table
510 * - must be done after init_tstack and before any operation
511 * that add attribute values
512 */
tstack_set_avtbl(tstack_t * stack,attr_vtbl_t * table)513 static inline void tstack_set_avtbl(tstack_t *stack, attr_vtbl_t *table) {
514 assert(stack->avtbl == NULL);
515 stack->avtbl = table;
516 }
517
518
519 /*
520 * Add or replace an operator
521 * - op = operator code
522 * - asssoc = whether op is associative or not
523 * - eval. check = evaluator and checker functions
524 * - op must be non-negative and less than the operator's table size
525 * (set in init_tstack)
526 *
527 * If op is between 0 and stack->op_table.num_ops then the
528 * current values for op are replaced. If op is larger than
529 * num_ops, then a new operation is added.
530 */
531 extern void tstack_add_op(tstack_t *stack, int32_t op, bool assoc, eval_fun_t eval, check_fun_t check);
532
533 /*
534 * Empty the stack
535 */
536 extern void tstack_reset(tstack_t *stack);
537
538 /*
539 * Delete all
540 */
541 extern void delete_tstack(tstack_t *stack);
542
543
544 /*
545 * PUSH DATA OR OPERATOR
546 */
547
548 /*
549 * Push an operator op
550 * - op = opcode
551 * - loc = location
552 * op is considered valid if it's between 0 and num_ops
553 *
554 * This starts a new frame.
555 *
556 * In DEBUG mode: raise exception TSTACK_INVALID_OP if op is invalid and set
557 * stack->error_loc = loc
558 * stack->error_op = op
559 * stack->error_string = NULL
560 */
561 extern void tstack_push_op(tstack_t *stack, int32_t op, loc_t *loc);
562
563 /*
564 * Push opcode op (to be used as argument to another operation)
565 * - this does not modify the current frame, just push op on top of the current frame.
566 *
567 * In DEBUG mode, raise exception TSTACK_INVALID_OP if op is invalid (same as above)
568 */
569 extern void tstack_push_opcode(tstack_t *stack, int32_t op, loc_t *loc);
570
571 /*
572 * Push a string or symbol of length n
573 * - tag should be either TAG_SYMBOL or TAG_STRING
574 * - copy s[0] ... s[n-1] and add '\0'
575 * - s must be terminated by '\0'
576 */
577 extern void tstack_push_str(tstack_t *stack, tag_t tag, char *s, uint32_t n, loc_t *loc);
578
tstack_push_string(tstack_t * stack,char * s,uint32_t n,loc_t * loc)579 static inline void tstack_push_string(tstack_t *stack, char *s, uint32_t n, loc_t *loc) {
580 tstack_push_str(stack, TAG_STRING, s, n, loc);
581 }
582
tstack_push_symbol(tstack_t * stack,char * s,uint32_t n,loc_t * loc)583 static inline void tstack_push_symbol(tstack_t *stack, char *s, uint32_t n, loc_t *loc) {
584 tstack_push_str(stack, TAG_SYMBOL, s, n, loc);
585 }
586
tstack_push_not_symbol(tstack_t * stack,char * s,uint32_t n,loc_t * loc)587 static inline void tstack_push_not_symbol(tstack_t *stack, char *s, uint32_t n, loc_t *loc) {
588 tstack_push_str(stack, TAG_NOT_SYMBOL, s, n, loc);
589 }
590
591
592 /*
593 * These functions are like push_symbol but they raise an exception if
594 * the name s is already used (TSTACK_TYPENAME_REDEF,
595 * TSTACK_TERMNAME_REDEF, or TSTACK_MACRO_REDEF)
596 */
597 extern void tstack_push_free_typename(tstack_t *stack, char *s, uint32_t n, loc_t *loc);
598 extern void tstack_push_free_termname(tstack_t *stack, char *s, uint32_t n, loc_t *loc);
599 extern void tstack_push_free_macroname(tstack_t *stack, char *s, uint32_t n, loc_t *loc);
600
601 /*
602 * Variant: raise exception (TSTACK_TYPENAME_REDEF) if s is already
603 * used either as a type or as a macro name
604 */
605 extern void tstack_push_free_type_or_macro_name(tstack_t *stack, char *s, uint32_t n, loc_t *loc);
606
607
608 /*
609 * Find the term or type of name s and push that term or type on the stack
610 *
611 * raise exception TSTACK_UNDEF_TERM, TSTACK_UNDEF_TYPE, or TSTACK_UNDEF_MACRO
612 * if the name is not mapped to a term, type, or macro.
613 */
614 extern void tstack_push_type_by_name(tstack_t *stack, char *s, loc_t *loc);
615 extern void tstack_push_term_by_name(tstack_t *stack, char *s, loc_t *loc);
616 extern void tstack_push_macro_by_name(tstack_t *stack, char *s, loc_t *loc);
617
618 /*
619 * Convert a string to a rational and push that
620 * - s must be null-terminated and of rational or floating point formats
621 * (cf. rational.h, yices.h)
622 *
623 * raise exception TSTACK_FORMAT_... if the string s does not have
624 * the right format, and set
625 * stack->error_loc = loc
626 * stack->error_op = NO_OP
627 * stack->error_string = s
628 */
629 extern void tstack_push_rational(tstack_t *stack, char *s, loc_t *loc);
630 extern void tstack_push_float(tstack_t *stack, char *s, loc_t *loc);
631
632 /*
633 * Convert a string to a bitvector constant an push that
634 * - n = length of the string
635 * - s must be a string of binary or hexadecimal digits (no prefix)
636 *
637 * raise exception TSTACK_FORMAT_... if the string s does not have
638 * the right format, and set
639 * stack->error_loc = loc
640 * stack->error_op = NO_OP
641 * stack->error_string = s
642 */
643 extern void tstack_push_bvbin(tstack_t *stack, char *s, uint32_t n, loc_t *loc);
644 extern void tstack_push_bvhex(tstack_t *stack, char *s, uint32_t n, loc_t *loc);
645
646 /*
647 * Push primitive types or terms
648 */
649 extern void tstack_push_bool_type(tstack_t *stack, loc_t *loc);
650 extern void tstack_push_int_type(tstack_t *stack, loc_t *loc);
651 extern void tstack_push_real_type(tstack_t *stack, loc_t *loc);
652 extern void tstack_push_true(tstack_t *stack, loc_t *loc);
653 extern void tstack_push_false(tstack_t *stack, loc_t *loc);
654
655 /*
656 * Push integer constants
657 */
658 extern void tstack_push_int32(tstack_t *stack, int32_t val, loc_t *loc);
659
660 /*
661 * Push terms or types built by other means:
662 * use these functions for predefined SMT-LIB terms and types
663 */
664 extern void tstack_push_term(tstack_t *stack, term_t t, loc_t *loc);
665 extern void tstack_push_type(tstack_t *stack, type_t tau, loc_t *loc);
666 extern void tstack_push_macro(tstack_t *stack, int32_t id, loc_t *loc);
667
668
669 /*
670 * EVALUATION
671 */
672
673 /*
674 * Eval: execute the operation defined by the top-level operator OP,
675 * applied to all the arguments on top of OP on the stack.
676 *
677 * Replace [op arg1 ... argn] by the result of the operation.
678 */
679 extern void tstack_eval(tstack_t *stack);
680
681 /*
682 * Check whether the stack is empty
683 */
tstack_is_empty(tstack_t * stack)684 static inline bool tstack_is_empty(tstack_t *stack) {
685 return stack->top == 1;
686 }
687
688 /*
689 * Read result.
690 *
691 * Call sequence to use these functions:
692 * 1) tstack_push_op(stack, BUILD_TERM, xxx)
693 * 2) sequence of push/eval to build the term
694 * 3) when tstack_eval evaluates the BUILD_TERM command,
695 * stack->result.term is available.
696 *
697 * Same thing for types, but replace by BUILD_TYPE.
698 */
tstack_get_term(tstack_t * stack)699 static inline term_t tstack_get_term(tstack_t *stack) {
700 return stack->result.term;
701 }
702
tstack_get_type(tstack_t * stack)703 static inline term_t tstack_get_type(tstack_t *stack) {
704 return stack->result.type;
705 }
706
707
708
709 #endif /* __TERM_STACK2_H */
710