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 <assert.h>
10 #include <ctype.h>
11 #include <inttypes.h>
12 #include <stdarg.h>
13 #include <stdio.h>
14 #include <stdlib.h>
15 #include <string.h>
16 #include <unistd.h>
17
18 #include "boolector.h"
19 #include "btoropt.h"
20 #include "utils/btorhash.h"
21 #include "utils/btorhashptr.h"
22 #include "utils/btormem.h"
23 #include "utils/btorstack.h"
24 #include "utils/btorutil.h"
25
26 #ifdef BTOR_HAVE_SIGNALS
27 #include <signal.h>
28 #endif
29
30 /*------------------------------------------------------------------------*/
31
32 #define BTORUNT_USAGE \
33 "usage: btoruntrace [ <option> ... ] [ <trace> ]\n" \
34 "\n" \
35 "where <option> is one of the following:\n" \
36 "\n" \
37 " -v, --verbosity increase verbosity\n" \
38 " -e, --exit-on-abort exit on boolector abort\n" \
39 " -s, --skip skip checks for return values\n" \
40 " -i, --ignore-sat-result do not exit on mismatching sat result\n" \
41 " -b <btoropt> <val> set boolector option <btoropt> to <val>\n" \
42 " (Note: overrides trace opt settings!)\n" \
43 " -d, --dump-stdout dump to stdout " \
44 "(default: dump to temp file at\n" \
45 " /tmp/<trace-basename>.(btor|smt2)\n"
46
47 /*------------------------------------------------------------------------*/
48
49 void boolector_chkclone (Btor *);
50 void boolector_set_btor_id (Btor *, BoolectorNode *, int32_t);
51 void boolector_get_btor_msg (Btor *);
52 void boolector_print_value_smt2 (Btor *, BoolectorNode *, char *, FILE *);
53 void boolector_var_mark_bool (Btor *, BoolectorNode *);
54
55 /*------------------------------------------------------------------------*/
56 typedef struct BtorUNT BtorUNT;
57
58 struct BtorUNTBtorOpt
59 {
60 BtorOption kind;
61 char *name;
62 uint32_t val;
63 };
64
65 typedef struct BtorUNTBtorOpt BtorUNTBtorOpt;
66
67 BTOR_DECLARE_STACK (BtorUNTBtorOptPtr, BtorUNTBtorOpt *);
68
69 struct BtorUNT
70 {
71 BtorMemMgr *mm;
72 BtorUNTBtorOptPtrStack cl_btor_opts;
73 BtorPtrHashTable *btor_opts;
74 uint32_t verbosity;
75 bool exit_on_abort;
76 bool skip;
77 bool ignore_sat;
78 bool dump_stdout;
79 uint32_t line;
80 char *filename;
81 };
82
83 /*------------------------------------------------------------------------*/
84
85 static BtorUNT *
btorunt_new(void)86 btorunt_new (void)
87 {
88 BtorUNT *res;
89 BtorMemMgr *mm;
90 BtorUNTBtorOpt *opt;
91 BtorOption o;
92 Btor *tmpbtor;
93 char *lng;
94 uint32_t dflt;
95
96 mm = btor_mem_mgr_new ();
97 BTOR_CNEW (mm, res);
98 res->mm = mm;
99 BTOR_INIT_STACK (mm, res->cl_btor_opts);
100 res->btor_opts = btor_hashptr_table_new (mm, btor_hash_str, btor_compare_str);
101
102 /* add end of options marker */
103 BTOR_NEW (res->mm, opt);
104 opt->kind = BTOR_OPT_NUM_OPTS;
105 opt->name = btor_mem_strdup (res->mm, BTOR_OPT_NUM_OPTS_STR);
106 opt->val = 0;
107 btor_hashptr_table_add (res->btor_opts, BTOR_OPT_NUM_OPTS_STR)->data.as_ptr =
108 opt;
109
110 /* add boolector options */
111 tmpbtor = boolector_new ();
112 for (o = boolector_first_opt (tmpbtor), lng = 0;
113 boolector_has_opt (tmpbtor, o);
114 o = boolector_next_opt (tmpbtor, o))
115 {
116 lng = (char *) boolector_get_opt_lng (tmpbtor, o);
117 dflt = boolector_get_opt_dflt (tmpbtor, o);
118 BTOR_NEW (res->mm, opt);
119 opt->kind = o;
120 opt->name = btor_mem_strdup (res->mm, lng);
121 opt->val = dflt;
122 btor_hashptr_table_add (res->btor_opts, lng)->data.as_ptr = opt;
123 }
124 res->line = 1;
125 boolector_delete(tmpbtor);
126 return res;
127 }
128
129 static void
btorunt_delete(BtorUNT * unt)130 btorunt_delete (BtorUNT *unt)
131 {
132 uint32_t i;
133 BtorUNTBtorOpt *o;
134 BtorPtrHashTableIterator it;
135 BtorMemMgr *mm;
136
137 mm = unt->mm;
138
139 for (i = 0; i < BTOR_COUNT_STACK (unt->cl_btor_opts); i++)
140 {
141 o = BTOR_PEEK_STACK (unt->cl_btor_opts, i);
142 assert (o);
143 btor_mem_freestr (mm, o->name);
144 BTOR_DELETE (mm, o);
145 }
146 BTOR_RELEASE_STACK (unt->cl_btor_opts);
147
148 btor_iter_hashptr_init (&it, unt->btor_opts);
149 while (btor_iter_hashptr_has_next (&it))
150 {
151 o = btor_iter_hashptr_next_data (&it)->as_ptr;
152 assert (o);
153 btor_mem_freestr (mm, o->name);
154 BTOR_DELETE (mm, o);
155 }
156 btor_hashptr_table_delete (unt->btor_opts);
157
158 BTOR_DELETE (mm, unt);
159 btor_mem_mgr_delete (mm);
160 }
161
162 /*------------------------------------------------------------------------*/
163
164 static BtorUNT *g_btorunt;
165
166 /*------------------------------------------------------------------------*/
167
168 static void
btorunt_error(const char * msg,...)169 btorunt_error (const char *msg, ...)
170 {
171 va_list list;
172 fputs ("btoruntrace: ", stderr);
173 va_start (list, msg);
174 vfprintf (stderr, msg, list);
175 va_end (list);
176 fputc ('\n', stderr);
177 fflush (stderr);
178 exit (1);
179 }
180
181 static void
btorunt_parse_error(const char * msg,...)182 btorunt_parse_error (const char *msg, ...)
183 {
184 va_list list;
185 fprintf (stderr,
186 "btoruntrace: parse error in '%s' line %d: ",
187 g_btorunt->filename,
188 g_btorunt->line);
189 va_start (list, msg);
190 vfprintf (stderr, msg, list);
191 va_end (list);
192 fputc ('\n', stderr);
193 fflush (stderr);
194 exit (1);
195 }
196
197 #define BTORUNT_LOG(fmt, args...) \
198 do \
199 { \
200 if (g_btorunt->verbosity) \
201 { \
202 printf ("[btorunt] "); \
203 printf (fmt, ##args); \
204 printf ("\n"); \
205 } \
206 } while (0)
207
208 /*------------------------------------------------------------------------*/
209
210 static bool
btorunt_has_cl_btor_opt(BtorUNT * unt,BtorOption opt)211 btorunt_has_cl_btor_opt (BtorUNT *unt, BtorOption opt)
212 {
213 assert (unt);
214
215 uint32_t i;
216 BtorUNTBtorOpt *o;
217
218 for (i = 0; i < BTOR_COUNT_STACK (unt->cl_btor_opts); i++)
219 {
220 o = BTOR_PEEK_STACK (unt->cl_btor_opts, i);
221 if (o->kind == opt) return true;
222 }
223 return false;
224 }
225
226 static BtorUNTBtorOpt *
btorunt_get_btor_opt(BtorUNT * unt,const char * opt)227 btorunt_get_btor_opt (BtorUNT *unt, const char *opt)
228 {
229 assert (unt);
230 assert (opt);
231 BtorPtrHashBucket *b;
232 b = btor_hashptr_table_get (unt->btor_opts, (void *) opt);
233 return !b ? NULL : b->data.as_ptr;
234 }
235
236 static bool
is_num_str(const char * str)237 is_num_str (const char *str)
238 {
239 const char *p;
240 int32_t ch;
241 if (*(p = str) == '-') p++;
242 if (!isdigit ((int32_t) *p++)) return false;
243 while (isdigit (ch = *p)) p++;
244 return ch == 0;
245 }
246
247 static void
parse_check_last_arg(char * op)248 parse_check_last_arg (char *op)
249 {
250 if (strtok (0, " "))
251 {
252 btorunt_parse_error ("too many arguments for '%s'", op);
253 }
254 }
255
256 static bool
parse_bool_arg(char * op)257 parse_bool_arg (char *op)
258 {
259 const char *tok;
260 if (!(tok = strtok (0, " "))
261 || (strcmp (tok, "true") && strcmp (tok, "false")))
262 {
263 btorunt_parse_error ("expected Boolean argument for '%s'", op);
264 }
265 assert (tok);
266 return !strcmp (tok, "true") ? true : false;
267 }
268
269 static int32_t
parse_int_arg(char * op)270 parse_int_arg (char *op)
271 {
272 const char *tok;
273 if (!(tok = strtok (0, " ")) || !is_num_str (tok))
274 {
275 btorunt_parse_error ("expected integer argument for '%s'", op);
276 }
277 assert (tok);
278 return atoi (tok);
279 }
280
281 static uint32_t
parse_uint_arg(char * op)282 parse_uint_arg (char *op)
283 {
284 const char *tok;
285 if (!(tok = strtok (0, " ")) || !is_num_str (tok) || tok[0] == '-')
286 {
287 btorunt_parse_error ("expected unsigned integer argument for '%s'", op);
288 }
289 assert (tok);
290 return strtoul (tok, 0, 10);
291 }
292
293 static char *
parse_str_arg(char * op)294 parse_str_arg (char *op)
295 {
296 char *tok;
297 if (!(tok = strtok (0, " ")))
298 {
299 btorunt_parse_error ("expected string argument for '%s'", op);
300 }
301 return tok;
302 }
303
304 /* Parse
305 * <enum> <long-opt> <value>
306 * or
307 * <long-opt> <value>
308 */
309 static BtorOption
parse_opt(char ** arg_str)310 parse_opt (char **arg_str)
311 {
312 BtorUNTBtorOpt *unt_opt;
313 BtorOption opt = BTOR_OPT_NUM_OPTS;
314 char *tok;
315
316 if (!(tok = strtok (0, " ")))
317 {
318 btorunt_parse_error ("expected long option name");
319 }
320
321 if (is_num_str (tok) && tok[0] != '-')
322 {
323 opt = strtoul (tok, 0, 10);
324 tok = strtok (0, " ");
325 }
326
327 unt_opt = btorunt_get_btor_opt (g_btorunt, tok);
328 if (!unt_opt)
329 btorunt_parse_error ("unknown option '%s'", tok);
330
331 if (arg_str) *arg_str = tok;
332 if (opt == BTOR_OPT_NUM_OPTS)
333 {
334 opt = unt_opt->kind;
335 }
336 else if (opt != unt_opt->kind)
337 {
338 btorunt_parse_error (
339 "expected enum value '%u' for long option '%s', got '%u'",
340 unt_opt->kind,
341 tok,
342 opt);
343 }
344
345 return opt;
346 }
347
348 #define PARSE_ARGS0(op) parse_check_last_arg (op);
349
350 #define PARSE_ARGS1(op, type1) \
351 arg1_##type1 = parse_##type1##_arg (op); \
352 parse_check_last_arg (op);
353
354 #define PARSE_ARGS2(op, type1, type2) \
355 arg1_##type1 = parse_##type1##_arg (op); \
356 arg2_##type2 = parse_##type2##_arg (op); \
357 parse_check_last_arg (op);
358
359 #define PARSE_ARGS3(op, type1, type2, type3) \
360 arg1_##type1 = parse_##type1##_arg (op); \
361 arg2_##type2 = parse_##type2##_arg (op); \
362 arg3_##type3 = parse_##type3##_arg (op); \
363 parse_check_last_arg (op);
364
365 /*--------------------------------------------------------------------------*/
366
367 static void *
hmap_get(BtorPtrHashTable * hmap,char * key)368 hmap_get (BtorPtrHashTable *hmap, char *key)
369 {
370 assert (hmap);
371 assert (key);
372
373 BtorPtrHashBucket *bucket;
374
375 bucket = btor_hashptr_table_get (hmap, key);
376 if (!bucket) btorunt_error ("'%s' is not hashed", key);
377 assert (bucket);
378 return bucket->data.as_ptr;
379 }
380
381 static BoolectorSort
get_sort(BtorPtrHashTable * hmap,char * key)382 get_sort (BtorPtrHashTable *hmap, char *key)
383 {
384 return (BoolectorSort) (size_t) hmap_get (hmap, key);
385 }
386
387 static void
hmap_add(BtorPtrHashTable * hmap,char * key,void * value)388 hmap_add (BtorPtrHashTable *hmap, char *key, void *value)
389 {
390 assert (hmap);
391 assert (key);
392
393 BtorPtrHashBucket *bucket;
394
395 bucket = btor_hashptr_table_get (hmap, key);
396 if (!bucket)
397 {
398 char *key_cp;
399 BTOR_NEWN (hmap->mm, key_cp, (strlen (key) + 1));
400 strcpy (key_cp, key);
401 bucket = btor_hashptr_table_add (hmap, key_cp);
402 }
403 assert (bucket);
404 bucket->data.as_ptr = value;
405 }
406
407 static void
hmap_clear(BtorPtrHashTable * hmap)408 hmap_clear (BtorPtrHashTable *hmap)
409 {
410 assert (hmap);
411
412 BtorPtrHashBucket *bucket;
413
414 for (bucket = hmap->first; bucket; bucket = hmap->first)
415 {
416 char *key = (char *) bucket->key;
417 btor_hashptr_table_remove (hmap, key, NULL, NULL);
418 BTOR_DELETEN (hmap->mm, key, (strlen (key) + 1));
419 }
420 }
421
422 /*------------------------------------------------------------------------*/
423
424 enum
425 {
426 RET_NONE,
427 RET_VOIDPTR,
428 RET_NODEPTR,
429 RET_SORTPTR,
430 RET_INT,
431 RET_UINT,
432 RET_CHARPTR,
433 RET_ARRASS,
434 RET_BOOL,
435 RET_SKIP
436 };
437
438 BTOR_DECLARE_STACK (BoolectorSort, BoolectorSort);
439
440 #define BTOR_STR_LEN 40
441
442 static bool
check_return_str(char * expected,char * got)443 check_return_str (char *expected, char *got)
444 {
445 size_t pos1 = 0, pos2 = 0;
446 for (; pos1 < strlen (expected) && expected[pos1] != '@'; pos1++)
447 ;
448 for (; pos2 < strlen (got) && got[pos2] != '@'; pos2++)
449 ;
450
451 if (pos1 != pos2) return false;
452
453 return strncmp (expected, got, pos1) == 0;
454 }
455
456 static void
parse(FILE * file)457 parse (FILE *file)
458 {
459 size_t i;
460 int32_t ch;
461 bool delete;
462 uint32_t len, buffer_len, val;
463 char *buffer, *tok, *basename;
464 BoolectorNode **tmp;
465 BtorPtrHashTable *hmap;
466 BtorOption opt;
467 Btor *btor;
468
469 int32_t exp_ret; /* expected return value */
470 bool ret_bool; /* actual return value bool */
471 int32_t ret_int; /* actual return value int */
472 uint32_t ret_uint; /* actual return value unsigned int */
473 char *ret_str; /* actual return value string */
474 void *ret_ptr; /* actual return value string */
475 char **res1_pptr, **res2_pptr; /* result pointer */
476
477 char *btor_str; /* btor pointer string */
478 char *exp_str; /* expression string (pointer) */
479 int32_t arg1_int, arg2_int, arg3_int;
480 uint32_t arg1_uint, arg2_uint, arg3_uint;
481 char *arg1_str, *arg2_str, *arg3_str;
482 char check_buf[128];
483 BtorIntStack arg_int;
484 BtorCharPtrStack arg_str;
485 BoolectorSortStack sort_stack;
486
487 Btor *tmpbtor;
488 FILE *outfile;
489 int32_t flen, pres, pstat;
490 char *outfilename, *emsg;
491
492 BTORUNT_LOG ("parsing %s", g_btorunt->filename);
493
494 delete = true;
495
496 exp_ret = RET_NONE;
497 ret_int = 0;
498 ret_uint = 0;
499 ret_ptr = 0;
500 ret_str = 0;
501 ret_bool = false;
502 len = 0;
503 buffer_len = 256;
504 arg2_int = 0;
505 btor = 0;
506
507 hmap = btor_hashptr_table_new (
508 g_btorunt->mm, (BtorHashPtr) btor_hash_str, (BtorCmpPtr) strcmp);
509
510 BTOR_CNEWN (g_btorunt->mm, buffer, buffer_len);
511
512 BTOR_INIT_STACK (g_btorunt->mm, arg_int);
513 BTOR_INIT_STACK (g_btorunt->mm, arg_str);
514 BTOR_INIT_STACK (g_btorunt->mm, sort_stack);
515
516 BTOR_CNEWN (g_btorunt->mm, btor_str, BTOR_STR_LEN);
517
518 NEXT:
519 BTOR_RESET_STACK (arg_int);
520 BTOR_RESET_STACK (arg_str);
521 BTOR_RESET_STACK (sort_stack);
522 ch = getc (file);
523 if (ch == EOF) goto DONE;
524 if (ch == '\r') goto NEXT;
525 if (ch != '\n')
526 {
527 if (len + 1 >= buffer_len)
528 {
529 BTOR_REALLOC (g_btorunt->mm, buffer, buffer_len, buffer_len * 2);
530 buffer_len *= 2;
531 BTORUNT_LOG ("buffer resized");
532 }
533 buffer[len++] = ch;
534 buffer[len] = 0;
535 goto NEXT;
536 }
537 BTORUNT_LOG (" %d: %s", g_btorunt->line, buffer);
538
539 /* NOTE take care of c function parameter evaluation order with more
540 * than 1 argument */
541 if (!(tok = strtok (buffer, " ")))
542 btorunt_parse_error ("empty line");
543 else if (exp_ret)
544 {
545 if (!strcmp (tok, "return"))
546 {
547 if (exp_ret == RET_VOIDPTR)
548 {
549 exp_str = parse_str_arg ("return");
550 parse_check_last_arg ("return");
551 hmap_add (hmap, exp_str, ret_ptr);
552 }
553 else if (exp_ret == RET_NODEPTR)
554 {
555 exp_str = parse_str_arg ("return");
556 parse_check_last_arg ("return");
557 if (!g_btorunt->skip)
558 {
559 bool is_inv = ((uintptr_t) 1 & (uintptr_t) ret_ptr) != 0;
560 int32_t id = boolector_get_node_id (btor, ret_ptr);
561 snprintf (check_buf, 128, "n%d@%p", is_inv ? -id : id, btor);
562 if (!check_return_str (exp_str, check_buf))
563 {
564 btorunt_error (
565 "Boolector under test changed. "
566 "expected node %s but got %s",
567 exp_str,
568 check_buf);
569 }
570 }
571 hmap_add (hmap, exp_str, ret_ptr);
572 }
573 else if (exp_ret == RET_SORTPTR)
574 {
575 exp_str = parse_str_arg ("return");
576 parse_check_last_arg ("return");
577 if (!g_btorunt->skip)
578 {
579 snprintf (check_buf, 128, "s%" PRId64 "@%p", (int64_t) ret_ptr, btor);
580 if (!check_return_str (exp_str, check_buf))
581 {
582 btorunt_error (
583 "Boolector under test changed. "
584 "expected node %s but got %s",
585 exp_str,
586 check_buf);
587 }
588 }
589 hmap_add (hmap, exp_str, ret_ptr);
590 }
591 else if (exp_ret == RET_BOOL)
592 {
593 bool exp_bool = parse_bool_arg ("return");
594 if (exp_bool != ret_bool && !g_btorunt->skip)
595 btorunt_error ("expected return value %s but got %s",
596 exp_bool ? "true" : "false",
597 ret_bool ? "true" : "false");
598 }
599 else if (exp_ret == RET_INT)
600 {
601 int32_t exp_int = parse_int_arg ("return");
602 parse_check_last_arg ("return");
603 if (exp_int != ret_int && !g_btorunt->skip)
604 btorunt_error (
605 "expected return value %d but got %d", exp_int, ret_int);
606 }
607 else if (exp_ret == RET_UINT)
608 {
609 uint32_t exp_uint = parse_uint_arg ("return");
610 parse_check_last_arg ("return");
611 if (exp_uint != ret_uint && !g_btorunt->skip)
612 btorunt_error (
613 "expected return value %d but got %d", exp_uint, ret_uint);
614 }
615 else if (exp_ret == RET_CHARPTR)
616 {
617 exp_str = parse_str_arg ("return");
618 parse_check_last_arg ("return");
619 if (strcmp (exp_str, ret_str) && !g_btorunt->skip)
620 btorunt_error (
621 "expected return string %s but got %s", exp_str, ret_str);
622 }
623 else if (exp_ret == RET_ARRASS)
624 {
625 PARSE_ARGS3 (tok, str, str, int);
626 if (ret_int)
627 {
628 hmap_add (hmap, arg1_str, res1_pptr);
629 hmap_add (hmap, arg2_str, res2_pptr);
630 }
631 if (arg3_int != ret_int && !g_btorunt->skip)
632 btorunt_error (
633 "expected return value %d but got %d", arg3_int, ret_int);
634 }
635 else
636 assert (exp_ret == RET_SKIP);
637 }
638 else
639 {
640 btorunt_parse_error ("return expected");
641 }
642 exp_ret = RET_NONE;
643 }
644 else
645 {
646 /* get btor object for all functions except for 'new' and 'get_btor' */
647 if (strcmp (tok, "new") && strcmp (tok, "get_btor"))
648 {
649 exp_str = parse_str_arg (tok);
650 snprintf (btor_str, BTOR_STR_LEN, "%s", exp_str);
651 btor = hmap_get (hmap, btor_str);
652 assert (btor);
653 }
654 if (!strcmp (tok, "chkclone"))
655 {
656 PARSE_ARGS0 (tok);
657 boolector_chkclone (btor);
658 }
659 else if (!strcmp (tok, "new"))
660 {
661 PARSE_ARGS0 (tok);
662 btor = boolector_new ();
663 /* set btor options given via CL
664 * (Note: overrules opt values set via trace file!) */
665 for (i = 0; i < BTOR_COUNT_STACK (g_btorunt->cl_btor_opts); i++)
666 {
667 boolector_set_opt (btor,
668 BTOR_PEEK_STACK (g_btorunt->cl_btor_opts, i)->kind,
669 BTOR_PEEK_STACK (g_btorunt->cl_btor_opts, i)->val);
670 BTORUNT_LOG (" *** set boolector option '%s' to '%u' (via CL)",
671 BTOR_PEEK_STACK (g_btorunt->cl_btor_opts, i)->name,
672 BTOR_PEEK_STACK (g_btorunt->cl_btor_opts, i)->val);
673 }
674 exp_ret = RET_VOIDPTR;
675 ret_ptr = btor;
676 }
677 else if (!strcmp (tok, "clone"))
678 {
679 exp_ret = RET_VOIDPTR;
680 ret_ptr = boolector_clone (btor);
681 }
682 else if (!strcmp (tok, "match_node_by_id"))
683 {
684 PARSE_ARGS1 (tok, int);
685 ret_ptr = boolector_match_node_by_id (btor, arg1_int);
686 exp_ret = RET_NODEPTR;
687 }
688 else if (!strcmp (tok, "match_node_by_symbol"))
689 {
690 PARSE_ARGS1 (tok, str);
691 ret_ptr = boolector_match_node_by_symbol (btor, arg1_str);
692 exp_ret = RET_NODEPTR;
693 }
694 else if (!strcmp (tok, "match_node"))
695 {
696 PARSE_ARGS1 (tok, str);
697 ret_ptr = boolector_match_node (btor, hmap_get (hmap, arg1_str));
698 exp_ret = RET_NODEPTR;
699 }
700 else if (!strcmp (tok, "delete"))
701 {
702 PARSE_ARGS0 (tok);
703 boolector_delete (btor);
704 delete = false;
705 }
706 else if (!strcmp (tok, "set_btor_id"))
707 {
708 PARSE_ARGS2 (tok, str, int);
709 boolector_set_btor_id (btor, hmap_get (hmap, arg1_str), arg2_int);
710 }
711 else if (!strcmp (tok, "get_btor_msg"))
712 {
713 PARSE_ARGS0 (tok);
714 boolector_get_btor_msg (btor);
715 }
716 else if (!strcmp (tok, "set_msg_prefix"))
717 {
718 PARSE_ARGS1 (tok, str);
719 boolector_set_msg_prefix (btor, arg1_str);
720 }
721 else if (!strcmp (tok, "reset_time"))
722 {
723 PARSE_ARGS0 (tok);
724 boolector_reset_time (btor);
725 }
726 else if (!strcmp (tok, "reset_stats"))
727 {
728 PARSE_ARGS0 (tok);
729 boolector_reset_stats (btor);
730 }
731 else if (!strcmp (tok, "print_stats"))
732 {
733 PARSE_ARGS0 (tok);
734 boolector_print_stats (btor);
735 }
736 else if (!strcmp (tok, "assert"))
737 {
738 PARSE_ARGS1 (tok, str);
739 boolector_assert (btor, hmap_get (hmap, arg1_str));
740 }
741 else if (!strcmp (tok, "assume"))
742 {
743 PARSE_ARGS1 (tok, str);
744 boolector_assume (btor, hmap_get (hmap, arg1_str));
745 }
746 else if (!strcmp (tok, "reset_assumptions"))
747 {
748 PARSE_ARGS0 (tok);
749 boolector_reset_assumptions (btor);
750 }
751 else if (!strcmp (tok, "fixate_assumptions"))
752 {
753 PARSE_ARGS0 (tok);
754 boolector_fixate_assumptions (btor);
755 }
756 else if (!strcmp (tok, "failed"))
757 {
758 PARSE_ARGS1 (tok, str);
759 ret_bool = boolector_failed (btor, hmap_get (hmap, arg1_str));
760 exp_ret = RET_BOOL;
761 }
762 else if (!strcmp (tok, "sat"))
763 {
764 PARSE_ARGS0 (tok);
765 ret_int = boolector_sat (btor);
766 exp_ret = g_btorunt->ignore_sat ? RET_SKIP : RET_INT;
767 }
768 else if (!strcmp (tok, "limited_sat"))
769 {
770 PARSE_ARGS2 (tok, int, int);
771 ret_int = boolector_limited_sat (btor, arg1_int, arg2_int);
772 exp_ret = g_btorunt->ignore_sat ? RET_SKIP : RET_INT;
773 }
774 else if (!strcmp (tok, "simplify"))
775 {
776 PARSE_ARGS0 (tok);
777 ret_int = boolector_simplify (btor);
778 exp_ret = RET_INT;
779 }
780 else if (!strcmp (tok, "set_sat_solver"))
781 {
782 PARSE_ARGS1 (tok, str);
783 boolector_set_sat_solver (btor, arg1_str);
784 }
785 else if (!strcmp (tok, "set_opt"))
786 {
787 opt = parse_opt (&arg1_str);
788 val = parse_uint_arg (tok);
789 parse_check_last_arg (tok);
790 if (!btorunt_has_cl_btor_opt (g_btorunt, opt))
791 {
792 boolector_set_opt (btor, opt, val);
793 BTORUNT_LOG (" set boolector option '%s' to '%u' (via trace)",
794 arg1_str,
795 val);
796 }
797 }
798 else if (!strcmp (tok, "get_opt"))
799 {
800 if (!g_btorunt->skip)
801 {
802 opt = parse_opt (0);
803 parse_check_last_arg (tok);
804 ret_uint = boolector_get_opt (btor, opt);
805 exp_ret = RET_UINT;
806 }
807 else
808 {
809 exp_ret = RET_SKIP;
810 }
811 }
812 else if (!strcmp (tok, "get_opt_min"))
813 {
814 if (!g_btorunt->skip)
815 {
816 opt = parse_opt (0);
817 parse_check_last_arg (tok);
818 ret_uint = boolector_get_opt_min (btor, opt);
819 exp_ret = RET_UINT;
820 }
821 else
822 {
823 exp_ret = RET_SKIP;
824 }
825 }
826 else if (!strcmp (tok, "get_opt_max"))
827 {
828 if (!g_btorunt->skip)
829 {
830 opt = parse_opt (0);
831 parse_check_last_arg (tok);
832 ret_uint = boolector_get_opt_max (btor, opt);
833 exp_ret = RET_UINT;
834 }
835 else
836 {
837 exp_ret = RET_SKIP;
838 }
839 }
840 else if (!strcmp (tok, "get_opt_dflt"))
841 {
842 if (!g_btorunt->skip)
843 {
844 opt = parse_opt (0);
845 parse_check_last_arg (tok);
846 ret_uint = boolector_get_opt_dflt (btor, opt);
847 exp_ret = RET_UINT;
848 }
849 else
850 {
851 exp_ret = RET_SKIP;
852 }
853 }
854 else if (!strcmp (tok, "get_opt_shrt"))
855 {
856 if (!g_btorunt->skip)
857 {
858 opt = parse_opt (0);
859 parse_check_last_arg (tok);
860 ret_str = (void *) boolector_get_opt_shrt (btor, opt);
861 exp_ret = RET_UINT;
862 }
863 else
864 {
865 exp_ret = RET_SKIP;
866 }
867 }
868 else if (!strcmp (tok, "get_opt_lng"))
869 {
870 if (!g_btorunt->skip)
871 {
872 opt = parse_opt (0);
873 parse_check_last_arg (tok);
874 ret_str = (void *) boolector_get_opt_lng (btor, opt);
875 exp_ret = RET_CHARPTR;
876 }
877 else
878 {
879 exp_ret = RET_SKIP;
880 }
881 }
882 else if (!strcmp (tok, "get_opt_desc"))
883 {
884 if (!g_btorunt->skip)
885 {
886 opt = parse_opt (0);
887 parse_check_last_arg (tok);
888 ret_str = (void *) boolector_get_opt_desc (btor, opt);
889 exp_ret = RET_CHARPTR;
890 }
891 else
892 {
893 exp_ret = RET_SKIP;
894 }
895 }
896 else if (!strcmp (tok, "has_opt"))
897 {
898 if (!g_btorunt->skip)
899 {
900 opt = parse_opt (0);
901 parse_check_last_arg (tok);
902 ret_bool = boolector_has_opt (btor, opt);
903 exp_ret = RET_BOOL;
904 }
905 else
906 {
907 exp_ret = RET_SKIP;
908 }
909 }
910 else if (!strcmp (tok, "first_opt"))
911 {
912 if (!g_btorunt->skip)
913 {
914 PARSE_ARGS0 (tok);
915 ret_int = boolector_first_opt (btor);
916 exp_ret = RET_INT;
917 }
918 else
919 {
920 exp_ret = RET_SKIP;
921 }
922 }
923 else if (!strcmp (tok, "next_opt"))
924 {
925 if (!g_btorunt->skip)
926 {
927 opt = parse_opt (0);
928 parse_check_last_arg (tok);
929 ret_int = boolector_next_opt (btor, opt);
930 exp_ret = RET_INT;
931 }
932 else
933 {
934 exp_ret = RET_SKIP;
935 }
936 }
937 else if (!strcmp (tok, "copy"))
938 {
939 PARSE_ARGS1 (tok, str);
940 ret_ptr = boolector_copy (btor, hmap_get (hmap, arg1_str));
941 exp_ret = RET_NODEPTR;
942 }
943 else if (!strcmp (tok, "release"))
944 {
945 PARSE_ARGS1 (tok, str);
946 boolector_release (btor, hmap_get (hmap, arg1_str));
947 }
948 else if (!strcmp (tok, "release_all"))
949 {
950 PARSE_ARGS0 (tok);
951 boolector_release_all (btor);
952 }
953 else if (!strcmp (tok, "is_bv_const_zero"))
954 {
955 PARSE_ARGS1 (tok, str);
956 if (!g_btorunt->skip)
957 {
958 ret_bool = boolector_is_bv_const_zero (btor, hmap_get (hmap, arg1_str));
959 exp_ret = RET_BOOL;
960 }
961 else
962 exp_ret = RET_SKIP;
963 }
964 else if (!strcmp (tok, "is_bv_const_one"))
965 {
966 PARSE_ARGS1 (tok, str);
967 if (!g_btorunt->skip)
968 {
969 ret_bool = boolector_is_bv_const_one (btor, hmap_get (hmap, arg1_str));
970 exp_ret = RET_BOOL;
971 }
972 else
973 exp_ret = RET_SKIP;
974 }
975 else if (!strcmp (tok, "is_bv_const_ones"))
976 {
977 PARSE_ARGS1 (tok, str);
978 if (!g_btorunt->skip)
979 {
980 ret_bool = boolector_is_bv_const_ones (btor, hmap_get (hmap, arg1_str));
981 exp_ret = RET_BOOL;
982 }
983 else
984 exp_ret = RET_SKIP;
985 }
986 else if (!strcmp (tok, "is_bv_const_min_signed"))
987 {
988 PARSE_ARGS1 (tok, str);
989 if (!g_btorunt->skip)
990 {
991 ret_bool =
992 boolector_is_bv_const_min_signed (btor, hmap_get (hmap, arg1_str));
993 exp_ret = RET_BOOL;
994 }
995 else
996 exp_ret = RET_SKIP;
997 }
998 else if (!strcmp (tok, "is_bv_const_max_signed"))
999 {
1000 PARSE_ARGS1 (tok, str);
1001 if (!g_btorunt->skip)
1002 {
1003 ret_bool =
1004 boolector_is_bv_const_max_signed (btor, hmap_get (hmap, arg1_str));
1005 exp_ret = RET_BOOL;
1006 }
1007 else
1008 exp_ret = RET_SKIP;
1009 }
1010 /* expressions */
1011 else if (!strcmp (tok, "const"))
1012 {
1013 PARSE_ARGS1 (tok, str);
1014 ret_ptr = boolector_const (btor, arg1_str);
1015 exp_ret = RET_NODEPTR;
1016 }
1017 else if (!strcmp (tok, "constd"))
1018 {
1019 PARSE_ARGS2 (tok, str, str);
1020 ret_ptr = boolector_constd (btor, get_sort (hmap, arg1_str), arg2_str);
1021 exp_ret = RET_NODEPTR;
1022 }
1023 else if (!strcmp (tok, "zero"))
1024 {
1025 PARSE_ARGS1 (tok, str);
1026 ret_ptr = boolector_zero (btor, get_sort (hmap, arg1_str));
1027 exp_ret = RET_NODEPTR;
1028 }
1029 else if (!strcmp (tok, "false"))
1030 {
1031 PARSE_ARGS0 (tok);
1032 ret_ptr = boolector_false (btor);
1033 exp_ret = RET_NODEPTR;
1034 }
1035 else if (!strcmp (tok, "ones"))
1036 {
1037 PARSE_ARGS1 (tok, str);
1038 ret_ptr = boolector_ones (btor, get_sort (hmap, arg1_str));
1039 exp_ret = RET_NODEPTR;
1040 }
1041 else if (!strcmp (tok, "true"))
1042 {
1043 PARSE_ARGS0 (tok);
1044 ret_ptr = boolector_true (btor);
1045 exp_ret = RET_NODEPTR;
1046 }
1047 else if (!strcmp (tok, "one"))
1048 {
1049 PARSE_ARGS1 (tok, str);
1050 ret_ptr = boolector_one (btor, get_sort (hmap, arg1_str));
1051 exp_ret = RET_NODEPTR;
1052 }
1053 else if (!strcmp (tok, "min_signed"))
1054 {
1055 PARSE_ARGS1 (tok, str);
1056 ret_ptr = boolector_min_signed (btor, get_sort (hmap, arg1_str));
1057 exp_ret = RET_NODEPTR;
1058 }
1059 else if (!strcmp (tok, "max_signed"))
1060 {
1061 PARSE_ARGS1 (tok, str);
1062 ret_ptr = boolector_max_signed (btor, get_sort (hmap, arg1_str));
1063 exp_ret = RET_NODEPTR;
1064 }
1065 else if (!strcmp (tok, "unsigned_int"))
1066 {
1067 PARSE_ARGS2 (tok, uint, str);
1068 ret_ptr =
1069 boolector_unsigned_int (btor, arg1_uint, get_sort (hmap, arg2_str));
1070 exp_ret = RET_NODEPTR;
1071 }
1072 else if (!strcmp (tok, "int"))
1073 {
1074 PARSE_ARGS2 (tok, int, str);
1075 ret_ptr = boolector_int (btor, arg1_int, get_sort (hmap, arg2_str));
1076 exp_ret = RET_NODEPTR;
1077 }
1078 else if (!strcmp (tok, "var"))
1079 {
1080 PARSE_ARGS2 (tok, str, str);
1081 arg2_str = !strcmp (arg2_str, "(null)") ? 0 : arg2_str;
1082 ret_ptr = boolector_var (btor, get_sort (hmap, arg1_str), arg2_str);
1083 exp_ret = RET_NODEPTR;
1084 }
1085 else if (!strcmp (tok, "array"))
1086 {
1087 PARSE_ARGS2 (tok, str, str);
1088 arg2_str = !strcmp (arg2_str, "(null)") ? 0 : arg2_str;
1089 ret_ptr = boolector_array (btor, get_sort (hmap, arg1_str), arg2_str);
1090 exp_ret = RET_NODEPTR;
1091 }
1092 else if (!strcmp (tok, "const_array"))
1093 {
1094 PARSE_ARGS2 (tok, str, str);
1095 ret_ptr = boolector_const_array (
1096 btor, get_sort (hmap, arg1_str), hmap_get (hmap, arg2_str));
1097 exp_ret = RET_NODEPTR;
1098 }
1099 else if (!strcmp (tok, "uf"))
1100 {
1101 PARSE_ARGS2 (tok, str, str);
1102 arg2_str = !strcmp (arg2_str, "(null)") ? 0 : arg2_str;
1103 ret_ptr = boolector_uf (btor, get_sort (hmap, arg1_str), arg2_str);
1104 exp_ret = RET_NODEPTR;
1105 }
1106 else if (!strcmp (tok, "not"))
1107 {
1108 PARSE_ARGS1 (tok, str);
1109 ret_ptr = boolector_not (btor, hmap_get (hmap, arg1_str));
1110 exp_ret = RET_NODEPTR;
1111 }
1112 else if (!strcmp (tok, "neg"))
1113 {
1114 PARSE_ARGS1 (tok, str);
1115 ret_ptr = boolector_neg (btor, hmap_get (hmap, arg1_str));
1116 exp_ret = RET_NODEPTR;
1117 }
1118 else if (!strcmp (tok, "redor"))
1119 {
1120 PARSE_ARGS1 (tok, str);
1121 ret_ptr = boolector_redor (btor, hmap_get (hmap, arg1_str));
1122 exp_ret = RET_NODEPTR;
1123 }
1124 else if (!strcmp (tok, "redxor"))
1125 {
1126 PARSE_ARGS1 (tok, str);
1127 ret_ptr = boolector_redxor (btor, hmap_get (hmap, arg1_str));
1128 exp_ret = RET_NODEPTR;
1129 }
1130 else if (!strcmp (tok, "redand"))
1131 {
1132 PARSE_ARGS1 (tok, str);
1133 ret_ptr = boolector_redand (btor, hmap_get (hmap, arg1_str));
1134 exp_ret = RET_NODEPTR;
1135 }
1136 else if (!strcmp (tok, "slice"))
1137 {
1138 PARSE_ARGS3 (tok, str, uint, uint);
1139 ret_ptr = boolector_slice (
1140 btor, hmap_get (hmap, arg1_str), arg2_uint, arg3_uint);
1141 exp_ret = RET_NODEPTR;
1142 }
1143 else if (!strcmp (tok, "uext"))
1144 {
1145 PARSE_ARGS2 (tok, str, uint);
1146 ret_ptr = boolector_uext (btor, hmap_get (hmap, arg1_str), arg2_uint);
1147 exp_ret = RET_NODEPTR;
1148 }
1149 else if (!strcmp (tok, "sext"))
1150 {
1151 PARSE_ARGS2 (tok, str, uint);
1152 ret_ptr = boolector_sext (btor, hmap_get (hmap, arg1_str), arg2_uint);
1153 exp_ret = RET_NODEPTR;
1154 }
1155 else if (!strcmp (tok, "implies"))
1156 {
1157 PARSE_ARGS2 (tok, str, str);
1158 ret_ptr = boolector_implies (
1159 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1160 exp_ret = RET_NODEPTR;
1161 }
1162 else if (!strcmp (tok, "iff"))
1163 {
1164 PARSE_ARGS2 (tok, str, str);
1165 ret_ptr = boolector_iff (
1166 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1167 exp_ret = RET_NODEPTR;
1168 }
1169 else if (!strcmp (tok, "xor"))
1170 {
1171 PARSE_ARGS2 (tok, str, str);
1172 ret_ptr = boolector_xor (
1173 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1174 exp_ret = RET_NODEPTR;
1175 }
1176 else if (!strcmp (tok, "xnor"))
1177 {
1178 PARSE_ARGS2 (tok, str, str);
1179 ret_ptr = boolector_xnor (
1180 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1181 exp_ret = RET_NODEPTR;
1182 }
1183 else if (!strcmp (tok, "and"))
1184 {
1185 PARSE_ARGS2 (tok, str, str);
1186 ret_ptr = boolector_and (
1187 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1188 exp_ret = RET_NODEPTR;
1189 }
1190 else if (!strcmp (tok, "nand"))
1191 {
1192 PARSE_ARGS2 (tok, str, str);
1193 ret_ptr = boolector_nand (
1194 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1195 exp_ret = RET_NODEPTR;
1196 }
1197 else if (!strcmp (tok, "or"))
1198 {
1199 PARSE_ARGS2 (tok, str, str);
1200 ret_ptr = boolector_or (
1201 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1202 exp_ret = RET_NODEPTR;
1203 }
1204 else if (!strcmp (tok, "nor"))
1205 {
1206 PARSE_ARGS2 (tok, str, str);
1207 ret_ptr = boolector_nor (
1208 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1209 exp_ret = RET_NODEPTR;
1210 }
1211 else if (!strcmp (tok, "eq"))
1212 {
1213 PARSE_ARGS2 (tok, str, str);
1214 ret_ptr = boolector_eq (
1215 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1216 exp_ret = RET_NODEPTR;
1217 }
1218 else if (!strcmp (tok, "ne"))
1219 {
1220 PARSE_ARGS2 (tok, str, str);
1221 ret_ptr = boolector_ne (
1222 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1223 exp_ret = RET_NODEPTR;
1224 }
1225 else if (!strcmp (tok, "add"))
1226 {
1227 PARSE_ARGS2 (tok, str, str);
1228 ret_ptr = boolector_add (
1229 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1230 exp_ret = RET_NODEPTR;
1231 }
1232 else if (!strcmp (tok, "uaddo"))
1233 {
1234 PARSE_ARGS2 (tok, str, str);
1235 ret_ptr = boolector_uaddo (
1236 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1237 exp_ret = RET_NODEPTR;
1238 }
1239 else if (!strcmp (tok, "saddo"))
1240 {
1241 PARSE_ARGS2 (tok, str, str);
1242 ret_ptr = boolector_saddo (
1243 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1244 exp_ret = RET_NODEPTR;
1245 }
1246 else if (!strcmp (tok, "mul"))
1247 {
1248 PARSE_ARGS2 (tok, str, str);
1249 ret_ptr = boolector_mul (
1250 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1251 exp_ret = RET_NODEPTR;
1252 }
1253 else if (!strcmp (tok, "umulo"))
1254 {
1255 PARSE_ARGS2 (tok, str, str);
1256 ret_ptr = boolector_umulo (
1257 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1258 exp_ret = RET_NODEPTR;
1259 }
1260 else if (!strcmp (tok, "smulo"))
1261 {
1262 PARSE_ARGS2 (tok, str, str);
1263 ret_ptr = boolector_smulo (
1264 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1265 exp_ret = RET_NODEPTR;
1266 }
1267 else if (!strcmp (tok, "ult"))
1268 {
1269 PARSE_ARGS2 (tok, str, str);
1270 ret_ptr = boolector_ult (
1271 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1272 exp_ret = RET_NODEPTR;
1273 }
1274 else if (!strcmp (tok, "slt"))
1275 {
1276 PARSE_ARGS2 (tok, str, str);
1277 ret_ptr = boolector_slt (
1278 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1279 exp_ret = RET_NODEPTR;
1280 }
1281 else if (!strcmp (tok, "ulte"))
1282 {
1283 PARSE_ARGS2 (tok, str, str);
1284 ret_ptr = boolector_ulte (
1285 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1286 exp_ret = RET_NODEPTR;
1287 }
1288 else if (!strcmp (tok, "slte"))
1289 {
1290 PARSE_ARGS2 (tok, str, str);
1291 ret_ptr = boolector_slte (
1292 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1293 exp_ret = RET_NODEPTR;
1294 }
1295 else if (!strcmp (tok, "ugt"))
1296 {
1297 PARSE_ARGS2 (tok, str, str);
1298 ret_ptr = boolector_ugt (
1299 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1300 exp_ret = RET_NODEPTR;
1301 }
1302 else if (!strcmp (tok, "sgt"))
1303 {
1304 PARSE_ARGS2 (tok, str, str);
1305 ret_ptr = boolector_sgt (
1306 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1307 exp_ret = RET_NODEPTR;
1308 }
1309 else if (!strcmp (tok, "ugte"))
1310 {
1311 PARSE_ARGS2 (tok, str, str);
1312 ret_ptr = boolector_ugte (
1313 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1314 exp_ret = RET_NODEPTR;
1315 }
1316 else if (!strcmp (tok, "sgte"))
1317 {
1318 PARSE_ARGS2 (tok, str, str);
1319 ret_ptr = boolector_sgte (
1320 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1321 exp_ret = RET_NODEPTR;
1322 }
1323 else if (!strcmp (tok, "sll"))
1324 {
1325 PARSE_ARGS2 (tok, str, str);
1326 ret_ptr = boolector_sll (
1327 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1328 exp_ret = RET_NODEPTR;
1329 }
1330 else if (!strcmp (tok, "srl"))
1331 {
1332 PARSE_ARGS2 (tok, str, str);
1333 ret_ptr = boolector_srl (
1334 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1335 exp_ret = RET_NODEPTR;
1336 }
1337 else if (!strcmp (tok, "sra"))
1338 {
1339 PARSE_ARGS2 (tok, str, str);
1340 ret_ptr = boolector_sra (
1341 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1342 exp_ret = RET_NODEPTR;
1343 }
1344 else if (!strcmp (tok, "rol"))
1345 {
1346 PARSE_ARGS2 (tok, str, str);
1347 ret_ptr = boolector_rol (
1348 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1349 exp_ret = RET_NODEPTR;
1350 }
1351 else if (!strcmp (tok, "roli"))
1352 {
1353 PARSE_ARGS2 (tok, str, int);
1354 ret_ptr = boolector_roli (btor, hmap_get (hmap, arg1_str), arg2_int);
1355 exp_ret = RET_VOIDPTR;
1356 }
1357 else if (!strcmp (tok, "ror"))
1358 {
1359 PARSE_ARGS2 (tok, str, str);
1360 ret_ptr = boolector_ror (
1361 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1362 exp_ret = RET_NODEPTR;
1363 }
1364 else if (!strcmp (tok, "rori"))
1365 {
1366 PARSE_ARGS2 (tok, str, int);
1367 ret_ptr = boolector_rori (btor, hmap_get (hmap, arg1_str), arg2_int);
1368 exp_ret = RET_VOIDPTR;
1369 }
1370 else if (!strcmp (tok, "sub"))
1371 {
1372 PARSE_ARGS2 (tok, str, str);
1373 ret_ptr = boolector_sub (
1374 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1375 exp_ret = RET_NODEPTR;
1376 }
1377 else if (!strcmp (tok, "usubo"))
1378 {
1379 PARSE_ARGS2 (tok, str, str);
1380 ret_ptr = boolector_usubo (
1381 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1382 exp_ret = RET_NODEPTR;
1383 }
1384 else if (!strcmp (tok, "ssubo"))
1385 {
1386 PARSE_ARGS2 (tok, str, str);
1387 ret_ptr = boolector_ssubo (
1388 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1389 exp_ret = RET_NODEPTR;
1390 }
1391 else if (!strcmp (tok, "udiv"))
1392 {
1393 PARSE_ARGS2 (tok, str, str);
1394 ret_ptr = boolector_udiv (
1395 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1396 exp_ret = RET_NODEPTR;
1397 }
1398 else if (!strcmp (tok, "sdiv"))
1399 {
1400 PARSE_ARGS2 (tok, str, str);
1401 ret_ptr = boolector_sdiv (
1402 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1403 exp_ret = RET_NODEPTR;
1404 }
1405 else if (!strcmp (tok, "sdivo"))
1406 {
1407 PARSE_ARGS2 (tok, str, str);
1408 ret_ptr = boolector_sdivo (
1409 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1410 exp_ret = RET_NODEPTR;
1411 }
1412 else if (!strcmp (tok, "urem"))
1413 {
1414 PARSE_ARGS2 (tok, str, str);
1415 ret_ptr = boolector_urem (
1416 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1417 exp_ret = RET_NODEPTR;
1418 }
1419 else if (!strcmp (tok, "srem"))
1420 {
1421 PARSE_ARGS2 (tok, str, str);
1422 ret_ptr = boolector_srem (
1423 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1424 exp_ret = RET_NODEPTR;
1425 }
1426 else if (!strcmp (tok, "smod"))
1427 {
1428 PARSE_ARGS2 (tok, str, str);
1429 ret_ptr = boolector_smod (
1430 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1431 exp_ret = RET_NODEPTR;
1432 }
1433 else if (!strcmp (tok, "concat"))
1434 {
1435 PARSE_ARGS2 (tok, str, str);
1436 ret_ptr = boolector_concat (
1437 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1438 exp_ret = RET_NODEPTR;
1439 }
1440 else if (!strcmp (tok, "repeat"))
1441 {
1442 PARSE_ARGS2 (tok, str, uint);
1443 ret_ptr = boolector_repeat (btor, hmap_get (hmap, arg1_str), arg2_uint);
1444 exp_ret = RET_NODEPTR;
1445 }
1446 else if (!strcmp (tok, "read"))
1447 {
1448 PARSE_ARGS2 (tok, str, str);
1449 ret_ptr = boolector_read (
1450 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1451 exp_ret = RET_NODEPTR;
1452 }
1453 else if (!strcmp (tok, "write"))
1454 {
1455 PARSE_ARGS3 (tok, str, str, str);
1456 ret_ptr = boolector_write (btor,
1457 hmap_get (hmap, arg1_str),
1458 hmap_get (hmap, arg2_str),
1459 hmap_get (hmap, arg3_str));
1460 exp_ret = RET_NODEPTR;
1461 }
1462 else if (!strcmp (tok, "cond"))
1463 {
1464 PARSE_ARGS3 (tok, str, str, str);
1465 ret_ptr = boolector_cond (btor,
1466 hmap_get (hmap, arg1_str),
1467 hmap_get (hmap, arg2_str),
1468 hmap_get (hmap, arg3_str));
1469 exp_ret = RET_NODEPTR;
1470 }
1471 else if (!strcmp (tok, "param"))
1472 {
1473 PARSE_ARGS2 (tok, str, str);
1474 arg2_str = !strcmp (arg2_str, "(null)") ? 0 : arg2_str;
1475 ret_ptr = boolector_param (btor, get_sort (hmap, arg1_str), arg2_str);
1476 exp_ret = RET_NODEPTR;
1477 }
1478 else if (!strcmp (tok, "fun"))
1479 {
1480 arg1_uint = parse_uint_arg (tok); /* paramc */
1481 BTOR_NEWN (g_btorunt->mm, tmp, arg1_uint); /* params */
1482 for (i = 0; i < arg1_uint; i++)
1483 tmp[i] = hmap_get (hmap, parse_str_arg (tok));
1484 arg1_str = parse_str_arg (tok); /* function body */
1485 parse_check_last_arg (tok);
1486 ret_ptr = boolector_fun (btor, tmp, arg1_uint, hmap_get (hmap, arg1_str));
1487 BTOR_DELETEN (g_btorunt->mm, tmp, arg1_uint);
1488 exp_ret = RET_NODEPTR;
1489 }
1490 else if (!strcmp (tok, "exists"))
1491 {
1492 arg1_uint = parse_uint_arg (tok);
1493 BTOR_NEWN (g_btorunt->mm, tmp, arg1_uint); /* vars */
1494 for (i = 0; i < arg1_uint; i++)
1495 tmp[i] = hmap_get (hmap, parse_str_arg (tok));
1496 arg1_str = parse_str_arg (tok); /* body */
1497 parse_check_last_arg (tok);
1498 ret_ptr =
1499 boolector_exists (btor, tmp, arg1_uint, hmap_get (hmap, arg1_str));
1500 BTOR_DELETEN (g_btorunt->mm, tmp, arg1_uint);
1501 exp_ret = RET_NODEPTR;
1502 }
1503 else if (!strcmp (tok, "forall"))
1504 {
1505 arg1_uint = parse_uint_arg (tok);
1506 BTOR_NEWN (g_btorunt->mm, tmp, arg1_uint); /* vars */
1507 for (i = 0; i < arg1_uint; i++)
1508 tmp[i] = hmap_get (hmap, parse_str_arg (tok));
1509 arg1_str = parse_str_arg (tok); /* body */
1510 parse_check_last_arg (tok);
1511 ret_ptr =
1512 boolector_forall (btor, tmp, arg1_uint, hmap_get (hmap, arg1_str));
1513 BTOR_DELETEN (g_btorunt->mm, tmp, arg1_uint);
1514 exp_ret = RET_NODEPTR;
1515 }
1516 else if (!strcmp (tok, "apply"))
1517 {
1518 arg1_uint = parse_uint_arg (tok); /* argc */
1519 BTOR_NEWN (g_btorunt->mm, tmp, arg1_uint); /* args */
1520 for (i = 0; i < arg1_uint; i++)
1521 tmp[i] = hmap_get (hmap, parse_str_arg (tok));
1522 arg1_str = parse_str_arg (tok); /* function */
1523 parse_check_last_arg (tok);
1524 ret_ptr =
1525 boolector_apply (btor, tmp, arg1_uint, hmap_get (hmap, arg1_str));
1526 BTOR_DELETEN (g_btorunt->mm, tmp, arg1_uint);
1527 exp_ret = RET_NODEPTR;
1528 }
1529 else if (!strcmp (tok, "inc"))
1530 {
1531 PARSE_ARGS1 (tok, str);
1532 ret_ptr = boolector_inc (btor, hmap_get (hmap, arg1_str));
1533 exp_ret = RET_NODEPTR;
1534 }
1535 else if (!strcmp (tok, "dec"))
1536 {
1537 PARSE_ARGS1 (tok, str);
1538 ret_ptr = boolector_dec (btor, hmap_get (hmap, arg1_str));
1539 exp_ret = RET_NODEPTR;
1540 }
1541 /* getter */
1542 else if (!strcmp (tok, "get_refs"))
1543 {
1544 PARSE_ARGS0 (tok);
1545 if (!g_btorunt->skip)
1546 {
1547 ret_uint = boolector_get_refs (btor);
1548 exp_ret = RET_UINT;
1549 }
1550 else
1551 exp_ret = RET_SKIP;
1552 }
1553 else if (!strcmp (tok, "get_node_id"))
1554 {
1555 PARSE_ARGS1 (tok, str);
1556 if (!g_btorunt->skip)
1557 {
1558 ret_int = boolector_get_node_id (btor, hmap_get (hmap, arg1_str));
1559 exp_ret = RET_INT;
1560 }
1561 else
1562 exp_ret = RET_SKIP;
1563 }
1564 else if (!strcmp (tok, "get_symbol"))
1565 {
1566 PARSE_ARGS1 (tok, str);
1567 if (!g_btorunt->skip)
1568 {
1569 ret_str =
1570 (char *) boolector_get_symbol (btor, hmap_get (hmap, arg1_str));
1571 if (!ret_str) ret_str = "(null)";
1572 exp_ret = RET_CHARPTR;
1573 }
1574 else
1575 exp_ret = RET_SKIP;
1576 }
1577 else if (!strcmp (tok, "set_symbol"))
1578 {
1579 PARSE_ARGS2 (tok, str, str);
1580 boolector_set_symbol (btor, hmap_get (hmap, arg1_str), arg2_str);
1581 }
1582 else if (!strcmp (tok, "get_width"))
1583 {
1584 PARSE_ARGS1 (tok, str);
1585 if (!g_btorunt->skip)
1586 {
1587 ret_uint = boolector_get_width (btor, hmap_get (hmap, arg1_str));
1588 exp_ret = RET_UINT;
1589 }
1590 else
1591 exp_ret = RET_SKIP;
1592 }
1593 else if (!strcmp (tok, "get_index_width"))
1594 {
1595 PARSE_ARGS1 (tok, str);
1596 if (!g_btorunt->skip)
1597 {
1598 ret_uint = boolector_get_index_width (btor, hmap_get (hmap, arg1_str));
1599 exp_ret = RET_UINT;
1600 }
1601 else
1602 exp_ret = RET_SKIP;
1603 }
1604 else if (!strcmp (tok, "get_bits"))
1605 {
1606 PARSE_ARGS1 (tok, str);
1607 ret_ptr = (char *) boolector_get_bits (btor, hmap_get (hmap, arg1_str));
1608 exp_ret = RET_VOIDPTR;
1609 }
1610 else if (!strcmp (tok, "free_bits"))
1611 {
1612 PARSE_ARGS1 (tok, str);
1613 boolector_free_bits (btor, hmap_get (hmap, arg1_str));
1614 }
1615 else if (!strcmp (tok, "get_fun_arity"))
1616 {
1617 PARSE_ARGS1 (tok, str);
1618 if (!g_btorunt->skip)
1619 {
1620 ret_uint = boolector_get_fun_arity (btor, hmap_get (hmap, arg1_str));
1621 exp_ret = RET_UINT;
1622 }
1623 else
1624 exp_ret = RET_SKIP;
1625 }
1626 else if (!strcmp (tok, "get_btor"))
1627 {
1628 PARSE_ARGS1 (tok, str);
1629 if (!g_btorunt->skip)
1630 {
1631 ret_ptr = boolector_get_btor (hmap_get (hmap, arg1_str));
1632 exp_ret = RET_VOIDPTR;
1633 }
1634 else
1635 exp_ret = RET_SKIP;
1636 }
1637 else if (!strcmp (tok, "is_const"))
1638 {
1639 PARSE_ARGS1 (tok, str);
1640 if (!g_btorunt->skip)
1641 {
1642 ret_bool = boolector_is_const (btor, hmap_get (hmap, arg1_str));
1643 exp_ret = RET_BOOL;
1644 }
1645 else
1646 exp_ret = RET_SKIP;
1647 }
1648 else if (!strcmp (tok, "is_var"))
1649 {
1650 PARSE_ARGS1 (tok, str);
1651 if (!g_btorunt->skip)
1652 {
1653 ret_bool = boolector_is_var (btor, hmap_get (hmap, arg1_str));
1654 exp_ret = RET_BOOL;
1655 }
1656 else
1657 exp_ret = RET_SKIP;
1658 }
1659 else if (!strcmp (tok, "is_array"))
1660 {
1661 PARSE_ARGS1 (tok, str);
1662 if (!g_btorunt->skip)
1663 {
1664 ret_bool = boolector_is_array (btor, hmap_get (hmap, arg1_str));
1665 exp_ret = RET_BOOL;
1666 }
1667 else
1668 exp_ret = RET_SKIP;
1669 }
1670 else if (!strcmp (tok, "is_array_var"))
1671 {
1672 PARSE_ARGS1 (tok, str);
1673 if (!g_btorunt->skip)
1674 {
1675 ret_bool = boolector_is_array_var (btor, hmap_get (hmap, arg1_str));
1676 exp_ret = RET_BOOL;
1677 }
1678 else
1679 exp_ret = RET_SKIP;
1680 }
1681 else if (!strcmp (tok, "is_param"))
1682 {
1683 PARSE_ARGS1 (tok, str);
1684 if (!g_btorunt->skip)
1685 {
1686 ret_bool = boolector_is_param (btor, hmap_get (hmap, arg1_str));
1687 exp_ret = RET_BOOL;
1688 }
1689 else
1690 exp_ret = RET_SKIP;
1691 }
1692 else if (!strcmp (tok, "is_bound_param"))
1693 {
1694 PARSE_ARGS1 (tok, str);
1695 if (!g_btorunt->skip)
1696 {
1697 ret_bool = boolector_is_bound_param (btor, hmap_get (hmap, arg1_str));
1698 exp_ret = RET_BOOL;
1699 }
1700 else
1701 exp_ret = RET_SKIP;
1702 }
1703 else if (!strcmp (tok, "is_uf"))
1704 {
1705 PARSE_ARGS1 (tok, str);
1706 if (!g_btorunt->skip)
1707 {
1708 ret_bool = boolector_is_uf (btor, hmap_get (hmap, arg1_str));
1709 exp_ret = RET_BOOL;
1710 }
1711 else
1712 exp_ret = RET_SKIP;
1713 }
1714 else if (!strcmp (tok, "is_fun"))
1715 {
1716 PARSE_ARGS1 (tok, str);
1717 if (!g_btorunt->skip)
1718 {
1719 ret_bool = boolector_is_fun (btor, hmap_get (hmap, arg1_str));
1720 exp_ret = RET_BOOL;
1721 }
1722 else
1723 exp_ret = RET_SKIP;
1724 }
1725 else if (!strcmp (tok, "fun_sort_check"))
1726 {
1727 arg1_uint = parse_uint_arg (tok); /* argc */
1728 BTOR_NEWN (g_btorunt->mm, tmp, arg1_uint);
1729 for (i = 0; i < arg1_uint; i++) /* args */
1730 tmp[i] = hmap_get (hmap, parse_str_arg (tok));
1731 arg1_str = parse_str_arg (tok); /* function body */
1732 parse_check_last_arg (tok);
1733 ret_int = boolector_fun_sort_check (
1734 btor, tmp, arg1_uint, hmap_get (hmap, arg1_str));
1735 exp_ret = RET_SKIP;
1736 BTOR_DELETEN (g_btorunt->mm, tmp, arg1_uint);
1737 }
1738 else if (!strcmp (tok, "bv_assignment"))
1739 {
1740 PARSE_ARGS1 (tok, str);
1741 ret_ptr =
1742 (char *) boolector_bv_assignment (btor, hmap_get (hmap, arg1_str));
1743 exp_ret = RET_VOIDPTR;
1744 }
1745 else if (!strcmp (tok, "free_bv_assignment"))
1746 {
1747 PARSE_ARGS1 (tok, str);
1748 boolector_free_bv_assignment (btor, hmap_get (hmap, arg1_str));
1749 }
1750 else if (!strcmp (tok, "array_assignment"))
1751 {
1752 PARSE_ARGS1 (tok, str);
1753 boolector_array_assignment (
1754 btor, hmap_get (hmap, arg1_str), &res1_pptr, &res2_pptr, &ret_uint);
1755 exp_ret = RET_ARRASS;
1756 }
1757 else if (!strcmp (tok, "free_array_assignment"))
1758 {
1759 PARSE_ARGS3 (tok, str, str, uint);
1760 boolector_free_array_assignment (btor,
1761 hmap_get (hmap, arg1_str),
1762 hmap_get (hmap, arg2_str),
1763 arg3_uint);
1764 }
1765 else if (!strcmp (tok, "uf_assignment"))
1766 {
1767 PARSE_ARGS1 (tok, str);
1768 boolector_uf_assignment (
1769 btor, hmap_get (hmap, arg1_str), &res1_pptr, &res2_pptr, &ret_uint);
1770 exp_ret = RET_ARRASS;
1771 }
1772 else if (!strcmp (tok, "free_uf_assignment"))
1773 {
1774 PARSE_ARGS3 (tok, str, str, uint);
1775 boolector_free_uf_assignment (btor,
1776 hmap_get (hmap, arg1_str),
1777 hmap_get (hmap, arg2_str),
1778 arg3_uint);
1779 }
1780 else if (!strcmp (tok, "print_model"))
1781 {
1782 PARSE_ARGS1 (tok, str);
1783 boolector_print_model (btor, arg1_str, stdout);
1784 }
1785 else if (!strcmp (tok, "print_value_smt2"))
1786 {
1787 PARSE_ARGS2 (tok, str, str);
1788 boolector_print_value_smt2 (
1789 btor, hmap_get (hmap, arg1_str), arg2_str, stdout);
1790 }
1791 else if (!strcmp (tok, "var_mark_bool"))
1792 {
1793 PARSE_ARGS1 (tok, str);
1794 boolector_var_mark_bool (btor, hmap_get (hmap, arg1_str));
1795 }
1796 /* sorts */
1797 else if (!strcmp (tok, "bool_sort"))
1798 {
1799 PARSE_ARGS0 (tok);
1800 ret_ptr = (void *) (size_t) boolector_bool_sort (btor);
1801 exp_ret = RET_SORTPTR;
1802 }
1803 else if (!strcmp (tok, "bitvec_sort"))
1804 {
1805 PARSE_ARGS1 (tok, uint);
1806 ret_ptr = (void *) (size_t) boolector_bitvec_sort (btor, arg1_uint);
1807 exp_ret = RET_SORTPTR;
1808 }
1809 else if (!strcmp (tok, "array_sort"))
1810 {
1811 PARSE_ARGS2 (tok, str, str);
1812 ret_ptr = (void *) (size_t) boolector_array_sort (
1813 btor, get_sort (hmap, arg1_str), get_sort (hmap, arg2_str));
1814 exp_ret = RET_SORTPTR;
1815 }
1816 else if (!strcmp (tok, "copy_sort"))
1817 {
1818 PARSE_ARGS1 (tok, str);
1819 ret_ptr = (void *) (size_t) boolector_copy_sort (
1820 btor, get_sort (hmap, arg1_str));
1821 exp_ret = RET_SORTPTR;
1822 }
1823 else if (!strcmp (tok, "fun_sort"))
1824 {
1825 while ((tok = strtok (0, " ")))
1826 BTOR_PUSH_STACK (sort_stack, get_sort (hmap, tok));
1827 assert (BTOR_COUNT_STACK (sort_stack) >= 2);
1828 ret_ptr = (void *) (size_t) boolector_fun_sort (
1829 btor,
1830 sort_stack.start,
1831 BTOR_COUNT_STACK (sort_stack) - 1,
1832 BTOR_TOP_STACK (sort_stack));
1833 exp_ret = RET_SORTPTR;
1834 }
1835 else if (!strcmp (tok, "release_sort"))
1836 {
1837 PARSE_ARGS1 (tok, str);
1838 boolector_release_sort (btor, get_sort (hmap, arg1_str));
1839 }
1840 else if (!strcmp (tok, "is_equal_sort"))
1841 {
1842 PARSE_ARGS2 (tok, str, str);
1843 ret_bool = boolector_is_equal_sort (
1844 btor, hmap_get (hmap, arg1_str), hmap_get (hmap, arg2_str));
1845 exp_ret = RET_BOOL;
1846 }
1847 else if (!strcmp (tok, "is_array_sort"))
1848 {
1849 PARSE_ARGS1 (tok, str);
1850 ret_bool = boolector_is_array_sort (btor, get_sort (hmap, arg1_str));
1851 exp_ret = RET_BOOL;
1852 }
1853 else if (!strcmp (tok, "is_fun_sort"))
1854 {
1855 PARSE_ARGS1 (tok, str);
1856 if (!g_btorunt->skip)
1857 {
1858 ret_bool = boolector_is_fun_sort (btor, get_sort (hmap, arg1_str));
1859 exp_ret = RET_BOOL;
1860 }
1861 else
1862 {
1863 exp_ret = RET_SKIP;
1864 }
1865 }
1866 else if (!strcmp (tok, "is_bitvec_sort"))
1867 {
1868 PARSE_ARGS1 (tok, str);
1869 if (!g_btorunt->skip)
1870 {
1871 ret_bool = boolector_is_bitvec_sort (btor, get_sort (hmap, arg1_str));
1872 exp_ret = RET_BOOL;
1873 }
1874 else
1875 {
1876 exp_ret = RET_SKIP;
1877 }
1878 }
1879 else if (!strcmp (tok, "bitvec_sort_get_width"))
1880 {
1881 PARSE_ARGS1 (tok, str);
1882 if (!g_btorunt->skip)
1883 {
1884 ret_uint =
1885 boolector_bitvec_sort_get_width (btor, get_sort (hmap, arg1_str));
1886 exp_ret = RET_UINT;
1887 }
1888 else
1889 {
1890 exp_ret = RET_SKIP;
1891 }
1892 }
1893 else if (!strcmp (tok, "get_sort"))
1894 {
1895 PARSE_ARGS1 (tok, str);
1896 ret_ptr = boolector_get_sort (btor, hmap_get (hmap, arg1_str));
1897 exp_ret = RET_SORTPTR;
1898 }
1899 else if (!strcmp (tok, "fun_get_domain_sort"))
1900 {
1901 PARSE_ARGS1 (tok, str);
1902 ret_ptr = boolector_fun_get_domain_sort (btor, hmap_get (hmap, arg1_str));
1903 exp_ret = RET_SORTPTR;
1904 }
1905 else if (!strcmp (tok, "fun_get_codomain_sort"))
1906 {
1907 PARSE_ARGS1 (tok, str);
1908 ret_ptr =
1909 boolector_fun_get_codomain_sort (btor, hmap_get (hmap, arg1_str));
1910 exp_ret = RET_SORTPTR;
1911 }
1912 /* dumping */
1913 else if (!strcmp (tok, "dump_btor_node"))
1914 {
1915 PARSE_ARGS1 (tok, str);
1916 boolector_dump_btor_node (btor, stdout, hmap_get (hmap, arg1_str));
1917 }
1918 else if (!strcmp (tok, "dump_smt2_node"))
1919 {
1920 PARSE_ARGS1 (tok, str);
1921 boolector_dump_smt2_node (btor, stdout, hmap_get (hmap, arg1_str));
1922 }
1923 else if (!strcmp (tok, "dump_btor") || !strcmp (tok, "dump_smt2"))
1924 {
1925 PARSE_ARGS0 (tok);
1926
1927 if (g_btorunt->dump_stdout)
1928 {
1929 if (!strcmp (tok, "dump_btor"))
1930 boolector_dump_btor (btor, stdout);
1931 else
1932 boolector_dump_smt2 (btor, stdout);
1933 }
1934 else
1935 {
1936 basename = strrchr (g_btorunt->filename, '/');
1937 if (basename)
1938 basename += 1; /* skip '/' character */
1939 else
1940 basename = g_btorunt->filename;
1941 flen = 40 + strlen ("/tmp/") + strlen (basename);
1942 BTOR_NEWN (g_btorunt->mm, outfilename, flen);
1943
1944 if (!strcmp (tok, "dump_btor"))
1945 {
1946 sprintf (outfilename, "/tmp/%s.%s", basename, "btor");
1947 outfile = fopen (outfilename, "w");
1948 assert (outfile);
1949 boolector_dump_btor (btor, outfile);
1950 }
1951 else
1952 {
1953 sprintf (outfilename, "/tmp/%s.%s", basename, "smt2");
1954 outfile = fopen (outfilename, "w");
1955 assert (outfile);
1956 boolector_dump_smt2 (btor, outfile);
1957 }
1958
1959 BTORUNT_LOG ("dump formula to %s", outfilename);
1960 fclose (outfile);
1961 outfile = fopen (outfilename, "r");
1962 tmpbtor = boolector_new ();
1963 boolector_set_opt (tmpbtor, BTOR_OPT_PARSE_INTERACTIVE, 0);
1964 bool parsed_smt2;
1965 pres = boolector_parse (
1966 tmpbtor, outfile, outfilename, stdout, &emsg, &pstat, &parsed_smt2);
1967 (void) pres;
1968 (void) parsed_smt2;
1969 if (emsg)
1970 fprintf (stderr, "error while parsing dumped file: %s\n", emsg);
1971 assert (pres != BOOLECTOR_PARSE_ERROR);
1972 (void) pstat;
1973 boolector_delete (tmpbtor);
1974 fclose (outfile);
1975 unlink (outfilename);
1976 BTOR_DELETEN (g_btorunt->mm, outfilename, flen);
1977 }
1978 }
1979 else if (!strcmp (tok, "dump_aiger_ascii"))
1980 {
1981 PARSE_ARGS1 (tok, int);
1982 boolector_dump_aiger_ascii (btor, stdout, arg1_int);
1983 }
1984 else if (!strcmp (tok, "dump_aiger_binary"))
1985 {
1986 PARSE_ARGS1 (tok, int);
1987 boolector_dump_aiger_binary (btor, stdout, arg1_int);
1988 }
1989 else
1990 {
1991 btorunt_parse_error ("invalid command '%s'", tok);
1992 }
1993 }
1994 g_btorunt->line++;
1995 len = 0;
1996 goto NEXT;
1997 DONE:
1998 BTORUNT_LOG ("done %s", g_btorunt->filename);
1999 BTOR_RELEASE_STACK (arg_int);
2000 BTOR_RELEASE_STACK (arg_str);
2001 BTOR_RELEASE_STACK (sort_stack);
2002 BTOR_DELETEN (g_btorunt->mm, buffer, buffer_len);
2003 BTOR_DELETEN (g_btorunt->mm, btor_str, BTOR_STR_LEN);
2004 hmap_clear (hmap);
2005 btor_hashptr_table_delete (hmap);
2006 if (delete) boolector_delete (btor);
2007 }
2008
2009 #ifdef BTOR_HAVE_SIGNALS
2010 static void
exit_on_signal(int32_t sig)2011 exit_on_signal (int32_t sig)
2012 {
2013 BTORUNT_LOG ("exit on signal %d", sig);
2014 raise (sig);
2015 }
2016 #endif
2017
2018 int32_t
main(int32_t argc,char ** argv)2019 main (int32_t argc, char **argv)
2020 {
2021 int32_t i;
2022 uint32_t val;
2023 Btor *tmpbtor;
2024 BtorOption o;
2025 BtorUNTBtorOpt *btoropt;
2026 char *tmp;
2027 const char *lng;
2028 FILE *file;
2029
2030 g_btorunt = btorunt_new ();
2031
2032 for (i = 1, tmpbtor = 0; i < argc; i++)
2033 {
2034 if (!strcmp (argv[i], "-h"))
2035 {
2036 printf ("%s", BTORUNT_USAGE);
2037 exit (0);
2038 }
2039 else if (!strcmp (argv[i], "-v") || !strcmp (argv[i], "--verbose"))
2040 g_btorunt->verbosity = 1;
2041 else if (!strcmp (argv[i], "-e") || !strcmp (argv[i], "--exit-on-abort"))
2042 g_btorunt->exit_on_abort = true;
2043 else if (!strcmp (argv[i], "-s") || !strcmp (argv[i], "--skip"))
2044 g_btorunt->skip = true;
2045 else if (!strcmp (argv[i], "-i")
2046 || !strcmp (argv[i], "--ignore-sat-result"))
2047 g_btorunt->ignore_sat = true;
2048 else if (!strcmp (argv[i], "-b"))
2049 {
2050 if (++i == argc) btorunt_error ("argument to '-b' missing (try '-h')");
2051 if (!tmpbtor) tmpbtor = boolector_new ();
2052 for (o = boolector_first_opt (tmpbtor), lng = 0;
2053 boolector_has_opt (tmpbtor, o);
2054 o = boolector_next_opt (tmpbtor, o))
2055 {
2056 lng = boolector_get_opt_lng (tmpbtor, o);
2057 if (!strcmp (lng, argv[i])) break;
2058 }
2059 if (!lng) btorunt_error ("invalid boolector option '%s'", argv[i]);
2060 if (++i == argc) btorunt_error ("argument to '-b' missing (try '-h')");
2061 val = (uint32_t) strtol (argv[i], &tmp, 10);
2062 if (tmp[0] != 0) btorunt_error ("invalid argument to '-b' (try -h)");
2063 BTOR_NEW (g_btorunt->mm, btoropt);
2064 btoropt->kind = o;
2065 btoropt->name = btor_mem_strdup (g_btorunt->mm, lng);
2066 btoropt->val = val;
2067 BTOR_PUSH_STACK (g_btorunt->cl_btor_opts, btoropt);
2068 }
2069 else if (!strcmp (argv[i], "-d") || !strcmp (argv[i], "--dump-stdout"))
2070 g_btorunt->dump_stdout = true;
2071 else if (argv[i][0] == '-')
2072 btorunt_error ("invalid command line option '%s' (try '-h')", argv[i]);
2073 else if (g_btorunt->filename)
2074 btorunt_error ("multiple trace files specified (try '-h')");
2075 else
2076 g_btorunt->filename = argv[i];
2077 }
2078
2079 if (tmpbtor) boolector_delete (tmpbtor);
2080
2081 if (g_btorunt->filename)
2082 {
2083 file = fopen (g_btorunt->filename, "r");
2084 if (!file) btorunt_error ("can not read '%s'", g_btorunt->filename);
2085 }
2086 else
2087 g_btorunt->filename = "<stdin>", file = stdin;
2088
2089 #ifdef BTOR_HAVE_SIGNALS
2090 if (g_btorunt->exit_on_abort)
2091 {
2092 BTORUNT_LOG ("setting signal handlers since '-e' specified");
2093 signal (SIGINT, exit_on_signal);
2094 signal (SIGSEGV, exit_on_signal);
2095 signal (SIGABRT, exit_on_signal);
2096 signal (SIGTERM, exit_on_signal);
2097 }
2098 #endif
2099
2100 parse (file);
2101 fclose (file);
2102 btorunt_delete (g_btorunt);
2103 return 0;
2104 }
2105