1 /**
2 * Btor2Tools: A tool package for the BTOR format.
3 *
4 * Copyright (c) 2012-2015 Armin Biere.
5 * Copyright (c) 2017 Mathias Preiner.
6 * Copyright (c) 2017-2018 Aina Niemetz.
7 *
8 * All rights reserved.
9 *
10 * This file is part of the Btor2Tools package.
11 * See LICENSE.txt for more information on using this software.
12 */
13
14 #include "btor2parser/btor2parser.h"
15
16 #include <assert.h>
17 #include <inttypes.h>
18 #include <stdio.h>
19 #include <stdlib.h>
20 #include <string.h>
21
22 static int32_t close_input;
23 static FILE* input_file;
24 static const char* input_name;
25
26 /* Parse BTOR2 file and print to stdout. */
27
28 int32_t
main(int32_t argc,char ** argv)29 main (int32_t argc, char** argv)
30 {
31 Btor2Parser* reader;
32 Btor2LineIterator it;
33 Btor2Line* l;
34 uint32_t j;
35 int32_t i, verbosity = 0;
36 const char* err;
37 for (i = 1; i < argc; i++)
38 {
39 if (!strcmp (argv[i], "-h"))
40 {
41 fprintf (stderr, "usage: catbtor [-h|-v] [ <btorfile> ]\n");
42 exit (1);
43 }
44 else if (!strcmp (argv[i], "-v"))
45 verbosity++;
46 else if (argv[i][0] == '-')
47 {
48 fprintf (
49 stderr, "*** catbtor: invalid option '%s' (try '-h')\n", argv[i]);
50 exit (1);
51 }
52 else if (input_name)
53 {
54 fprintf (stderr, "*** catbtor: too many inputs (try '-h')\n");
55 exit (1);
56 }
57 else
58 input_name = argv[i];
59 }
60 if (!input_name)
61 {
62 input_file = stdin;
63 assert (!close_input);
64 input_name = "<stdin>";
65 }
66 else
67 {
68 input_file = fopen (input_name, "r");
69 if (!input_file)
70 {
71 fprintf (
72 stderr, "*** catbtor: can not open '%s' for reading\n", input_name);
73 exit (1);
74 }
75 close_input = 1;
76 }
77 if (verbosity)
78 {
79 fprintf (stderr,
80 "; [catbor] simple CAT for BTOR files\n"
81 "; [catbor] reading '%s'\n",
82 input_name);
83 fflush (stderr);
84 }
85 reader = btor2parser_new ();
86 if (!btor2parser_read_lines (reader, input_file))
87 {
88 err = btor2parser_error (reader);
89 assert (err);
90 fprintf (stderr, "*** catbtor: parse error in '%s' %s\n", input_name, err);
91 btor2parser_delete (reader);
92 if (close_input) fclose (input_file);
93 exit (1);
94 }
95 if (close_input) fclose (input_file);
96 if (verbosity)
97 {
98 fprintf (stderr, "; [catbor] finished parsing '%s'\n", input_name);
99 fflush (stderr);
100 }
101 if (verbosity)
102 {
103 fprintf (stderr, "; [catbor] starting to dump BTOR model to '<stdout>'\n");
104 fflush (stderr);
105 }
106 it = btor2parser_iter_init (reader);
107 while ((l = btor2parser_iter_next (&it)))
108 {
109 printf ("%" PRId64 " %s", l->id, l->name);
110 if (l->tag == BTOR2_TAG_sort)
111 {
112 printf (" %s", l->sort.name);
113 switch (l->sort.tag)
114 {
115 case BTOR2_TAG_SORT_bitvec: printf (" %u", l->sort.bitvec.width); break;
116 case BTOR2_TAG_SORT_array:
117 printf (" %" PRId64 " %" PRId64, l->sort.array.index, l->sort.array.element);
118 break;
119 default:
120 assert (0);
121 fprintf (stderr, "*** catbtor: invalid sort encountered\n");
122 exit (1);
123 }
124 }
125 else if (l->sort.id)
126 printf (" %" PRId64, l->sort.id);
127 for (j = 0; j < l->nargs; j++) printf (" %" PRId64, l->args[j]);
128 if (l->tag == BTOR2_TAG_slice) printf (" %" PRId64 " %" PRId64, l->args[1], l->args[2]);
129 if (l->tag == BTOR2_TAG_sext || l->tag == BTOR2_TAG_uext)
130 printf (" %" PRId64, l->args[1]);
131 if (l->constant) printf (" %s", l->constant);
132 if (l->symbol) printf (" %s", l->symbol);
133 fputc ('\n', stdout);
134 }
135 btor2parser_delete (reader);
136 if (verbosity)
137 {
138 fprintf (stderr, "; [catbor] finished dumping BTOR model to '<stdout>'\n");
139 fflush (stderr);
140 }
141 return 0;
142 }
143