1 /* Boolector: Satisfiability Modulo Theories (SMT) solver.
2 *
3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4 *
5 * This file is part of Boolector.
6 * See COPYING for more information on using this software.
7 */
8
9 #include "btorsmt.h"
10 #include "btorbv.h"
11 #include "btoropt.h"
12 #include "utils/btorhashptr.h"
13 #include "utils/btormem.h"
14 #include "utils/btorstack.h"
15 #include "utils/btorutil.h"
16
17 #include <assert.h>
18 #include <ctype.h>
19 #include <stdarg.h>
20 #include <stdbool.h>
21 #include <stdlib.h>
22
23 BTOR_DECLARE_STACK (BoolectorNodePtr, BoolectorNode *);
24
25 /*------------------------------------------------------------------------*/
26
27 typedef struct BtorSMTParser BtorSMTParser;
28 typedef struct BtorSMTNode BtorSMTNode;
29 typedef struct BtorSMTNodes BtorSMTNodes;
30 typedef struct BtorSMTSymbol BtorSMTSymbol;
31
32 enum BtorSMTCharacterClass
33 {
34 BTOR_SMTCC_IDENTIFIER_START = 1,
35 BTOR_SMTCC_IDENTIFIER_MIDDLE = 2,
36 BTOR_SMTCC_ARITHMETIC_OPERATOR = 4,
37 BTOR_SMTCC_NUMERAL_START = 8,
38 BTOR_SMTCC_DIGIT = 16,
39 BTOR_SMTCC_SPACE = 32,
40 BTOR_SMTCC_IDENTIFIER_PREFIX = 64,
41 };
42
43 enum BtorSMTToken
44 {
45 BTOR_SMTOK_ERR = 0,
46 BTOR_SMTOK_EOF = EOF,
47
48 BTOR_SMTOK_IDENTIFIER = 'a',
49 BTOR_SMTOK_NUMERAL = '0',
50 BTOR_SMTOK_RATIONAL = '.',
51 BTOR_SMTOK_USERVAL = '{',
52 BTOR_SMTOK_LP = '(',
53 BTOR_SMTOK_RP = ')',
54 BTOR_SMTOK_STRING = '"',
55 BTOR_SMTOK_VAR = '?',
56 BTOR_SMTOK_FVAR = '$',
57 BTOR_SMTOK_ATTR = ':',
58 BTOR_SMTOK_ARITH = '=',
59
60 BTOR_SMTOK_KEYWORD = 256, /* above ASCII codes */
61 BTOR_SMTOK_AND = 256,
62 BTOR_SMTOK_ASSUMPTION = 257,
63 BTOR_SMTOK_BENCHMARK = 258,
64 BTOR_SMTOK_DISTINCT = 259,
65 BTOR_SMTOK_EXTRAFUNS = 260,
66 BTOR_SMTOK_EXTRAPREDS = 261,
67 BTOR_SMTOK_EXTRASORTS = 262,
68 BTOR_SMTOK_FALSE = 263,
69 BTOR_SMTOK_FLET = 264,
70 BTOR_SMTOK_FORMULA = 265,
71 BTOR_SMTOK_IFF = 266,
72 BTOR_SMTOK_IF_THEN_ELSE = 267,
73 BTOR_SMTOK_IMPLIES = 268,
74 BTOR_SMTOK_ITE = 269,
75 BTOR_SMTOK_LET = 270,
76 BTOR_SMTOK_LOGICATTR = 271,
77 BTOR_SMTOK_NOT = 272,
78 BTOR_SMTOK_NOTES = 273,
79 BTOR_SMTOK_OR = 274,
80 BTOR_SMTOK_SAT = 275,
81 BTOR_SMTOK_STATUS = 276,
82 BTOR_SMTOK_TRUE = 277,
83 BTOR_SMTOK_UNKNOWN = 278,
84 BTOR_SMTOK_UNSAT = 279,
85 BTOR_SMTOK_XOR = 280,
86
87 BTOR_SMTOK_CONCAT = 281, /* QF_BV specific symbols */
88 BTOR_SMTOK_EQ = 282,
89 BTOR_SMTOK_EXTRACT = 283,
90 BTOR_SMTOK_BIT0 = 284,
91 BTOR_SMTOK_BIT1 = 285,
92 BTOR_SMTOK_BVADD = 286,
93 BTOR_SMTOK_BVNOT = 287,
94 BTOR_SMTOK_BVMUL = 288,
95 BTOR_SMTOK_BVULE = 289,
96 BTOR_SMTOK_BVAND = 290,
97 BTOR_SMTOK_BVLSHR = 291,
98 BTOR_SMTOK_BVSLT = 292,
99 BTOR_SMTOK_BVULT = 293,
100 BTOR_SMTOK_BVNEG = 294,
101 BTOR_SMTOK_BVSLE = 295,
102 BTOR_SMTOK_BVSHL = 296,
103 BTOR_SMTOK_BVSUB = 297,
104 BTOR_SMTOK_BVSDIV = 298,
105 BTOR_SMTOK_BVASHR = 299,
106 BTOR_SMTOK_BVOR = 300,
107 BTOR_SMTOK_BVUDIV = 301,
108 BTOR_SMTOK_BVUREM = 302,
109 BTOR_SMTOK_BVNAND = 303,
110 BTOR_SMTOK_BVNOR = 304,
111 BTOR_SMTOK_BVUGT = 305,
112 BTOR_SMTOK_BVUGE = 306,
113 BTOR_SMTOK_BVSGT = 307,
114 BTOR_SMTOK_BVSGE = 308,
115 BTOR_SMTOK_BVCOMP = 309,
116
117 BTOR_SMTOK_REPEAT = 310,
118 BTOR_SMTOK_ZERO_EXTEND = 311,
119 BTOR_SMTOK_SIGN_EXTEND = 312,
120 BTOR_SMTOK_ROTATE_LEFT = 313,
121 BTOR_SMTOK_ROTATE_RIGHT = 314,
122
123 BTOR_SMTOK_BVXOR = 315,
124 BTOR_SMTOK_BVSREM = 316,
125 BTOR_SMTOK_BVSMOD = 317,
126 BTOR_SMTOK_BVXNOR = 318,
127
128 BTOR_SMTOK_SELECT = 319,
129 BTOR_SMTOK_STORE = 320,
130
131 BTOR_SMTOK_UNSUPPORTED_KEYWORD = 512,
132 BTOR_SMTOK_AXIOMS = 512,
133 BTOR_SMTOK_DEFINITIONS = 513,
134 BTOR_SMTOK_EXISTS = 514,
135 BTOR_SMTOK_EXTENSIONS = 515,
136 BTOR_SMTOK_FORALL = 516,
137 BTOR_SMTOK_FUNS = 517,
138 BTOR_SMTOK_LANGUAGE = 518,
139 BTOR_SMTOK_LOGIC = 519,
140 BTOR_SMTOK_PREDS = 520,
141 BTOR_SMTOK_SORTS = 521,
142 BTOR_SMTOK_THEORY = 522,
143 BTOR_SMTOK_THEORYATTR = 523,
144
145 BTOR_SMTOK_INTERNAL = 1024,
146 BTOR_SMTOK_BIND = 1024,
147 BTOR_SMTOK_TRANSLATED = 1025, // TODO ...
148 };
149
150 typedef enum BtorSMTToken BtorSMTToken;
151
152 struct BtorSMTNode
153 {
154 void *head;
155 void *tail;
156 BoolectorNode *exp; // TODO overlay with tail/head?
157 };
158
159 BTOR_DECLARE_STACK (BtorSMTNodePtr, BtorSMTNode *);
160
161 struct BtorSMTSymbol
162 {
163 char *name;
164 BtorSMTToken token;
165 BtorSMTSymbol *next;
166 BtorSMTNode *last;
167 BoolectorNode *exp;
168 };
169
170 struct BtorSMTParser
171 {
172 BtorMemMgr *mem;
173 Btor *btor;
174 bool parsed;
175
176 uint32_t verbosity;
177 uint32_t modelgen;
178 uint32_t incremental;
179 BtorOptIncrementalSMT1 incremental_smt1;
180
181 struct
182 {
183 uint32_t nparsed, handled;
184 } assumptions;
185 struct
186 {
187 uint32_t nparsed, handled, nchecked;
188 } formulas;
189
190 uint32_t nprefix;
191 BtorCharStack *prefix;
192 FILE *infile;
193 const char *infile_name;
194 FILE *outfile;
195 uint32_t lineno;
196 bool saved;
197 int32_t saved_char;
198
199 uint_least64_t bytes;
200
201 BtorLogic required_logic;
202
203 char *error;
204 BtorCharStack buffer;
205
206 unsigned char types[256];
207
208 BtorSMTSymbol *symbol;
209 BtorSMTSymbol **symtab;
210 uint32_t szsymtab;
211 uint32_t symbols;
212
213 uint32_t constants;
214
215 BtorSMTNode *bind;
216 BtorSMTNode *translated;
217
218 BtorPtrHashTable *nodes;
219 BtorSMTNodePtrStack stack;
220 BtorSMTNodePtrStack work;
221 BtorSMTNodePtrStack delete;
222 BtorIntStack heads;
223 };
224
225 /*------------------------------------------------------------------------*/
226
227 static uint32_t btor_smt_primes[] = {1001311, 2517041, 3543763, 4026227};
228 #define BTOR_SMT_PRIMES ((sizeof btor_smt_primes) / sizeof *btor_smt_primes)
229
230 static void *
car(BtorSMTNode * node)231 car (BtorSMTNode *node)
232 {
233 assert (node);
234 return node->head;
235 }
236
237 static void *
cdr(BtorSMTNode * node)238 cdr (BtorSMTNode *node)
239 {
240 assert (node);
241 return node->tail;
242 }
243
244 #define isleaf(l) ((uintptr_t) 1 & (uintptr_t) (l))
245 #define leaf(l) ((void *) ((uintptr_t) 1 | (uintptr_t) (l)))
246 #define strip(l) ((BtorSMTSymbol *) ((~(uintptr_t) 1) & (uintptr_t) (l)))
247
248 static BtorSMTNode *
cons(BtorSMTParser * parser,void * h,void * t)249 cons (BtorSMTParser *parser, void *h, void *t)
250 {
251 BtorSMTNode *res;
252
253 BTOR_NEW (parser->mem, res);
254 BTOR_CLR (res);
255
256 btor_hashptr_table_add (parser->nodes, res);
257 assert (parser->nodes->count > 0);
258
259 res->head = h;
260 res->tail = t;
261
262 return res;
263 }
264
265 static uint32_t
hash_name(const char * name)266 hash_name (const char *name)
267 {
268 uint32_t i, res;
269 const char *p;
270 char ch;
271
272 i = 0;
273 res = 0;
274
275 for (p = name; (ch = *p); p++)
276 {
277 res += btor_smt_primes[i++] * (uint32_t) ch;
278
279 if (i == BTOR_SMT_PRIMES) i = 0;
280
281 res = (res << 4) | (res >> 28);
282 }
283
284 return res;
285 }
286
287 static BtorSMTSymbol **
find_symbol_position(BtorSMTParser * parser,const char * name)288 find_symbol_position (BtorSMTParser *parser, const char *name)
289 {
290 uint32_t h = hash_name (name) & (parser->szsymtab - 1);
291 BtorSMTSymbol **p, *s;
292
293 for (p = parser->symtab + h; (s = *p) && strcmp (name, s->name); p = &s->next)
294 ;
295
296 return p;
297 }
298
299 static void
delete_symbol(BtorSMTParser * parser,BtorSMTSymbol * symbol)300 delete_symbol (BtorSMTParser *parser, BtorSMTSymbol *symbol)
301 {
302 BoolectorNode *exp;
303
304 assert (parser->symbols > 0);
305 parser->symbols--;
306
307 btor_mem_freestr (parser->mem, symbol->name);
308
309 if ((exp = symbol->exp)) boolector_release (parser->btor, exp);
310
311 BTOR_DELETE (parser->mem, symbol);
312 }
313
314 static void
remove_and_delete_symbol(BtorSMTParser * parser,BtorSMTSymbol * symbol)315 remove_and_delete_symbol (BtorSMTParser *parser, BtorSMTSymbol *symbol)
316 {
317 BtorSMTSymbol **p;
318
319 p = find_symbol_position (parser, symbol->name);
320 assert (*p == symbol);
321
322 *p = symbol->next;
323 delete_symbol (parser, symbol);
324 }
325
326 static void
delete_smt_node(BtorSMTParser * parser,BtorSMTNode * node)327 delete_smt_node (BtorSMTParser *parser, BtorSMTNode *node)
328 {
329 BtorSMTSymbol *s;
330
331 if (!node) return;
332
333 assert (parser->nodes->count > 0);
334 assert (btor_hashptr_table_get (parser->nodes, node));
335 btor_hashptr_table_remove (parser->nodes, node, 0, 0);
336
337 if (node->exp) boolector_release (parser->btor, node->exp);
338
339 if (!parser->modelgen && isleaf (car (node)))
340 {
341 s = strip (car (node));
342 if (s->last == node) remove_and_delete_symbol (parser, s);
343 }
344
345 BTOR_DELETE (parser->mem, node);
346 }
347
348 static void
smt_message(BtorSMTParser * parser,uint32_t level,const char * fmt,...)349 smt_message (BtorSMTParser *parser, uint32_t level, const char *fmt, ...)
350 {
351 va_list ap;
352
353 if (parser->verbosity < level) return;
354
355 fflush (stdout);
356 fprintf (stdout, "[btorsmt] ");
357 if (parser->incremental) printf ("%d : ", parser->formulas.nchecked);
358 va_start (ap, fmt);
359 vfprintf (stdout, fmt, ap);
360 va_end (ap);
361 fprintf (stdout, " after %.2f seconds\n", btor_util_time_stamp ());
362 fflush (stdout);
363 }
364
365 static void
recursively_delete_smt_node(BtorSMTParser * parser,BtorSMTNode * root)366 recursively_delete_smt_node (BtorSMTParser *parser, BtorSMTNode *root)
367 {
368 BtorSMTNode *node;
369
370 assert (BTOR_EMPTY_STACK (parser->delete));
371
372 BTOR_PUSH_STACK (parser->delete, root);
373 while (!BTOR_EMPTY_STACK (parser->delete))
374 {
375 node = BTOR_POP_STACK (parser->delete);
376
377 if (!node) continue;
378
379 if (isleaf (node)) continue;
380
381 if (car (node) == parser->bind)
382 {
383 /* NOTE: assignment == cdr (node) shared, so do not delete here */
384 assert (cdr (node));
385 }
386 else
387 {
388 BTOR_PUSH_STACK (parser->delete, cdr (node));
389 BTOR_PUSH_STACK (parser->delete, car (node));
390 }
391
392 delete_smt_node (parser, node);
393 }
394 }
395
396 static uint32_t
length(BtorSMTNode * node)397 length (BtorSMTNode *node)
398 {
399 BtorSMTNode *p;
400 uint32_t res;
401
402 assert (!isleaf (node));
403
404 res = 0;
405 for (p = node; p; p = cdr (p)) res++;
406
407 return res;
408 }
409
410 static bool
is_list_of_length(BtorSMTNode * node,uint32_t l)411 is_list_of_length (BtorSMTNode *node, uint32_t l)
412 {
413 if (isleaf (node)) return false;
414
415 return length (node) == l;
416 }
417
418 static void
release_smt_symbols(BtorSMTParser * parser)419 release_smt_symbols (BtorSMTParser *parser)
420 {
421 BtorSMTSymbol *p, *next;
422 uint32_t i;
423
424 for (i = 0; i < parser->szsymtab; i++)
425 {
426 for (p = parser->symtab[i]; p; p = next)
427 {
428 next = p->next;
429 delete_symbol (parser, p);
430 }
431 }
432 BTOR_DELETEN (parser->mem, parser->symtab, parser->szsymtab);
433 parser->symtab = 0;
434 parser->szsymtab = 0;
435 }
436
437 static void
release_smt_nodes(BtorSMTParser * parser)438 release_smt_nodes (BtorSMTParser *parser)
439 {
440 while (parser->nodes && parser->nodes->count)
441 recursively_delete_smt_node (parser, parser->nodes->first->key);
442 }
443
444 static void
release_smt_internals(BtorSMTParser * parser)445 release_smt_internals (BtorSMTParser *parser)
446 {
447 release_smt_nodes (parser);
448 release_smt_symbols (parser);
449
450 if (parser->nodes)
451 {
452 btor_hashptr_table_delete (parser->nodes);
453 parser->nodes = 0;
454 }
455 BTOR_RELEASE_STACK (parser->stack);
456 BTOR_RELEASE_STACK (parser->work);
457 BTOR_RELEASE_STACK (parser->delete);
458 BTOR_RELEASE_STACK (parser->heads);
459 BTOR_RELEASE_STACK (parser->buffer);
460 }
461
462 static void
delete_smt_parser(BtorSMTParser * parser)463 delete_smt_parser (BtorSMTParser *parser)
464 {
465 BtorMemMgr *mm;
466
467 mm = parser->mem;
468
469 release_smt_internals (parser);
470
471 btor_mem_freestr (mm, parser->error);
472
473 BTOR_DELETE (mm, parser);
474 btor_mem_mgr_delete (mm);
475 }
476
477 static char *
perr_smt(BtorSMTParser * parser,const char * fmt,...)478 perr_smt (BtorSMTParser *parser, const char *fmt, ...)
479 {
480 size_t bytes;
481 va_list ap;
482
483 if (!parser->error)
484 {
485 va_start (ap, fmt);
486 bytes = btor_mem_parse_error_msg_length (parser->infile_name, fmt, ap);
487 va_end (ap);
488
489 va_start (ap, fmt);
490 parser->error = btor_mem_parse_error_msg (
491 parser->mem, parser->infile_name, parser->lineno, -1, fmt, ap, bytes);
492 va_end (ap);
493 }
494
495 return parser->error;
496 }
497
498 static void
enlarge_symtab(BtorSMTParser * parser)499 enlarge_symtab (BtorSMTParser *parser)
500 {
501 BtorSMTSymbol *p, *next, **old_symtab, **new_symtab;
502 uint32_t h, i, old_size, new_size;
503
504 old_symtab = parser->symtab;
505 old_size = parser->szsymtab;
506
507 new_size = old_size ? 2 * old_size : 1;
508 BTOR_NEWN (parser->mem, new_symtab, new_size);
509 BTOR_CLRN (new_symtab, new_size);
510
511 for (i = 0; i < old_size; i++)
512 {
513 for (p = old_symtab[i]; p; p = next)
514 {
515 next = p->next;
516 h = hash_name (p->name) & (new_size - 1);
517 p->next = new_symtab[h];
518 new_symtab[h] = p;
519 }
520 }
521
522 BTOR_DELETEN (parser->mem, old_symtab, old_size);
523
524 parser->symtab = new_symtab;
525 parser->szsymtab = new_size;
526 }
527
528 static BtorSMTSymbol *
insert_symbol(BtorSMTParser * parser,const char * name)529 insert_symbol (BtorSMTParser *parser, const char *name)
530 {
531 BtorSMTSymbol **p, *res;
532
533 if (parser->szsymtab == parser->symbols) enlarge_symtab (parser);
534
535 p = find_symbol_position (parser, name);
536 if (!(res = *p))
537 {
538 BTOR_NEW (parser->mem, res);
539 BTOR_CLR (res);
540
541 res->token = BTOR_SMTOK_IDENTIFIER;
542 res->name = btor_mem_strdup (parser->mem, name);
543
544 parser->symbols++;
545 *p = res;
546 }
547
548 return res;
549 }
550
551 static BtorSMTParser *
new_smt_parser(Btor * btor)552 new_smt_parser (Btor *btor)
553 {
554 BtorSMTSymbol *bind, *translated;
555 BtorMemMgr *mem;
556 BtorSMTParser *res;
557 unsigned char type;
558 int32_t ch;
559
560 mem = btor_mem_mgr_new ();
561 BTOR_NEW (mem, res);
562 BTOR_CLR (res);
563
564 res->verbosity = boolector_get_opt (btor, BTOR_OPT_VERBOSITY);
565 res->modelgen = boolector_get_opt (btor, BTOR_OPT_MODEL_GEN);
566 res->incremental = boolector_get_opt (btor, BTOR_OPT_INCREMENTAL);
567 res->incremental_smt1 = boolector_get_opt (btor, BTOR_OPT_INCREMENTAL_SMT1);
568
569 smt_message (res, 2, "initializing SMT parser");
570 if (res->incremental)
571 {
572 smt_message (res, 2, "incremental checking of SMT benchmark");
573 if (res->incremental_smt1 == BTOR_INCREMENTAL_SMT1_BASIC)
574 smt_message (res, 2, "stop after first satisfiable ':formula'");
575 else if (res->incremental_smt1 == BTOR_INCREMENTAL_SMT1_CONTINUE)
576 smt_message (res, 2, "check all ':formula' for satisfiability");
577 }
578
579 res->mem = mem;
580 res->btor = btor;
581
582 res->nodes = btor_hashptr_table_new (mem, 0, 0);
583 BTOR_INIT_STACK (mem, res->stack);
584 BTOR_INIT_STACK (mem, res->work);
585 BTOR_INIT_STACK (mem, res->delete);
586 BTOR_INIT_STACK (mem, res->heads);
587 BTOR_INIT_STACK (mem, res->buffer);
588
589 res->required_logic = BTOR_LOGIC_QF_BV;
590
591 type = BTOR_SMTCC_IDENTIFIER_START | BTOR_SMTCC_IDENTIFIER_MIDDLE;
592
593 for (ch = 'a'; ch <= 'z'; ch++) res->types[ch] |= type;
594 for (ch = 'A'; ch <= 'Z'; ch++) res->types[ch] |= type;
595
596 res->types['_'] |= type;
597 res->types['.'] |= BTOR_SMTCC_IDENTIFIER_MIDDLE;
598 res->types['\''] |= BTOR_SMTCC_IDENTIFIER_MIDDLE;
599
600 type = BTOR_SMTCC_IDENTIFIER_MIDDLE;
601 type |= BTOR_SMTCC_DIGIT;
602
603 res->types['0'] |= type;
604
605 type |= BTOR_SMTCC_NUMERAL_START;
606 for (ch = '1'; ch <= '9'; ch++) res->types[ch] |= type;
607
608 res->types['='] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
609 res->types['<'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
610 res->types['>'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
611 res->types['&'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
612 res->types['@'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
613 res->types['#'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
614 res->types['+'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
615 res->types['-'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
616 res->types['*'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
617 res->types['/'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
618 res->types['%'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
619 res->types['|'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
620 res->types['~'] |= BTOR_SMTCC_ARITHMETIC_OPERATOR;
621
622 res->types[' '] |= BTOR_SMTCC_SPACE;
623 res->types['\t'] |= BTOR_SMTCC_SPACE;
624 res->types['\n'] |= BTOR_SMTCC_SPACE;
625 res->types[0xd] |= BTOR_SMTCC_SPACE;
626
627 res->types[':'] |= BTOR_SMTCC_IDENTIFIER_PREFIX;
628 res->types['?'] |= BTOR_SMTCC_IDENTIFIER_PREFIX;
629 res->types['$'] |= BTOR_SMTCC_IDENTIFIER_PREFIX;
630
631 insert_symbol (res, "and")->token = BTOR_SMTOK_AND;
632 insert_symbol (res, ":assumption")->token = BTOR_SMTOK_ASSUMPTION;
633 insert_symbol (res, ":axioms")->token = BTOR_SMTOK_AXIOMS;
634 insert_symbol (res, "benchmark")->token = BTOR_SMTOK_BENCHMARK;
635 insert_symbol (res, ":definitions")->token = BTOR_SMTOK_DEFINITIONS;
636 insert_symbol (res, "distinct")->token = BTOR_SMTOK_DISTINCT;
637 insert_symbol (res, "exists")->token = BTOR_SMTOK_EXISTS;
638 insert_symbol (res, ":extensions")->token = BTOR_SMTOK_EXTENSIONS;
639 insert_symbol (res, ":extrafuns")->token = BTOR_SMTOK_EXTRAFUNS;
640 insert_symbol (res, ":extrapreds")->token = BTOR_SMTOK_EXTRAPREDS;
641 insert_symbol (res, ":extrasorts")->token = BTOR_SMTOK_EXTRASORTS;
642 insert_symbol (res, "false")->token = BTOR_SMTOK_FALSE;
643 insert_symbol (res, "flet")->token = BTOR_SMTOK_FLET;
644 insert_symbol (res, "forall")->token = BTOR_SMTOK_FORALL;
645 insert_symbol (res, ":formula")->token = BTOR_SMTOK_FORMULA;
646 insert_symbol (res, ":funs")->token = BTOR_SMTOK_FUNS;
647 insert_symbol (res, "iff")->token = BTOR_SMTOK_IFF;
648 insert_symbol (res, "if_then_else")->token = BTOR_SMTOK_IF_THEN_ELSE;
649 insert_symbol (res, "implies")->token = BTOR_SMTOK_IMPLIES;
650 insert_symbol (res, "ite")->token = BTOR_SMTOK_ITE;
651 insert_symbol (res, ":language")->token = BTOR_SMTOK_LANGUAGE;
652 insert_symbol (res, "let")->token = BTOR_SMTOK_LET;
653 insert_symbol (res, "logic")->token = BTOR_SMTOK_LOGIC;
654 insert_symbol (res, ":logic")->token = BTOR_SMTOK_LOGICATTR;
655 insert_symbol (res, ":notes")->token = BTOR_SMTOK_NOTES;
656 insert_symbol (res, "not")->token = BTOR_SMTOK_NOT;
657 insert_symbol (res, "or")->token = BTOR_SMTOK_OR;
658 insert_symbol (res, ":preds")->token = BTOR_SMTOK_PREDS;
659 insert_symbol (res, "sat")->token = BTOR_SMTOK_SAT;
660 insert_symbol (res, ":sorts")->token = BTOR_SMTOK_SORTS;
661 insert_symbol (res, ":status")->token = BTOR_SMTOK_STATUS;
662 insert_symbol (res, "theory")->token = BTOR_SMTOK_THEORY;
663 insert_symbol (res, ":theory")->token = BTOR_SMTOK_THEORYATTR;
664 insert_symbol (res, "true")->token = BTOR_SMTOK_TRUE;
665 insert_symbol (res, "unknown")->token = BTOR_SMTOK_UNKNOWN;
666 insert_symbol (res, "unsat")->token = BTOR_SMTOK_UNSAT;
667 insert_symbol (res, "xor")->token = BTOR_SMTOK_XOR;
668
669 bind = insert_symbol (res, "<internal bind symbol>");
670 bind->token = BTOR_SMTOK_BIND;
671 res->bind = leaf (bind);
672
673 translated = insert_symbol (res, "<internal translated symbol>");
674 translated->token = BTOR_SMTOK_TRANSLATED;
675 res->translated = leaf (translated);
676
677 insert_symbol (res, "=")->token = BTOR_SMTOK_EQ;
678 insert_symbol (res, "concat")->token = BTOR_SMTOK_CONCAT;
679 insert_symbol (res, "bit0")->token = BTOR_SMTOK_BIT0;
680 insert_symbol (res, "bit1")->token = BTOR_SMTOK_BIT1;
681 insert_symbol (res, "bvadd")->token = BTOR_SMTOK_BVADD;
682 insert_symbol (res, "bvnot")->token = BTOR_SMTOK_BVNOT;
683 insert_symbol (res, "bvmul")->token = BTOR_SMTOK_BVMUL;
684 insert_symbol (res, "bvule")->token = BTOR_SMTOK_BVULE;
685 insert_symbol (res, "bvand")->token = BTOR_SMTOK_BVAND;
686 insert_symbol (res, "bvlshr")->token = BTOR_SMTOK_BVLSHR;
687 insert_symbol (res, "bvslt")->token = BTOR_SMTOK_BVSLT;
688 insert_symbol (res, "bvult")->token = BTOR_SMTOK_BVULT;
689 insert_symbol (res, "bvneg")->token = BTOR_SMTOK_BVNEG;
690 insert_symbol (res, "bvsle")->token = BTOR_SMTOK_BVSLE;
691 insert_symbol (res, "bvshl")->token = BTOR_SMTOK_BVSHL;
692 insert_symbol (res, "bvsub")->token = BTOR_SMTOK_BVSUB;
693 insert_symbol (res, "bvsdiv")->token = BTOR_SMTOK_BVSDIV;
694 insert_symbol (res, "bvashr")->token = BTOR_SMTOK_BVASHR;
695 insert_symbol (res, "bvor")->token = BTOR_SMTOK_BVOR;
696 insert_symbol (res, "bvudiv")->token = BTOR_SMTOK_BVUDIV;
697 insert_symbol (res, "bvurem")->token = BTOR_SMTOK_BVUREM;
698 insert_symbol (res, "bvnor")->token = BTOR_SMTOK_BVNOR;
699 insert_symbol (res, "bvnand")->token = BTOR_SMTOK_BVNAND;
700 insert_symbol (res, "bvugt")->token = BTOR_SMTOK_BVUGT;
701 insert_symbol (res, "bvuge")->token = BTOR_SMTOK_BVUGE;
702 insert_symbol (res, "bvsgt")->token = BTOR_SMTOK_BVSGT;
703 insert_symbol (res, "bvsge")->token = BTOR_SMTOK_BVSGE;
704 insert_symbol (res, "bvcomp")->token = BTOR_SMTOK_BVCOMP;
705 insert_symbol (res, "bvxor")->token = BTOR_SMTOK_BVXOR;
706 insert_symbol (res, "bvsrem")->token = BTOR_SMTOK_BVSREM;
707 insert_symbol (res, "bvsmod")->token = BTOR_SMTOK_BVSMOD;
708 insert_symbol (res, "bvxnor")->token = BTOR_SMTOK_BVXNOR;
709 insert_symbol (res, "select")->token = BTOR_SMTOK_SELECT;
710 insert_symbol (res, "store")->token = BTOR_SMTOK_STORE;
711
712 return res;
713 }
714
715 static int32_t
nextch_smt(BtorSMTParser * parser)716 nextch_smt (BtorSMTParser *parser)
717 {
718 int32_t res;
719
720 if (parser->saved)
721 {
722 res = parser->saved_char;
723 parser->saved = false;
724 }
725 else if (parser->prefix
726 && parser->nprefix < BTOR_COUNT_STACK (*parser->prefix))
727 {
728 parser->bytes++;
729 res = parser->prefix->start[parser->nprefix++];
730 }
731 else
732 {
733 parser->bytes++;
734 res = getc (parser->infile);
735 }
736
737 if (res == '\n') parser->lineno++;
738
739 return res;
740 }
741
742 static void
savech_smt(BtorSMTParser * parser,int32_t ch)743 savech_smt (BtorSMTParser *parser, int32_t ch)
744 {
745 assert (!parser->saved);
746
747 parser->saved_char = ch;
748 parser->saved = true;
749
750 if (ch == '\n')
751 {
752 assert (parser->lineno > 1);
753 parser->lineno--;
754 }
755 }
756
757 static unsigned char
int2type(BtorSMTParser * parser,int32_t ch)758 int2type (BtorSMTParser *parser, int32_t ch)
759 {
760 if (0 > ch || ch >= 256) return 0;
761 return parser->types[ch];
762 }
763
764 static bool
has_prefix(const char * str,const char * prefix)765 has_prefix (const char *str, const char *prefix)
766 {
767 const char *p, *q;
768
769 for (p = str, q = prefix; *q && *p == *q; p++, q++)
770 ;
771 return *q == 0;
772 }
773
774 static BtorSMTToken
nextok(BtorSMTParser * parser)775 nextok (BtorSMTParser *parser)
776 {
777 unsigned char type;
778 BtorSMTToken res;
779 int32_t ch;
780 uint32_t count;
781
782 parser->symbol = 0;
783 BTOR_RESET_STACK (parser->buffer);
784
785 SKIP_WHITE_SPACE:
786
787 ch = nextch_smt (parser);
788 if (ch == EOF) return EOF;
789
790 type = int2type (parser, ch);
791 if (type & BTOR_SMTCC_SPACE) goto SKIP_WHITE_SPACE;
792
793 if (type & BTOR_SMTCC_IDENTIFIER_START)
794 {
795 BTOR_PUSH_STACK (parser->buffer, ch);
796
797 while (int2type (parser, (ch = nextch_smt (parser)))
798 & BTOR_SMTCC_IDENTIFIER_MIDDLE)
799 BTOR_PUSH_STACK (parser->buffer, ch);
800
801 count = 0;
802
803 if (ch == '[')
804 {
805 BTOR_PUSH_STACK (parser->buffer, ch);
806
807 ch = nextch_smt (parser);
808
809 for (;;)
810 {
811 if (int2type (parser, ch) & BTOR_SMTCC_NUMERAL_START)
812 {
813 BTOR_PUSH_STACK (parser->buffer, ch);
814
815 while (int2type (parser, (ch = nextch_smt (parser)))
816 & BTOR_SMTCC_DIGIT)
817 BTOR_PUSH_STACK (parser->buffer, ch);
818
819 COUNT_AND_CONTINUE_WITH_NEXT_INDEX:
820
821 count++;
822
823 if (ch == ']') break;
824
825 if (ch != ':') goto UNEXPECTED_CHARACTER;
826
827 BTOR_PUSH_STACK (parser->buffer, ':');
828 ch = nextch_smt (parser);
829 }
830 else if (ch == '0')
831 {
832 BTOR_PUSH_STACK (parser->buffer, ch);
833 ch = nextch_smt (parser);
834 goto COUNT_AND_CONTINUE_WITH_NEXT_INDEX;
835 }
836 else
837 goto UNEXPECTED_CHARACTER;
838 }
839
840 if (!count) return !perr_smt (parser, "empty index list");
841
842 assert (ch == ']');
843 BTOR_PUSH_STACK (parser->buffer, ch);
844 }
845 else
846 {
847 if (!ch) goto UNEXPECTED_CHARACTER;
848
849 savech_smt (parser, ch);
850 }
851
852 BTOR_PUSH_STACK (parser->buffer, 0);
853
854 parser->symbol = insert_symbol (parser, parser->buffer.start);
855
856 if (count == 2 && has_prefix (parser->symbol->name, "extract["))
857 parser->symbol->token = BTOR_SMTOK_EXTRACT;
858
859 if (count == 1)
860 {
861 if (has_prefix (parser->symbol->name, "repeat["))
862 parser->symbol->token = BTOR_SMTOK_REPEAT;
863
864 if (has_prefix (parser->symbol->name, "zero_extend["))
865 parser->symbol->token = BTOR_SMTOK_ZERO_EXTEND;
866
867 if (has_prefix (parser->symbol->name, "sign_extend["))
868 parser->symbol->token = BTOR_SMTOK_SIGN_EXTEND;
869
870 if (has_prefix (parser->symbol->name, "rotate_left["))
871 parser->symbol->token = BTOR_SMTOK_ROTATE_LEFT;
872
873 if (has_prefix (parser->symbol->name, "rotate_right["))
874 parser->symbol->token = BTOR_SMTOK_ROTATE_RIGHT;
875 }
876
877 CHECK_FOR_UNSUPPORTED_KEYWORD:
878
879 if (parser->symbol->token >= BTOR_SMTOK_UNSUPPORTED_KEYWORD)
880 return !perr_smt (
881 parser, "unsupported keyword '%s'", parser->buffer.start);
882
883 return parser->symbol->token;
884 }
885
886 if (ch == '(') return BTOR_SMTOK_LP;
887
888 if (ch == ')') return BTOR_SMTOK_RP;
889
890 if (type & BTOR_SMTCC_IDENTIFIER_PREFIX)
891 {
892 res = ch;
893
894 assert (ch == '?' || ch == '$' || ch == ':');
895
896 assert ((ch == '?') == (res == BTOR_SMTOK_VAR));
897 assert ((ch == '$') == (res == BTOR_SMTOK_FVAR));
898 assert ((ch == ':') == (res == BTOR_SMTOK_ATTR));
899
900 BTOR_PUSH_STACK (parser->buffer, ch);
901
902 ch = nextch_smt (parser);
903 if (!(int2type (parser, ch) & BTOR_SMTCC_IDENTIFIER_START))
904 return !perr_smt (parser, "expected identifier after '%c'", res);
905
906 BTOR_PUSH_STACK (parser->buffer, ch);
907
908 while (int2type (parser, (ch = nextch_smt (parser)))
909 & BTOR_SMTCC_IDENTIFIER_MIDDLE)
910 BTOR_PUSH_STACK (parser->buffer, ch);
911
912 if (!ch) goto UNEXPECTED_CHARACTER;
913
914 savech_smt (parser, ch);
915 BTOR_PUSH_STACK (parser->buffer, 0);
916
917 parser->symbol = insert_symbol (parser, parser->buffer.start);
918
919 if (res == BTOR_SMTOK_VAR || res == BTOR_SMTOK_FVAR)
920 parser->symbol->token = res;
921
922 goto CHECK_FOR_UNSUPPORTED_KEYWORD;
923 }
924
925 if (type & BTOR_SMTCC_NUMERAL_START)
926 {
927 BTOR_PUSH_STACK (parser->buffer, ch);
928
929 while (int2type (parser, (ch = nextch_smt (parser))) & BTOR_SMTCC_DIGIT)
930 BTOR_PUSH_STACK (parser->buffer, ch);
931
932 CHECK_FOR_FRACTIONAL_PART:
933
934 if (ch == '.')
935 {
936 res = BTOR_SMTOK_RATIONAL;
937
938 BTOR_PUSH_STACK (parser->buffer, ch);
939 ch = nextch_smt (parser);
940
941 if (int2type (parser, ch) & BTOR_SMTCC_NUMERAL_START)
942 {
943 BTOR_PUSH_STACK (parser->buffer, ch);
944
945 while (int2type (parser, (ch = nextch_smt (parser)))
946 & BTOR_SMTCC_NUMERAL_START)
947 BTOR_PUSH_STACK (parser->buffer, ch);
948 }
949 else if (ch == '0')
950 {
951 BTOR_PUSH_STACK (parser->buffer, ch);
952
953 ch = nextch_smt (parser);
954 if (int2type (parser, ch) & BTOR_SMTCC_DIGIT)
955 goto UNEXPECTED_DIGIT_AFTER_ZERO;
956 }
957 else
958 goto UNEXPECTED_CHARACTER;
959 }
960 else
961 res = BTOR_SMTOK_NUMERAL;
962
963 if (!ch) goto UNEXPECTED_CHARACTER;
964
965 savech_smt (parser, ch);
966 BTOR_PUSH_STACK (parser->buffer, 0);
967
968 parser->symbol = insert_symbol (parser, parser->buffer.start);
969 parser->symbol->token = res;
970
971 return res;
972 }
973
974 if (ch == '0')
975 {
976 BTOR_PUSH_STACK (parser->buffer, ch);
977
978 ch = nextch_smt (parser);
979 if (int2type (parser, ch) & BTOR_SMTCC_DIGIT)
980 {
981 UNEXPECTED_DIGIT_AFTER_ZERO:
982 return !perr_smt (parser, "unexpected digit after '0'");
983 }
984
985 goto CHECK_FOR_FRACTIONAL_PART;
986 }
987
988 if (type & BTOR_SMTCC_ARITHMETIC_OPERATOR)
989 {
990 BTOR_PUSH_STACK (parser->buffer, ch);
991
992 while (int2type (parser, (ch = nextch_smt (parser)))
993 & BTOR_SMTCC_ARITHMETIC_OPERATOR)
994 BTOR_PUSH_STACK (parser->buffer, ch);
995
996 if (!ch) goto UNEXPECTED_CHARACTER;
997
998 BTOR_PUSH_STACK (parser->buffer, 0);
999
1000 parser->symbol = insert_symbol (parser, parser->buffer.start);
1001 if (parser->symbol->token == BTOR_SMTOK_IDENTIFIER)
1002 parser->symbol->token = BTOR_SMTOK_ARITH;
1003
1004 return parser->symbol->token;
1005 }
1006
1007 if (ch == ';')
1008 {
1009 while ((ch = nextch_smt (parser)) != '\n')
1010 if (ch == EOF) return BTOR_SMTOK_EOF;
1011
1012 goto SKIP_WHITE_SPACE;
1013 }
1014
1015 if (ch == '{')
1016 {
1017 BTOR_PUSH_STACK (parser->buffer, ch);
1018
1019 while ((ch = nextch_smt (parser)) != '}')
1020 {
1021 if (ch == '{') return !perr_smt (parser, "unescaped '{' after '{'");
1022
1023 if (ch == '\\')
1024 {
1025 BTOR_PUSH_STACK (parser->buffer, ch);
1026 ch = nextch_smt (parser);
1027 }
1028
1029 if (ch == EOF) return !perr_smt (parser, "unexpected EOF after '{'");
1030
1031 BTOR_PUSH_STACK (parser->buffer, ch);
1032 }
1033
1034 assert (ch == '}');
1035 BTOR_PUSH_STACK (parser->buffer, ch);
1036 BTOR_PUSH_STACK (parser->buffer, 0);
1037
1038 parser->symbol = insert_symbol (parser, parser->buffer.start);
1039 parser->symbol->token = BTOR_SMTOK_USERVAL;
1040
1041 return BTOR_SMTOK_USERVAL;
1042 }
1043
1044 if (ch == '"')
1045 {
1046 while ((ch = nextch_smt (parser)) != '"')
1047 {
1048 if (ch == '\\')
1049 {
1050 BTOR_PUSH_STACK (parser->buffer, ch);
1051 ch = nextch_smt (parser);
1052 }
1053
1054 if (ch == EOF) return !perr_smt (parser, "unexpected EOF after '\"'");
1055
1056 BTOR_PUSH_STACK (parser->buffer, ch);
1057 }
1058
1059 BTOR_PUSH_STACK (parser->buffer, 0);
1060
1061 parser->symbol = insert_symbol (parser, parser->buffer.start);
1062 parser->symbol->token = BTOR_SMTOK_STRING;
1063
1064 return BTOR_SMTOK_STRING;
1065 }
1066
1067 UNEXPECTED_CHARACTER:
1068 if (isprint (ch)) return !perr_smt (parser, "unexpected character '%c'", ch);
1069
1070 return !perr_smt (parser, "unexpected character with ASCII code %d", ch);
1071 }
1072
1073 static const char *
next_numeral(const char * str)1074 next_numeral (const char *str)
1075 {
1076 const char *p = str;
1077 int32_t ch;
1078
1079 assert (str);
1080
1081 if (isdigit ((int32_t) *p++))
1082 {
1083 while (isdigit (ch = *p++))
1084 ;
1085
1086 if (ch == ':')
1087 {
1088 assert (isdigit ((int32_t) *p));
1089 return p;
1090 }
1091
1092 assert (ch == ']');
1093 }
1094 else
1095 {
1096 while ((ch = *p++))
1097 if (ch == '[')
1098 {
1099 assert (isdigit ((int32_t) *p));
1100 return p;
1101 }
1102 }
1103
1104 return 0;
1105 }
1106
1107 static int32_t
extrafun(BtorSMTParser * parser,BtorSMTNode * fdecl)1108 extrafun (BtorSMTParser *parser, BtorSMTNode *fdecl)
1109 {
1110 BtorSMTSymbol *symbol, *sortsymbol;
1111 BtorSMTNode *node, *sort;
1112 int32_t addrlen, datalen;
1113 const char *p;
1114 BoolectorSort s, is, es;
1115
1116 if (!fdecl || !cdr (fdecl) || isleaf (fdecl) || !isleaf (node = car (fdecl))
1117 || (symbol = strip (node))->token != BTOR_SMTOK_IDENTIFIER)
1118 return !perr_smt (parser, "invalid function declaration");
1119
1120 if (cdr (cdr (fdecl)))
1121 return !perr_smt (parser,
1122 "no support for function declaration "
1123 "with more than one argument");
1124
1125 sort = car (cdr (fdecl));
1126 if (!sort || !isleaf (sort)
1127 || (sortsymbol = strip (sort))->token != BTOR_SMTOK_IDENTIFIER)
1128 {
1129 INVALID_SORT:
1130 return !perr_smt (parser,
1131 "invalid or unsupported sort "
1132 "in function declaration");
1133 }
1134
1135 if (symbol->exp)
1136 return !perr_smt (parser, "multiple definitions for '%s'", symbol->name);
1137
1138 p = sortsymbol->name;
1139
1140 if (!strcmp (p, "Bool"))
1141 {
1142 s = boolector_bool_sort (parser->btor);
1143 symbol->exp = boolector_var (parser->btor, s, symbol->name);
1144 boolector_release_sort (parser->btor, s);
1145 }
1146 else if (has_prefix (p, "BitVec"))
1147 {
1148 if (!(p = next_numeral (p)) || next_numeral (p)) goto INVALID_SORT;
1149
1150 datalen = atoi (p); /* TODO Overflow? */
1151 if (!datalen) goto INVALID_SORT;
1152
1153 s = boolector_bitvec_sort (parser->btor, datalen);
1154 symbol->exp = boolector_var (parser->btor, s, symbol->name);
1155 boolector_release_sort (parser->btor, s);
1156 }
1157 else if (has_prefix (p, "Array"))
1158 {
1159 if (!(p = next_numeral (p))) goto INVALID_SORT;
1160
1161 addrlen = atoi (p); /* TODO Overflow? */
1162 if (!addrlen) goto INVALID_SORT;
1163
1164 if (!(p = next_numeral (p)) || next_numeral (p)) goto INVALID_SORT;
1165
1166 datalen = atoi (p); /* TODO Overflow? */
1167 if (!datalen) goto INVALID_SORT;
1168
1169 es = boolector_bitvec_sort (parser->btor, datalen);
1170 is = boolector_bitvec_sort (parser->btor, addrlen);
1171 s = boolector_array_sort (parser->btor, is, es);
1172 symbol->exp = boolector_array (parser->btor, s, symbol->name);
1173 boolector_release_sort (parser->btor, is);
1174 boolector_release_sort (parser->btor, es);
1175 boolector_release_sort (parser->btor, s);
1176
1177 if (parser->required_logic == BTOR_LOGIC_QF_BV)
1178 {
1179 smt_message (parser, 2, "requires QF_AUFBV");
1180 parser->required_logic = BTOR_LOGIC_QF_AUFBV;
1181 }
1182
1183 /* TODO what about 'symbol->name' back annotation? */
1184 }
1185 else
1186 goto INVALID_SORT;
1187
1188 return 1;
1189 }
1190
1191 static bool
extrafuns(BtorSMTParser * parser,BtorSMTNode * list)1192 extrafuns (BtorSMTParser *parser, BtorSMTNode *list)
1193 {
1194 BtorSMTNode *p;
1195
1196 if (!list || isleaf (list))
1197 return !perr_smt (parser,
1198 "expected non empty list as argument to ':extrafuns'");
1199
1200 for (p = list; p; p = cdr (p))
1201 if (!extrafun (parser, car (p))) return 0;
1202
1203 return parser->error == 0;
1204 }
1205
1206 static bool
extrapred(BtorSMTParser * parser,BtorSMTNode * pdecl)1207 extrapred (BtorSMTParser *parser, BtorSMTNode *pdecl)
1208 {
1209 BtorSMTSymbol *symbol;
1210 BtorSMTNode *node;
1211 BoolectorSort s;
1212
1213 if (!pdecl || isleaf (pdecl) || !isleaf (node = car (pdecl))
1214 || (symbol = strip (node))->token != BTOR_SMTOK_IDENTIFIER)
1215 return !perr_smt (parser, "invalid predicate declaration");
1216
1217 if (cdr (pdecl))
1218 return !perr_smt (parser,
1219 "no support for predicate declarations with arguments");
1220
1221 if (symbol->exp)
1222 return !perr_smt (parser, "multiple definitions for '%s'", symbol->name);
1223
1224 s = boolector_bool_sort (parser->btor);
1225 symbol->exp = boolector_var (parser->btor, s, symbol->name);
1226 boolector_release_sort (parser->btor, s);
1227
1228 return true;
1229 }
1230
1231 static bool
extrapreds(BtorSMTParser * parser,BtorSMTNode * list)1232 extrapreds (BtorSMTParser *parser, BtorSMTNode *list)
1233 {
1234 BtorSMTNode *p;
1235
1236 if (!list || isleaf (list))
1237 return !perr_smt (parser,
1238 "expected non empty list as argument to ':extrapreds'");
1239
1240 for (p = list; p; p = cdr (p))
1241 if (!extrapred (parser, car (p))) return false;
1242
1243 return !parser->error;
1244 }
1245
1246 static BtorSMTToken
node2token(BtorSMTNode * node)1247 node2token (BtorSMTNode *node)
1248 {
1249 return (node && isleaf (node)) ? strip (node)->token : BTOR_SMTOK_ERR;
1250 }
1251
1252 static bool
is_let_or_flet(BtorSMTNode * node)1253 is_let_or_flet (BtorSMTNode *node)
1254 {
1255 BtorSMTToken token = node2token (node);
1256 return token == BTOR_SMTOK_LET || token == BTOR_SMTOK_FLET;
1257 }
1258
1259 static BoolectorNode *
node2exp(BtorSMTParser * parser,BtorSMTNode * node)1260 node2exp (BtorSMTParser *parser, BtorSMTNode *node)
1261 {
1262 const char *p, *start, *end;
1263 char *tmp, *ext, ch;
1264 BtorBitVector *tmpbv, *extbv;
1265 BtorSMTSymbol *symbol;
1266 int32_t len, tlen;
1267 BtorSMTToken token;
1268
1269 if (isleaf (node))
1270 {
1271 symbol = strip (node);
1272 if (symbol->exp) return symbol->exp;
1273
1274 token = symbol->token;
1275 if (token == BTOR_SMTOK_TRUE || token == BTOR_SMTOK_BIT1)
1276 return symbol->exp = boolector_const (parser->btor, "1");
1277
1278 if (token == BTOR_SMTOK_FALSE || token == BTOR_SMTOK_BIT0)
1279 return symbol->exp = boolector_const (parser->btor, "0");
1280
1281 p = symbol->name;
1282 if (*p++ == 'b' && *p++ == 'v')
1283 {
1284 if (isdigit ((int32_t) *p))
1285 {
1286 start = p++;
1287 for (end = p; isdigit ((int32_t) *end); end++)
1288 ;
1289
1290 if (*end == '[')
1291 {
1292 for (p = end + 1; isdigit ((int32_t) *p); p++)
1293 ;
1294
1295 if (*p == ']')
1296 {
1297 len = atoi (end + 1);
1298 if (len)
1299 {
1300 tmp =
1301 btor_util_dec_to_bin_str_n (parser->mem, start, end - start);
1302
1303 tlen = (int32_t) strlen (tmp);
1304
1305 if (tlen <= len)
1306 {
1307 if (tlen < len)
1308 {
1309 tmpbv = 0;
1310 if (!strcmp (tmp, ""))
1311 extbv = btor_bv_new (parser->mem, len - tlen);
1312 else
1313 {
1314 tmpbv = btor_bv_char_to_bv (parser->mem, tmp);
1315 extbv = btor_bv_uext (parser->mem, tmpbv, len - tlen);
1316 }
1317 ext = btor_bv_to_char (parser->mem, extbv);
1318 btor_mem_freestr (parser->mem, tmp);
1319 btor_bv_free (parser->mem, extbv);
1320 if (tmpbv) btor_bv_free (parser->mem, tmpbv);
1321 tmp = ext;
1322 }
1323
1324 symbol->exp = boolector_const (parser->btor, tmp);
1325 parser->constants++;
1326 }
1327
1328 btor_mem_freestr (parser->mem, tmp);
1329 }
1330 }
1331 }
1332 }
1333 else if (*p == 'b')
1334 {
1335 if (*++p == 'i' && *++p == 'n')
1336 {
1337 for (start = ++p; (ch = *p) == '0' || ch == '1'; p++)
1338 ;
1339
1340 if (start < p && !*p)
1341 {
1342 symbol->exp = boolector_const (parser->btor, start);
1343 parser->constants++;
1344 }
1345 }
1346 }
1347 else if (*p++ == 'h' && *p++ == 'e' && *p++ == 'x')
1348 {
1349 for (start = p; isxdigit ((int32_t) *p); p++)
1350 ;
1351
1352 if (start < p && !*p)
1353 {
1354 len = 4 * (p - start);
1355 tmp = btor_util_hex_to_bin_str (parser->mem, start);
1356 tlen = (int32_t) strlen (tmp);
1357 assert (tlen <= len);
1358 if (tlen < len)
1359 {
1360 tmpbv = 0;
1361 if (!strcmp (tmp, ""))
1362 extbv = btor_bv_new (parser->mem, len - tlen);
1363 else
1364 {
1365 tmpbv = btor_bv_char_to_bv (parser->mem, tmp);
1366 extbv = btor_bv_uext (parser->mem, tmpbv, len - tlen);
1367 }
1368 ext = btor_bv_to_char (parser->mem, extbv);
1369 btor_mem_freestr (parser->mem, tmp);
1370 btor_bv_free (parser->mem, extbv);
1371 if (tmpbv) btor_bv_free (parser->mem, tmpbv);
1372 tmp = ext;
1373 }
1374 symbol->exp = boolector_const (parser->btor, tmp);
1375 btor_mem_freestr (parser->mem, tmp);
1376 parser->constants++;
1377 }
1378 }
1379 else
1380 {
1381 /* DO NOT ADD ANYTHING HERE BECAUSE 'p' CHANGED */
1382 }
1383 }
1384
1385 if (symbol->exp) return symbol->exp;
1386
1387 (void) perr_smt (parser, "'%s' undefined", strip (node)->name);
1388 return 0;
1389 }
1390 else
1391 {
1392 assert (node->exp);
1393 return node->exp;
1394 }
1395
1396 return 0;
1397 }
1398
1399 static BoolectorNode *
node2nonarrayexp(BtorSMTParser * parser,BtorSMTNode * node)1400 node2nonarrayexp (BtorSMTParser *parser, BtorSMTNode *node)
1401 {
1402 BoolectorNode *res;
1403
1404 res = node2exp (parser, node);
1405 if (res && boolector_is_array (parser->btor, res))
1406 {
1407 (void) perr_smt (parser, "unexpected array argument");
1408 res = 0;
1409 }
1410
1411 return res;
1412 }
1413
1414 static void
translate_node(BtorSMTParser * parser,BtorSMTNode * node,BoolectorNode * exp)1415 translate_node (BtorSMTParser *parser, BtorSMTNode *node, BoolectorNode *exp)
1416 {
1417 (void) parser;
1418 assert (!isleaf (node));
1419 assert (!node->exp);
1420 node->exp = exp;
1421 }
1422
1423 static void
translate_symbol(BtorSMTParser * parser,BtorSMTNode * node)1424 translate_symbol (BtorSMTParser *parser, BtorSMTNode *node)
1425 {
1426 BtorSMTNode *c;
1427 BoolectorNode *a;
1428
1429 assert (!node->exp);
1430 if (!is_list_of_length (node, 1))
1431 {
1432 (void) perr_smt (parser, "symbolic head with argument");
1433 return;
1434 }
1435
1436 c = car (node);
1437 if ((a = node2nonarrayexp (parser, c)))
1438 translate_node (parser, node, boolector_copy (parser->btor, a));
1439 }
1440
1441 static void
translate_unary(BtorSMTParser * parser,BtorSMTNode * node,const char * name,BoolectorNode * (* f)(Btor *,BoolectorNode *))1442 translate_unary (BtorSMTParser *parser,
1443 BtorSMTNode *node,
1444 const char *name,
1445 BoolectorNode *(*f) (Btor *, BoolectorNode *) )
1446 {
1447 BtorSMTNode *c;
1448 BoolectorNode *a;
1449
1450 assert (!node->exp);
1451
1452 if (!is_list_of_length (node, 2))
1453 {
1454 (void) perr_smt (parser, "expected exactly one argument to '%s'", name);
1455 return;
1456 }
1457
1458 c = car (cdr (node));
1459 if ((a = node2nonarrayexp (parser, c)))
1460 translate_node (parser, node, f (parser->btor, a));
1461 }
1462
1463 static void
translate_binary(BtorSMTParser * parser,BtorSMTNode * node,const char * name,BoolectorNode * (* f)(Btor *,BoolectorNode *,BoolectorNode *))1464 translate_binary (BtorSMTParser *parser,
1465 BtorSMTNode *node,
1466 const char *name,
1467 BoolectorNode *(*f) (Btor *,
1468 BoolectorNode *,
1469 BoolectorNode *) )
1470 {
1471 BtorSMTNode *c0, *c1;
1472 BoolectorNode *a0, *a1;
1473
1474 assert (!node->exp);
1475
1476 if (!is_list_of_length (node, 3))
1477 {
1478 (void) perr_smt (parser, "expected exactly two arguments to '%s'", name);
1479 return;
1480 }
1481
1482 c0 = car (cdr (node));
1483 c1 = car (cdr (cdr (node)));
1484
1485 if ((a0 = node2nonarrayexp (parser, c0)))
1486 if ((a1 = node2nonarrayexp (parser, c1)))
1487 {
1488 if (boolector_get_width (parser->btor, a0)
1489 != boolector_get_width (parser->btor, a1))
1490 (void) perr_smt (parser, "expression width mismatch");
1491 else
1492 translate_node (parser, node, f (parser->btor, a0, a1));
1493 }
1494 }
1495
1496 static void
translate_eq(BtorSMTParser * parser,BtorSMTNode * node)1497 translate_eq (BtorSMTParser *parser, BtorSMTNode *node)
1498 {
1499 bool isarray0, isarray1;
1500 uint32_t len0, len1;
1501 BtorSMTNode *c0, *c1;
1502 BoolectorNode *a0, *a1;
1503
1504 assert (!node->exp);
1505
1506 if (!is_list_of_length (node, 3))
1507 {
1508 (void) perr_smt (parser, "expected exactly two arguments to '='");
1509 return;
1510 }
1511
1512 c0 = car (cdr (node));
1513 a0 = node2exp (parser, c0);
1514 if (!a0) return;
1515
1516 c1 = car (cdr (cdr (node)));
1517 a1 = node2exp (parser, c1);
1518 if (!a1) return;
1519
1520 len0 = boolector_get_width (parser->btor, a0);
1521 len1 = boolector_get_width (parser->btor, a1);
1522
1523 if (len0 != len1)
1524 {
1525 (void) perr_smt (parser, "expression width mismatch in '='");
1526 return;
1527 }
1528
1529 isarray0 = boolector_is_array (parser->btor, a0);
1530 isarray1 = boolector_is_array (parser->btor, a1);
1531
1532 if (isarray0 != isarray1)
1533 {
1534 (void) perr_smt (parser, "'=' between array and non array expression");
1535 return;
1536 }
1537
1538 if (isarray0 && isarray1)
1539 {
1540 len0 = boolector_get_index_width (parser->btor, a0);
1541 len1 = boolector_get_index_width (parser->btor, a1);
1542
1543 if (len0 != len1)
1544 {
1545 (void) perr_smt (parser, "index width mismatch in '='");
1546 return;
1547 }
1548 }
1549
1550 assert (!parser->error);
1551 translate_node (parser, node, boolector_eq (parser->btor, a0, a1));
1552 }
1553
1554 static void
translate_associative_binary(BtorSMTParser * parser,BtorSMTNode * node,const char * name,BoolectorNode * (* f)(Btor *,BoolectorNode *,BoolectorNode *))1555 translate_associative_binary (BtorSMTParser *parser,
1556 BtorSMTNode *node,
1557 const char *name,
1558 BoolectorNode *(*f) (Btor *,
1559 BoolectorNode *,
1560 BoolectorNode *) )
1561 {
1562 BoolectorNode *res, *tmp, *exp;
1563 BtorSMTNode *child, *p;
1564 uint32_t width;
1565
1566 assert (!node->exp);
1567
1568 child = car (cdr (node));
1569
1570 if (!(exp = node2nonarrayexp (parser, child)))
1571 {
1572 CHECK_FOR_PARSE_ERROR_AND_RETURN:
1573 assert (parser->error);
1574 return;
1575 }
1576
1577 width = boolector_get_width (parser->btor, exp);
1578 res = boolector_copy (parser->btor, exp);
1579
1580 for (p = cdr (cdr (node)); p; p = cdr (p))
1581 {
1582 child = car (p);
1583 if (!(exp = node2nonarrayexp (parser, child)))
1584 {
1585 RELEASE_RES_CHECK_FOR_PARSE_ERROR_AND_RETURN:
1586 boolector_release (parser->btor, res);
1587 assert (parser->error);
1588 goto CHECK_FOR_PARSE_ERROR_AND_RETURN;
1589 }
1590
1591 if (boolector_get_width (parser->btor, exp) != width)
1592 {
1593 perr_smt (parser, "mismatched width of arguments of '%s'", name);
1594 goto RELEASE_RES_CHECK_FOR_PARSE_ERROR_AND_RETURN;
1595 }
1596
1597 tmp = f (parser->btor, res, exp); /* left associative ? */
1598 boolector_release (parser->btor, res);
1599 res = tmp;
1600 }
1601
1602 translate_node (parser, node, res);
1603 }
1604
1605 static void
translate_cond(BtorSMTParser * parser,BtorSMTNode * node,const char * name)1606 translate_cond (BtorSMTParser *parser, BtorSMTNode *node, const char *name)
1607 {
1608 bool isarray1, isarray2;
1609 uint32_t width1, width2;
1610 BtorSMTNode *c0, *c1, *c2;
1611 BoolectorNode *a0, *a1, *a2;
1612
1613 assert (!node->exp);
1614
1615 if (!is_list_of_length (node, 4))
1616 {
1617 (void) perr_smt (parser, "expected exactly three arguments to '%s'", name);
1618 return;
1619 }
1620
1621 c0 = car (cdr (node));
1622 c1 = car (cdr (cdr (node)));
1623 c2 = car (cdr (cdr (cdr (node))));
1624
1625 a0 = node2nonarrayexp (parser, c0);
1626 if (!a0) return;
1627
1628 if (boolector_get_width (parser->btor, a0) != 1)
1629 {
1630 (void) perr_smt (parser, "non boolean conditional");
1631 return;
1632 }
1633
1634 a1 = node2exp (parser, c1);
1635 if (!a1) return;
1636
1637 a2 = node2exp (parser, c2);
1638 if (!a2) return;
1639
1640 width1 = boolector_get_width (parser->btor, a1);
1641 width2 = boolector_get_width (parser->btor, a2);
1642
1643 if (width1 != width2)
1644 {
1645 (void) perr_smt (parser, "expression width mismatch in conditional");
1646 return;
1647 }
1648
1649 isarray1 = boolector_is_array (parser->btor, a1);
1650 isarray2 = boolector_is_array (parser->btor, a2);
1651
1652 if (isarray1 != isarray2)
1653 {
1654 (void) perr_smt (parser,
1655 "conditional between array and non array expression");
1656 return;
1657 }
1658
1659 if (isarray1 && isarray2)
1660 {
1661 width1 = boolector_get_index_width (parser->btor, a1);
1662 width2 = boolector_get_index_width (parser->btor, a2);
1663
1664 if (width1 != width2)
1665 {
1666 (void) perr_smt (parser, "index width mismatch in conditional");
1667 return;
1668 }
1669 }
1670
1671 translate_node (parser, node, boolector_cond (parser->btor, a0, a1, a2));
1672 }
1673
1674 static void
translate_extract(BtorSMTParser * parser,BtorSMTNode * node)1675 translate_extract (BtorSMTParser *parser, BtorSMTNode *node)
1676 {
1677 BtorSMTSymbol *symbol;
1678 uint32_t upper, lower, len;
1679 const char *p;
1680 BoolectorNode *exp;
1681
1682 assert (!node->exp);
1683
1684 symbol = strip (car (node));
1685 assert (symbol->token == BTOR_SMTOK_EXTRACT);
1686 p = symbol->name;
1687
1688 if (!is_list_of_length (node, 2))
1689 {
1690 (void) perr_smt (parser, "expected exactly one argument to '%s'", p);
1691 return;
1692 }
1693
1694 if (!(exp = node2nonarrayexp (parser, car (cdr (node)))))
1695 {
1696 assert (parser->error);
1697 return;
1698 }
1699
1700 len = boolector_get_width (parser->btor, exp);
1701
1702 p = next_numeral (p);
1703 assert (p);
1704 upper = (uint32_t) strtol (p, 0, 10); /* TODO Overflow? */
1705 p = next_numeral (p);
1706 lower = (uint32_t) strtol (p, 0, 10); /* TODO Overflow? */
1707 assert (!next_numeral (p));
1708
1709 if (len <= upper || upper < lower)
1710 {
1711 (void) perr_smt (parser, "invalid '%s' on expression of width %d", p, len);
1712 return;
1713 }
1714
1715 translate_node (
1716 parser, node, boolector_slice (parser->btor, exp, upper, lower));
1717 }
1718
1719 static void
translate_repeat(BtorSMTParser * parser,BtorSMTNode * node)1720 translate_repeat (BtorSMTParser *parser, BtorSMTNode *node)
1721 {
1722 BoolectorNode *tmp, *exp, *res;
1723 BtorSMTSymbol *symbol;
1724 const char *p;
1725 int32_t i, count;
1726
1727 assert (!node->exp);
1728
1729 symbol = strip (car (node));
1730 assert (symbol->token == BTOR_SMTOK_REPEAT);
1731
1732 p = symbol->name;
1733
1734 if (!is_list_of_length (node, 2))
1735 {
1736 (void) perr_smt (parser, "expected exactly one argument to '%s'", p);
1737 return;
1738 }
1739
1740 if (!(exp = node2nonarrayexp (parser, car (cdr (node)))))
1741 {
1742 assert (parser->error);
1743 return;
1744 }
1745
1746 p = next_numeral (p);
1747 assert (p);
1748 assert (!next_numeral (p));
1749 count = atoi (p); /* TODO Overflow? */
1750
1751 if (!count)
1752 {
1753 (void) perr_smt (parser, "can not handle 'repeat[0]'");
1754 return;
1755 }
1756
1757 res = boolector_copy (parser->btor, exp);
1758
1759 for (i = 1; i < count; i++)
1760 {
1761 tmp = boolector_concat (parser->btor, exp, res);
1762 boolector_release (parser->btor, res);
1763 res = tmp;
1764 }
1765
1766 translate_node (parser, node, res);
1767 }
1768
1769 static void
translate_extend(BtorSMTParser * parser,BtorSMTNode * node,BoolectorNode * (* f)(Btor *,BoolectorNode *,uint32_t))1770 translate_extend (BtorSMTParser *parser,
1771 BtorSMTNode *node,
1772 BoolectorNode *(*f) (Btor *, BoolectorNode *, uint32_t))
1773 {
1774 BtorSMTSymbol *symbol;
1775 const char *p;
1776 BoolectorNode *exp;
1777 int32_t pad;
1778
1779 assert (!node->exp);
1780
1781 symbol = strip (car (node));
1782 p = symbol->name;
1783
1784 if (!is_list_of_length (node, 2))
1785 {
1786 (void) perr_smt (parser, "expected exactly one argument to '%s'", p);
1787 return;
1788 }
1789
1790 if (!(exp = node2nonarrayexp (parser, car (cdr (node)))))
1791 {
1792 assert (parser->error);
1793 return;
1794 }
1795
1796 p = next_numeral (p);
1797 assert (p);
1798 assert (!next_numeral (p));
1799 pad = atoi (p); /* TODO Overflow? */
1800
1801 translate_node (parser, node, f (parser->btor, exp, pad));
1802 }
1803
1804 static void
translate_rotate(BtorSMTParser * parser,BtorSMTNode * node)1805 translate_rotate (BtorSMTParser *parser, BtorSMTNode *node)
1806 {
1807 BoolectorNode *exp, *l, *r;
1808 BtorSMTSymbol *symbol;
1809 BtorSMTToken token;
1810 uint32_t shift, width;
1811 const char *p;
1812
1813 assert (!node->exp);
1814
1815 symbol = strip (car (node));
1816 token = symbol->token;
1817 assert (token == BTOR_SMTOK_ROTATE_LEFT || token == BTOR_SMTOK_ROTATE_RIGHT);
1818
1819 p = symbol->name;
1820
1821 if (!is_list_of_length (node, 2))
1822 {
1823 (void) perr_smt (parser, "expected exactly one argument to '%s'", p);
1824 return;
1825 }
1826
1827 if (!(exp = node2nonarrayexp (parser, car (cdr (node)))))
1828 {
1829 assert (parser->error);
1830 return;
1831 }
1832
1833 p = next_numeral (p);
1834 assert (p);
1835 assert (!next_numeral (p));
1836 shift = (uint32_t) strtol (p, 0, 10); /* TODO Overflow? */
1837
1838 width = boolector_get_width (parser->btor, exp);
1839 assert (width > 0);
1840 shift %= width;
1841
1842 if (shift)
1843 {
1844 if (token == BTOR_SMTOK_ROTATE_LEFT) shift = width - shift;
1845
1846 assert (1 <= shift && shift < width);
1847
1848 l = boolector_slice (parser->btor, exp, shift - 1, 0);
1849 r = boolector_slice (parser->btor, exp, width - 1, shift);
1850
1851 translate_node (parser, node, boolector_concat (parser->btor, l, r));
1852 assert (boolector_get_width (parser->btor, node->exp) == width);
1853
1854 boolector_release (parser->btor, l);
1855 boolector_release (parser->btor, r);
1856 }
1857 else
1858 translate_node (parser, node, boolector_copy (parser->btor, exp));
1859 }
1860
1861 static void
translate_concat(BtorSMTParser * parser,BtorSMTNode * node)1862 translate_concat (BtorSMTParser *parser, BtorSMTNode *node)
1863 {
1864 BtorSMTNode *c0, *c1;
1865 BoolectorNode *a0, *a1;
1866
1867 assert (!node->exp);
1868
1869 if (!is_list_of_length (node, 3))
1870 {
1871 (void) perr_smt (parser, "expected exactly two arguments to 'concat'");
1872 return;
1873 }
1874
1875 c0 = car (cdr (node));
1876 c1 = car (cdr (cdr (node)));
1877
1878 if ((a0 = node2nonarrayexp (parser, c0)))
1879 if ((a1 = node2nonarrayexp (parser, c1)))
1880 translate_node (parser, node, boolector_concat (parser->btor, a0, a1));
1881 }
1882
1883 static void
translate_shift(BtorSMTParser * parser,BtorSMTNode * node,const char * name,BoolectorNode * (* f)(Btor *,BoolectorNode *,BoolectorNode *))1884 translate_shift (BtorSMTParser *parser,
1885 BtorSMTNode *node,
1886 const char *name,
1887 BoolectorNode *(*f) (Btor *,
1888 BoolectorNode *,
1889 BoolectorNode *) )
1890 {
1891 BoolectorNode *a0, *a1, *c, *e, *t, *e0, *u, *l, *tmp;
1892 uint32_t width, l0, l1, p0, p1;
1893 BtorSMTNode *c0, *c1;
1894 BoolectorSort s;
1895
1896 assert (!node->exp);
1897
1898 if (!is_list_of_length (node, 3))
1899 {
1900 (void) perr_smt (parser, "expected exactly two arguments to '%s'", name);
1901 return;
1902 }
1903
1904 c0 = car (cdr (node));
1905 c1 = car (cdr (cdr (node)));
1906
1907 if (!(a0 = node2nonarrayexp (parser, c0)))
1908 {
1909 assert (parser->error);
1910 return;
1911 }
1912
1913 if (!(a1 = node2nonarrayexp (parser, c1)))
1914 {
1915 assert (parser->error);
1916 return;
1917 }
1918
1919 width = boolector_get_width (parser->btor, a0);
1920
1921 if (width != boolector_get_width (parser->btor, a1))
1922 {
1923 (void) perr_smt (parser, "expression width mismatch");
1924 return;
1925 }
1926
1927 l1 = 0;
1928 for (l0 = 1; l0 < width; l0 *= 2) l1++;
1929
1930 assert (l0 == (1u << l1));
1931
1932 if (width == 1)
1933 {
1934 assert (l0 == 1);
1935 assert (l1 == 0);
1936
1937 if (f == boolector_sra)
1938 translate_node (parser, node, boolector_copy (parser->btor, a0));
1939 else
1940 {
1941 tmp = boolector_not (parser->btor, a1);
1942 translate_node (parser, node, boolector_and (parser->btor, a0, tmp));
1943 boolector_release (parser->btor, tmp);
1944 }
1945 }
1946 else
1947 {
1948 assert (width >= 1);
1949 assert (width <= l0);
1950
1951 p0 = l0 - width;
1952 p1 = width - l1;
1953
1954 assert (p1 > 0);
1955
1956 u = boolector_slice (parser->btor, a1, width - 1, width - p1);
1957 l = boolector_slice (parser->btor, a1, l1 - 1, 0);
1958
1959 assert (boolector_get_width (parser->btor, u) == p1);
1960 assert (boolector_get_width (parser->btor, l) == l1);
1961
1962 if (p1 > 1)
1963 c = boolector_redor (parser->btor, u);
1964 else
1965 c = boolector_copy (parser->btor, u);
1966
1967 boolector_release (parser->btor, u);
1968
1969 if (f == boolector_sra)
1970 {
1971 tmp = boolector_slice (parser->btor, a0, width - 1, width - 1);
1972 t = boolector_sext (parser->btor, tmp, width - 1);
1973 boolector_release (parser->btor, tmp);
1974 }
1975 else
1976 {
1977 s = boolector_bitvec_sort (parser->btor, width);
1978 t = boolector_zero (parser->btor, s);
1979 boolector_release_sort (parser->btor, s);
1980 }
1981
1982 if (!p0)
1983 e0 = boolector_copy (parser->btor, a0);
1984 else if (f == boolector_sra)
1985 e0 = boolector_sext (parser->btor, a0, p0);
1986 else
1987 e0 = boolector_uext (parser->btor, a0, p0);
1988
1989 assert (boolector_get_width (parser->btor, e0) == l0);
1990
1991 e = f (parser->btor, e0, l);
1992 boolector_release (parser->btor, e0);
1993 boolector_release (parser->btor, l);
1994
1995 if (p0 > 0)
1996 {
1997 tmp = boolector_slice (parser->btor, e, width - 1, 0);
1998 boolector_release (parser->btor, e);
1999 e = tmp;
2000 }
2001
2002 translate_node (parser, node, boolector_cond (parser->btor, c, t, e));
2003
2004 boolector_release (parser->btor, c);
2005 boolector_release (parser->btor, t);
2006 boolector_release (parser->btor, e);
2007 }
2008 }
2009
2010 static void
translate_select(BtorSMTParser * parser,BtorSMTNode * node)2011 translate_select (BtorSMTParser *parser, BtorSMTNode *node)
2012 {
2013 BtorSMTNode *c0, *c1;
2014 BoolectorNode *a0, *a1;
2015
2016 assert (!node->exp);
2017
2018 if (!is_list_of_length (node, 3))
2019 {
2020 (void) perr_smt (parser, "expected exactly two arguments to 'select'");
2021 return;
2022 }
2023
2024 c0 = car (cdr (node));
2025 c1 = car (cdr (cdr (node)));
2026
2027 if (!(a0 = node2exp (parser, c0)))
2028 {
2029 assert (parser->error);
2030 return;
2031 }
2032
2033 if (!boolector_is_array (parser->btor, a0))
2034 {
2035 (void) perr_smt (parser, "invalid first argument to 'select'");
2036 return;
2037 }
2038
2039 if (!(a1 = node2nonarrayexp (parser, c1)))
2040 {
2041 assert (parser->error);
2042 return;
2043 }
2044
2045 if (boolector_get_index_width (parser->btor, a0)
2046 != boolector_get_width (parser->btor, a1))
2047 {
2048 (void) perr_smt (parser, "mismatched bit width of 'select' index");
2049 return;
2050 }
2051
2052 translate_node (parser, node, boolector_read (parser->btor, a0, a1));
2053 }
2054
2055 static void
translate_store(BtorSMTParser * parser,BtorSMTNode * node)2056 translate_store (BtorSMTParser *parser, BtorSMTNode *node)
2057 {
2058 BtorSMTNode *c0, *c1, *c2;
2059 BoolectorNode *a0, *a1, *a2;
2060
2061 assert (!node->exp);
2062
2063 if (!is_list_of_length (node, 4))
2064 {
2065 (void) perr_smt (parser, "expected exactly three arguments to 'store'");
2066 return;
2067 }
2068
2069 c0 = car (cdr (node));
2070 c1 = car (cdr (cdr (node)));
2071 c2 = car (cdr (cdr (cdr (node))));
2072
2073 if (!(a0 = node2exp (parser, c0)))
2074 {
2075 assert (parser->error);
2076 return;
2077 }
2078
2079 if (!boolector_is_array (parser->btor, a0))
2080 {
2081 (void) perr_smt (parser, "invalid first argument to 'store'");
2082 return;
2083 }
2084
2085 if (!(a1 = node2nonarrayexp (parser, c1)))
2086 {
2087 assert (parser->error);
2088 return;
2089 }
2090
2091 if (boolector_get_index_width (parser->btor, a0)
2092 != boolector_get_width (parser->btor, a1))
2093 {
2094 (void) perr_smt (parser, "mismatched bit width of 'store' index");
2095 return;
2096 }
2097
2098 if (!(a2 = node2nonarrayexp (parser, c2)))
2099 {
2100 assert (parser->error);
2101 return;
2102 }
2103
2104 if (boolector_get_width (parser->btor, a2)
2105 != boolector_get_width (parser->btor, a0))
2106 {
2107 (void) perr_smt (parser, "mismatched bit width of 'store' value");
2108 return;
2109 }
2110
2111 translate_node (parser, node, boolector_write (parser->btor, a0, a1, a2));
2112 }
2113
2114 static BoolectorNode *
translate_formula(BtorSMTParser * parser,BtorSMTNode * root)2115 translate_formula (BtorSMTParser *parser, BtorSMTNode *root)
2116 {
2117 BtorSMTNode *node, *child, *p, **s, **t, *tmp;
2118 BtorSMTNode *assignment, *body;
2119 BtorSMTSymbol *symbol;
2120 BtorSMTToken token;
2121 uint32_t start, end;
2122 BoolectorNode *exp;
2123
2124 assert (BTOR_EMPTY_STACK (parser->work));
2125 assert (BTOR_EMPTY_STACK (parser->stack));
2126
2127 assert (root);
2128 BTOR_PUSH_STACK (parser->stack, root);
2129
2130 while (!BTOR_EMPTY_STACK (parser->stack))
2131 {
2132 node = BTOR_POP_STACK (parser->stack);
2133
2134 if (node)
2135 {
2136 if (isleaf (node))
2137 {
2138 /* DO NOTHING HERE */
2139 }
2140 else if (car (node) == parser->bind)
2141 {
2142 BTOR_PUSH_STACK (parser->work, node);
2143 }
2144 else if (is_let_or_flet (car (node)))
2145 {
2146 /* node == ([f]let assignment body)
2147 * assignment == (var term)
2148 */
2149 if (!cdr (node) || !(assignment = car (cdr (node)))
2150 || isleaf (assignment) || !(token = node2token (car (assignment)))
2151 || (token != BTOR_SMTOK_FVAR && token != BTOR_SMTOK_VAR)
2152 || !cdr (assignment) || cdr (cdr (assignment)) || !cdr (cdr (node))
2153 || cdr (cdr (cdr (node))))
2154 return perr_smt (parser, "illformed 'let' or 'flet'"),
2155 (BoolectorNode *) 0;
2156
2157 body = car (cdr (cdr (node)));
2158
2159 BTOR_PUSH_STACK (parser->stack, node);
2160 BTOR_PUSH_STACK (parser->stack, 0);
2161
2162 BTOR_PUSH_STACK (parser->stack, body);
2163
2164 BTOR_PUSH_STACK (parser->stack,
2165 cons (parser, parser->bind, assignment));
2166
2167 BTOR_PUSH_STACK (parser->stack, car (cdr (assignment)));
2168 }
2169 else
2170 {
2171 BTOR_PUSH_STACK (parser->stack, node);
2172 BTOR_PUSH_STACK (parser->stack, 0);
2173
2174 start = BTOR_COUNT_STACK (parser->stack);
2175
2176 for (p = node; p; p = cdr (p))
2177 {
2178 child = car (p);
2179 assert (child);
2180 BTOR_PUSH_STACK (parser->stack, child);
2181 }
2182
2183 end = BTOR_COUNT_STACK (parser->stack);
2184
2185 if (start < end)
2186 {
2187 s = parser->stack.start + start;
2188 t = parser->stack.start + end - 1;
2189
2190 while (s < t)
2191 {
2192 tmp = *s;
2193 *s = *t;
2194 *t = tmp;
2195
2196 s++;
2197 t--;
2198 }
2199 }
2200 }
2201 }
2202 else
2203 {
2204 assert (!BTOR_EMPTY_STACK (parser->stack));
2205
2206 node = BTOR_POP_STACK (parser->stack);
2207
2208 assert (node);
2209 assert (!isleaf (node));
2210
2211 BTOR_PUSH_STACK (parser->work, node);
2212 }
2213 }
2214
2215 node = 0;
2216 for (s = parser->work.start; s < parser->work.top; s++)
2217 {
2218 node = *s;
2219
2220 assert (node);
2221 assert (!isleaf (node));
2222
2223 child = car (node);
2224
2225 if (!child) return perr_smt (parser, "empty list"), (BoolectorNode *) 0;
2226
2227 if (isleaf (child))
2228 {
2229 symbol = strip (child);
2230
2231 switch (symbol->token)
2232 {
2233 case BTOR_SMTOK_NOT:
2234 translate_unary (parser, node, "not", boolector_not);
2235 break;
2236 case BTOR_SMTOK_AND:
2237 translate_associative_binary (parser, node, "and", boolector_and);
2238 break;
2239 case BTOR_SMTOK_OR:
2240 translate_associative_binary (parser, node, "or", boolector_or);
2241 break;
2242 case BTOR_SMTOK_IMPLIES:
2243 translate_binary (parser, node, "implies", boolector_implies);
2244 break;
2245 case BTOR_SMTOK_XOR:
2246 translate_associative_binary (parser, node, "xor", boolector_xor);
2247 break;
2248 case BTOR_SMTOK_IFF:
2249 translate_associative_binary (parser, node, "iff", boolector_xnor);
2250 break;
2251
2252 case BTOR_SMTOK_EQ: translate_eq (parser, node); break;
2253
2254 case BTOR_SMTOK_DISTINCT:
2255 translate_binary (parser, node, "distinct", boolector_ne);
2256 break;
2257 case BTOR_SMTOK_ITE: translate_cond (parser, node, "ite"); break;
2258 case BTOR_SMTOK_IF_THEN_ELSE:
2259 translate_cond (parser, node, "if_then_else");
2260 break;
2261 case BTOR_SMTOK_BIND:
2262 assert (cdr (node));
2263 assert (cdr (cdr (node)));
2264 assert (!cdr (cdr (cdr (node))));
2265 assert (isleaf (car (cdr (node))));
2266 symbol = strip (car (cdr (node)));
2267 if (symbol->exp)
2268 return perr_smt (parser, "unsupported nested '[f]let'"),
2269 (BoolectorNode *) 0;
2270 body = car (cdr (cdr (node)));
2271 if ((exp = node2exp (parser, body)))
2272 {
2273 if (symbol->token == BTOR_SMTOK_FVAR)
2274 {
2275 if (boolector_get_width (parser->btor, exp) != 1)
2276 {
2277 return perr_smt (parser, "flet assignment width not one"),
2278 (BoolectorNode *) 0;
2279 }
2280 }
2281 else
2282 assert (symbol->token == BTOR_SMTOK_VAR);
2283
2284 assert (!symbol->exp);
2285 symbol->exp = boolector_copy (parser->btor, exp);
2286 }
2287 /* Prevent leaking of 'bind' nodes. */
2288 *s = 0;
2289 delete_smt_node (parser, node);
2290 break;
2291 case BTOR_SMTOK_LET:
2292 case BTOR_SMTOK_FLET:
2293 symbol = strip (car (car (cdr (node))));
2294 assert (symbol->token == BTOR_SMTOK_FVAR
2295 || symbol->token == BTOR_SMTOK_VAR);
2296 assert (symbol->exp);
2297 body = car (cdr (cdr (node)));
2298 if ((exp = node2exp (parser, body)))
2299 node->exp = boolector_copy (parser->btor, exp);
2300 boolector_release (parser->btor, symbol->exp);
2301 symbol->exp = 0;
2302 break;
2303 case BTOR_SMTOK_EXTRACT: translate_extract (parser, node); break;
2304 case BTOR_SMTOK_REPEAT: translate_repeat (parser, node); break;
2305 case BTOR_SMTOK_ZERO_EXTEND:
2306 translate_extend (parser, node, boolector_uext);
2307 break;
2308 case BTOR_SMTOK_SIGN_EXTEND:
2309 translate_extend (parser, node, boolector_sext);
2310 break;
2311 case BTOR_SMTOK_ROTATE_RIGHT:
2312 case BTOR_SMTOK_ROTATE_LEFT: translate_rotate (parser, node); break;
2313 case BTOR_SMTOK_CONCAT: translate_concat (parser, node); break;
2314 case BTOR_SMTOK_BVNOT:
2315 translate_unary (parser, node, "bvnot", boolector_not);
2316 break;
2317 case BTOR_SMTOK_BVNEG:
2318 translate_unary (parser, node, "bvneg", boolector_neg);
2319 break;
2320 case BTOR_SMTOK_BVADD:
2321 translate_associative_binary (parser, node, "bvadd", boolector_add);
2322 break;
2323 case BTOR_SMTOK_BVSUB:
2324 translate_binary (parser, node, "bvsub", boolector_sub);
2325 break;
2326 case BTOR_SMTOK_BVSDIV:
2327 translate_binary (parser, node, "bvsdiv", boolector_sdiv);
2328 break;
2329 case BTOR_SMTOK_BVUDIV:
2330 translate_binary (parser, node, "bvudiv", boolector_udiv);
2331 break;
2332 case BTOR_SMTOK_BVUREM:
2333 translate_binary (parser, node, "bvurem", boolector_urem);
2334 break;
2335 case BTOR_SMTOK_BVSREM:
2336 translate_binary (parser, node, "bvsrem", boolector_srem);
2337 break;
2338 case BTOR_SMTOK_BVSMOD:
2339 translate_binary (parser, node, "bvsmod", boolector_smod);
2340 break;
2341 case BTOR_SMTOK_BVMUL:
2342 translate_associative_binary (parser, node, "bvmul", boolector_mul);
2343 break;
2344 case BTOR_SMTOK_BVULE:
2345 translate_binary (parser, node, "bvule", boolector_ulte);
2346 break;
2347 case BTOR_SMTOK_BVSLE:
2348 translate_binary (parser, node, "bvsle", boolector_slte);
2349 break;
2350 case BTOR_SMTOK_BVSGT:
2351 translate_binary (parser, node, "bvsgt", boolector_sgt);
2352 break;
2353 case BTOR_SMTOK_BVSGE:
2354 translate_binary (parser, node, "bvsge", boolector_sgte);
2355 break;
2356 case BTOR_SMTOK_BVCOMP:
2357 translate_binary (parser, node, "bvcomp", boolector_eq);
2358 break;
2359 case BTOR_SMTOK_BVULT:
2360 translate_binary (parser, node, "bvult", boolector_ult);
2361 break;
2362 case BTOR_SMTOK_BVUGT:
2363 translate_binary (parser, node, "bvugt", boolector_ugt);
2364 break;
2365 case BTOR_SMTOK_BVUGE:
2366 translate_binary (parser, node, "bvuge", boolector_ugte);
2367 break;
2368 case BTOR_SMTOK_BVSLT:
2369 translate_binary (parser, node, "bvslt", boolector_slt);
2370 break;
2371 case BTOR_SMTOK_BVAND:
2372 translate_binary (parser, node, "bvand", boolector_and);
2373 break;
2374 case BTOR_SMTOK_BVOR:
2375 translate_binary (parser, node, "bvor", boolector_or);
2376 break;
2377 case BTOR_SMTOK_BVXOR:
2378 translate_binary (parser, node, "bvxor", boolector_xor);
2379 break;
2380 case BTOR_SMTOK_BVXNOR:
2381 translate_binary (parser, node, "bvxnor", boolector_xnor);
2382 break;
2383 case BTOR_SMTOK_BVNOR:
2384 translate_binary (parser, node, "bvnor", boolector_nor);
2385 break;
2386 case BTOR_SMTOK_BVNAND:
2387 translate_binary (parser, node, "bvnand", boolector_nand);
2388 break;
2389 case BTOR_SMTOK_BVLSHR:
2390 translate_shift (parser, node, "bvlshr", boolector_srl);
2391 break;
2392 case BTOR_SMTOK_BVASHR:
2393 translate_shift (parser, node, "bvashr", boolector_sra);
2394 break;
2395 case BTOR_SMTOK_BVSHL:
2396 translate_shift (parser, node, "bvshl", boolector_sll);
2397 break;
2398 case BTOR_SMTOK_SELECT: translate_select (parser, node); break;
2399 case BTOR_SMTOK_STORE: translate_store (parser, node); break;
2400 default:
2401 assert (symbol->token != BTOR_SMTOK_TRANSLATED);
2402 translate_symbol (parser, node);
2403 break;
2404 }
2405 }
2406 else
2407 {
2408 if (is_list_of_length (node, 1))
2409 {
2410 if ((exp = node2exp (parser, child)))
2411 translate_node (parser, node, boolector_copy (parser->btor, exp));
2412 }
2413 else
2414 (void) perr_smt (parser, "invalid list expression");
2415 }
2416
2417 if (parser->error) return (BoolectorNode *) 0;
2418 }
2419
2420 BTOR_RESET_STACK (parser->work);
2421
2422 if (!(exp = node2exp (parser, root)))
2423 {
2424 assert (parser->error);
2425 return (BoolectorNode *) 0;
2426 }
2427
2428 if (boolector_get_width (parser->btor, exp) != 1)
2429 return perr_smt (parser, "non boolean formula"), (BoolectorNode *) 0;
2430
2431 assert (!parser->error);
2432
2433 assert (exp);
2434
2435 return boolector_copy (parser->btor, exp);
2436 }
2437
2438 static void
smt_parser_inc_add_release_sat(BtorSMTParser * parser,BtorParseResult * res,BoolectorNode * exp)2439 smt_parser_inc_add_release_sat (BtorSMTParser *parser,
2440 BtorParseResult *res,
2441 BoolectorNode *exp)
2442 {
2443 char *prefix;
2444 int32_t satres, nchecked, ndigits;
2445 uint32_t formula;
2446 assert (parser->formulas.nchecked < parser->formulas.nparsed);
2447 formula = parser->formulas.nchecked;
2448 nchecked = 1;
2449
2450 if (parser->formulas.nchecked + 1 == parser->formulas.nparsed)
2451 {
2452 smt_message (parser, 3, "adding last ':formula' %d permanently", formula);
2453 boolector_assert (parser->btor, exp);
2454 }
2455 else
2456 {
2457 smt_message (parser, 3, "adding ':formula' %d as assumption", formula);
2458 boolector_assume (parser->btor, exp);
2459 }
2460 boolector_release (parser->btor, exp);
2461
2462 satres = boolector_sat (parser->btor);
2463 res->nsatcalls += 1;
2464 if (satres == BOOLECTOR_SAT)
2465 {
2466 smt_message (parser, 1, "':formula' %d SAT", formula);
2467 res->result = BOOLECTOR_SAT;
2468 fprintf (parser->outfile, "sat\n");
2469 }
2470 else
2471 {
2472 assert (satres == BOOLECTOR_UNSAT);
2473 smt_message (parser, 1, "':formula' %d UNSAT", formula);
2474 if (res->result == BOOLECTOR_UNKNOWN) res->result = BOOLECTOR_UNSAT;
2475 fprintf (parser->outfile, "unsat\n");
2476 }
2477 if (parser->verbosity >= 2) boolector_print_stats (parser->btor);
2478
2479 parser->formulas.nchecked += nchecked;
2480
2481 ndigits = btor_util_num_digits (parser->formulas.nchecked) + 3;
2482 BTOR_NEWN (parser->mem, prefix, ndigits);
2483 sprintf (prefix, "%d:", parser->formulas.nchecked);
2484 boolector_set_msg_prefix (parser->btor, prefix);
2485 BTOR_DELETEN (parser->mem, prefix, ndigits);
2486
2487 if (parser->formulas.nchecked == parser->formulas.nparsed)
2488 boolector_set_msg_prefix (parser->btor, 0);
2489 }
2490
2491 static bool
continue_parsing(BtorSMTParser * parser,BtorParseResult * res)2492 continue_parsing (BtorSMTParser *parser, BtorParseResult *res)
2493 {
2494 if (res->result != BOOLECTOR_SAT) return true;
2495 return parser->incremental
2496 && parser->incremental_smt1 == BTOR_INCREMENTAL_SMT1_CONTINUE;
2497 }
2498
2499 static char *
translate_benchmark(BtorSMTParser * parser,BtorSMTNode * top,BtorParseResult * res)2500 translate_benchmark (BtorSMTParser *parser,
2501 BtorSMTNode *top,
2502 BtorParseResult *res)
2503 {
2504 BtorSMTSymbol *symbol, *logic, *benchmark;
2505 BtorSMTNode *p, *node, *q;
2506 BoolectorNode *exp;
2507 BtorSMTToken status;
2508
2509 smt_message (parser, 2, "extracting expressions");
2510
2511 p = top;
2512
2513 if (!p || !(node = car (p)) || !isleaf (node)
2514 || strip (node)->token != BTOR_SMTOK_BENCHMARK)
2515 return perr_smt (parser, "expected 'benchmark' keyword");
2516
2517 p = cdr (p);
2518
2519 if (!p || !(benchmark = car (p)) || !isleaf (benchmark)
2520 || strip (benchmark)->token != BTOR_SMTOK_IDENTIFIER)
2521 return perr_smt (parser, "expected benchmark name");
2522
2523 benchmark = strip (benchmark);
2524
2525 smt_message (parser, 2, "benchmark %s", benchmark->name);
2526
2527 symbol = 0;
2528
2529 for (p = top; p; p = cdr (p))
2530 {
2531 node = car (p);
2532 if (!isleaf (node)) continue;
2533
2534 symbol = strip (node);
2535
2536 if (symbol->token == BTOR_SMTOK_EXTRASORTS
2537 || symbol->token == BTOR_SMTOK_EXTRAFUNS
2538 || symbol->token == BTOR_SMTOK_EXTRAPREDS
2539 || symbol->token == BTOR_SMTOK_ASSUMPTION
2540 || symbol->token == BTOR_SMTOK_FORMULA)
2541 return perr_smt (parser, "'%s' before ':logic'", symbol->name);
2542
2543 if (symbol->token == BTOR_SMTOK_LOGICATTR) break;
2544 }
2545
2546 if (!p) return perr_smt (parser, "no ':logic' attribute found");
2547
2548 p = cdr (p);
2549 if (!p) return perr_smt (parser, "argument to ':logic' missing");
2550
2551 node = car (p);
2552 if (!isleaf (node)) return perr_smt (parser, "invalid argument to ':logic'");
2553
2554 logic = strip (node);
2555 if (!strcmp (logic->name, "QF_BV"))
2556 res->logic = BTOR_LOGIC_QF_BV;
2557 else if (!strcmp (logic->name, "QF_AUFBV") || !strcmp (logic->name, "QF_ABV"))
2558 res->logic = BTOR_LOGIC_QF_AUFBV;
2559 else
2560 return perr_smt (parser, "unsupported logic '%s'", logic->name);
2561
2562 for (p = top; p; p = cdr (p))
2563 {
2564 node = car (p);
2565 if (!isleaf (node)) continue;
2566
2567 symbol = strip (node);
2568 if (symbol->token == BTOR_SMTOK_STATUS) break;
2569 }
2570
2571 if (p)
2572 {
2573 p = cdr (p);
2574 if (!p) return perr_smt (parser, "argument to ':status' missing");
2575
2576 node = car (p);
2577 if (!isleaf (node))
2578 {
2579 INVALID_STATUS_ARGUMENT:
2580 return perr_smt (parser, "invalid ':status' argument");
2581 }
2582
2583 symbol = strip (node);
2584 status = symbol->token;
2585
2586 if (status == BTOR_SMTOK_SAT)
2587 res->status = BOOLECTOR_SAT;
2588 else if (status == BTOR_SMTOK_UNSAT)
2589 res->status = BOOLECTOR_UNSAT;
2590 else if (status == BTOR_SMTOK_UNKNOWN)
2591 res->status = BOOLECTOR_UNKNOWN;
2592 else
2593 goto INVALID_STATUS_ARGUMENT;
2594 }
2595
2596 for (p = top; p && continue_parsing (parser, res); p = cdr (p))
2597 {
2598 q = p;
2599 node = car (p);
2600 if (!isleaf (node)) goto CONTINUE;
2601
2602 symbol = strip (node);
2603
2604 switch (symbol->token)
2605 {
2606 case BTOR_SMTOK_EXTRAFUNS:
2607 p = cdr (p);
2608 if (!p) return perr_smt (parser, "argument to ':extrafuns' missing");
2609
2610 if (!extrafuns (parser, car (p)))
2611 {
2612 assert (parser->error);
2613 return parser->error;
2614 }
2615
2616 break;
2617
2618 case BTOR_SMTOK_EXTRAPREDS:
2619
2620 p = cdr (p);
2621 if (!p) return perr_smt (parser, "argument to ':extrapreds' missing");
2622
2623 if (!extrapreds (parser, car (p)))
2624 {
2625 assert (parser->error);
2626 return parser->error;
2627 }
2628
2629 break;
2630
2631 case BTOR_SMTOK_ASSUMPTION:
2632
2633 p = cdr (p);
2634 if (!p) return perr_smt (parser, "argument to ':assumption' missing");
2635
2636 exp = translate_formula (parser, car (p));
2637 if (!exp)
2638 {
2639 assert (parser->error);
2640 return parser->error;
2641 }
2642
2643 recursively_delete_smt_node (parser, p->head);
2644 p->head = 0;
2645
2646 if (parser->incremental)
2647 {
2648 smt_message (parser,
2649 3,
2650 "adding ':assumption' %d",
2651 parser->assumptions.handled);
2652 }
2653 boolector_assert (parser->btor, exp);
2654 boolector_release (parser->btor, exp);
2655
2656 parser->assumptions.handled++;
2657
2658 break;
2659
2660 case BTOR_SMTOK_FORMULA:
2661
2662 p = cdr (p);
2663 if (!p) return perr_smt (parser, "argument to ':formula' missing");
2664
2665 exp = translate_formula (parser, car (p));
2666 if (!exp)
2667 {
2668 assert (parser->error);
2669 return parser->error;
2670 }
2671
2672 recursively_delete_smt_node (parser, p->head);
2673 p->head = 0;
2674
2675 if (!parser->incremental)
2676 {
2677 boolector_assert (parser->btor, exp);
2678 boolector_release (parser->btor, exp);
2679 }
2680 else
2681 smt_parser_inc_add_release_sat (parser, res, exp);
2682
2683 parser->formulas.handled++;
2684
2685 break;
2686
2687 case BTOR_SMTOK_EXTRASORTS:
2688 return perr_smt (parser, "':extrasorts' unsupported");
2689
2690 default: break;
2691 }
2692 CONTINUE:
2693 for (;;)
2694 {
2695 node = q->head;
2696 q->head = 0;
2697 recursively_delete_smt_node (parser, node);
2698 if (q == p) break;
2699 q = cdr (q);
2700 }
2701 }
2702
2703 if (parser->required_logic == BTOR_LOGIC_QF_AUFBV
2704 && res->logic == BTOR_LOGIC_QF_BV)
2705 {
2706 if (parser->incremental)
2707 {
2708 smt_message (
2709 parser,
2710 1,
2711 "need QF_AUFBV but only QF_BV specified in incremental mode");
2712 res->logic = BTOR_LOGIC_QF_AUFBV;
2713 }
2714 else
2715 return perr_smt (
2716 parser,
2717 "need QF_AUFBV but only QF_BV specified in non-incremental mode");
2718 }
2719
2720 if (parser->required_logic == BTOR_LOGIC_QF_BV
2721 && res->logic == BTOR_LOGIC_QF_AUFBV)
2722 {
2723 smt_message (
2724 parser,
2725 1,
2726 "no arrays found: only need QF_BV (even though QF_AUFBV specified)");
2727 res->logic = BTOR_LOGIC_QF_BV;
2728 }
2729
2730 assert (!parser->error);
2731
2732 return 0;
2733 }
2734
2735 static void
count_assumptions_and_formulas(BtorSMTParser * parser,BtorSMTNode * top)2736 count_assumptions_and_formulas (BtorSMTParser *parser, BtorSMTNode *top)
2737 {
2738 BtorSMTNode *p, *n;
2739 BtorSMTSymbol *s;
2740
2741 parser->formulas.nparsed = parser->assumptions.nparsed = 0;
2742
2743 for (p = top; p; p = cdr (p))
2744 {
2745 n = car (p);
2746
2747 if (!isleaf (n)) continue;
2748
2749 s = strip (n);
2750
2751 if (s->token == BTOR_SMTOK_FORMULA) parser->formulas.nparsed++;
2752
2753 if (s->token == BTOR_SMTOK_ASSUMPTION) parser->assumptions.nparsed++;
2754 }
2755 }
2756
2757 static void
set_last_occurrence_of_symbols(BtorSMTParser * parser,BtorSMTNode * top)2758 set_last_occurrence_of_symbols (BtorSMTParser *parser, BtorSMTNode *top)
2759 {
2760 BtorSMTNode *n, *h, *t;
2761 BtorSMTSymbol *s;
2762 uint32_t occs = 0;
2763
2764 assert (BTOR_EMPTY_STACK (parser->stack));
2765
2766 BTOR_PUSH_STACK (parser->stack, top);
2767 while (!BTOR_EMPTY_STACK (parser->stack))
2768 {
2769 n = BTOR_POP_STACK (parser->stack);
2770 if (isleaf (n)) continue;
2771
2772 h = car (n);
2773 t = cdr (n);
2774
2775 if (t)
2776 {
2777 assert (!isleaf (t));
2778 BTOR_PUSH_STACK (parser->stack, t);
2779 }
2780
2781 assert (h);
2782 if (isleaf (h))
2783 {
2784 s = strip (h);
2785 if (s->token == BTOR_SMTOK_IDENTIFIER)
2786 {
2787 s->last = n;
2788 occs++;
2789 }
2790 }
2791 else
2792 BTOR_PUSH_STACK (parser->stack, h);
2793 }
2794
2795 smt_message (parser, 1, "found %u occurrences of symbols", occs);
2796 }
2797
2798 /* Note: we need prefix in case of stdin as input (also applies to compressed
2799 * input files). */
2800 static const char *
parse(BtorSMTParser * parser,BtorCharStack * prefix,FILE * infile,const char * infile_name,FILE * outfile,BtorParseResult * res)2801 parse (BtorSMTParser *parser,
2802 BtorCharStack *prefix,
2803 FILE *infile,
2804 const char *infile_name,
2805 FILE *outfile,
2806 BtorParseResult *res)
2807 {
2808 BtorSMTNode *node, *top, **p, **first;
2809 BtorSMTToken token;
2810 const char *err;
2811 int32_t head;
2812
2813 assert (!parser->parsed);
2814 parser->parsed = true;
2815
2816 smt_message (parser, 1, "parsing SMT file %s", infile_name);
2817
2818 parser->infile_name = infile_name;
2819 parser->nprefix = 0;
2820 parser->prefix = prefix;
2821 parser->infile = infile;
2822 parser->outfile = outfile;
2823 parser->lineno = 1;
2824 parser->saved = false;
2825
2826 BTOR_CLR (res);
2827
2828 res->status = BOOLECTOR_UNKNOWN;
2829 res->result = BOOLECTOR_UNKNOWN;
2830
2831 assert (BTOR_EMPTY_STACK (parser->stack));
2832 assert (BTOR_EMPTY_STACK (parser->heads));
2833
2834 NEXT_TOKEN:
2835
2836 token = nextok (parser);
2837
2838 if (token == BTOR_SMTOK_LP)
2839 {
2840 head = BTOR_COUNT_STACK (parser->stack);
2841 BTOR_PUSH_STACK (parser->heads, head);
2842 goto NEXT_TOKEN;
2843 }
2844
2845 if (token == BTOR_SMTOK_RP)
2846 {
2847 if (BTOR_EMPTY_STACK (parser->heads))
2848 return perr_smt (parser, "too many closing ')'");
2849
2850 node = 0;
2851 head = BTOR_POP_STACK (parser->heads);
2852 assert ((size_t) head <= BTOR_COUNT_STACK (parser->stack));
2853 first = parser->stack.start + head;
2854 p = parser->stack.top;
2855 while (first < p) node = cons (parser, *--p, node);
2856
2857 parser->stack.top = first;
2858 BTOR_PUSH_STACK (parser->stack, node);
2859
2860 if (!BTOR_EMPTY_STACK (parser->heads)) goto NEXT_TOKEN;
2861
2862 token = nextok (parser);
2863 if (token != BTOR_SMTOK_EOF) return perr_smt (parser, "expected EOF");
2864
2865 assert (BTOR_COUNT_STACK (parser->stack) == 1);
2866 top = parser->stack.start[0];
2867 BTOR_RESET_STACK (parser->stack);
2868
2869 smt_message (parser, 2, "read %llu bytes", parser->bytes);
2870 smt_message (parser, 2, "found %u symbols", parser->symbols);
2871 smt_message (parser, 2, "generated %u nodes", parser->nodes->count);
2872
2873 count_assumptions_and_formulas (parser, top);
2874
2875 smt_message (
2876 parser, 1, "found %d assumptions", parser->assumptions.nparsed);
2877
2878 smt_message (parser, 1, "found %d formulas", parser->formulas.nparsed);
2879
2880 set_last_occurrence_of_symbols (parser, top);
2881
2882 err = translate_benchmark (parser, top, res);
2883 recursively_delete_smt_node (parser, top);
2884
2885 if (err)
2886 {
2887 assert (parser->error);
2888 return parser->error;
2889 }
2890
2891 smt_message (parser, 2, "found %u constants", parser->constants);
2892
2893 return 0; /* DONE */
2894 }
2895
2896 if (token == BTOR_SMTOK_ERR)
2897 {
2898 assert (parser->error);
2899 return parser->error;
2900 }
2901
2902 if (token == BTOR_SMTOK_EOF) return perr_smt (parser, "unexpected EOF");
2903
2904 if (BTOR_EMPTY_STACK (parser->heads))
2905 return perr_smt (parser, "expected '('");
2906
2907 assert (parser->symbol);
2908 BTOR_PUSH_STACK (parser->stack, leaf (parser->symbol));
2909
2910 goto NEXT_TOKEN;
2911 }
2912
2913 static const char *
parse_smt_parser(BtorSMTParser * parser,BtorCharStack * prefix,FILE * infile,const char * infile_name,FILE * outfile,BtorParseResult * res)2914 parse_smt_parser (BtorSMTParser *parser,
2915 BtorCharStack *prefix,
2916 FILE *infile,
2917 const char *infile_name,
2918 FILE *outfile,
2919 BtorParseResult *res)
2920 {
2921 (void) parse (parser, prefix, infile, infile_name, outfile, res);
2922 release_smt_internals (parser);
2923 return parser->error;
2924 }
2925
2926 static BtorParserAPI parsesmt_parser_api = {
2927 (BtorInitParser) new_smt_parser,
2928 (BtorResetParser) delete_smt_parser,
2929 (BtorParse) parse_smt_parser,
2930 };
2931
2932 const BtorParserAPI *
btor_parsesmt_parser_api()2933 btor_parsesmt_parser_api ()
2934 {
2935 return &parsesmt_parser_api;
2936 }
2937