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 "btorparse.h"
10 #include "boolector.h"
11 #include "btorcore.h"
12 #include "btoropt.h"
13 #include "parser/btorbtor.h"
14 #include "parser/btorbtor2.h"
15 #include "parser/btorsmt.h"
16 #include "parser/btorsmt2.h"
17 #include "utils/btormem.h"
18 #include "utils/btorstack.h"
19
20 #include <ctype.h>
21
22 static bool
has_compressed_suffix(const char * str,const char * suffix)23 has_compressed_suffix (const char *str, const char *suffix)
24 {
25 int32_t l = strlen (str), k = strlen (suffix), d = l - k;
26 if (d < 0) return 0;
27 if (!strcmp (str + d, suffix)) return 1;
28 if (d - 3 >= 0 && !strcmp (str + l - 3, ".gz") && !strcmp (str + l - 3, ".7z")
29 && !strncmp (str + d - 3, suffix, k))
30 return 1;
31 return 0;
32 }
33
34 /* return BOOLECTOR_(SAT|UNSAT|UNKNOWN|PARSE_ERROR) */
35 static int32_t
parse_aux(Btor * btor,FILE * infile,BtorCharStack * prefix,const char * infile_name,FILE * outfile,const BtorParserAPI * parser_api,char ** error_msg,int32_t * status,char * msg)36 parse_aux (Btor *btor,
37 FILE *infile,
38 BtorCharStack *prefix,
39 const char *infile_name,
40 FILE *outfile,
41 const BtorParserAPI *parser_api,
42 char **error_msg,
43 int32_t *status,
44 char *msg)
45 {
46 assert (btor);
47 assert (infile);
48 assert (infile_name);
49 assert (outfile);
50 assert (parser_api);
51 assert (error_msg);
52 assert (status);
53
54 BtorParser *parser;
55 BtorParseResult parse_res;
56 int32_t res;
57 char *emsg;
58
59 res = BOOLECTOR_UNKNOWN;
60 *error_msg = 0;
61
62 BTOR_MSG (btor->msg, 1, "%s", msg);
63 parser = parser_api->init (btor);
64
65 if ((emsg = parser_api->parse (
66 parser, prefix, infile, infile_name, outfile, &parse_res)))
67 {
68 res = BOOLECTOR_PARSE_ERROR;
69 btor->parse_error_msg = btor_mem_strdup (btor->mm, emsg);
70 *error_msg = btor->parse_error_msg;
71 }
72 else
73 {
74 res = parse_res.nsatcalls ? parse_res.result : BOOLECTOR_PARSE_UNKNOWN;
75
76 if (parse_res.logic == BTOR_LOGIC_QF_BV)
77 BTOR_MSG (btor->msg, 1, "logic QF_BV");
78 else if (parse_res.logic == BTOR_LOGIC_BV)
79 BTOR_MSG (btor->msg, 1, "logic BV");
80 else if (parse_res.logic == BTOR_LOGIC_QF_UFBV)
81 BTOR_MSG (btor->msg, 1, "logic QF_UFBV");
82 else if (parse_res.logic == BTOR_LOGIC_QF_ABV)
83 BTOR_MSG (btor->msg, 1, "logic QF_ABV");
84 else
85 {
86 assert (parse_res.logic == BTOR_LOGIC_QF_AUFBV);
87 BTOR_MSG (btor->msg, 1, "logic QF_AUFBV");
88 }
89
90 if (parse_res.status == BOOLECTOR_SAT)
91 BTOR_MSG (btor->msg, 1, "status sat");
92 else if (parse_res.status == BOOLECTOR_UNSAT)
93 BTOR_MSG (btor->msg, 1, "status unsat");
94 else
95 {
96 assert (parse_res.status == BOOLECTOR_UNKNOWN);
97 BTOR_MSG (btor->msg, 1, "status unknown");
98 }
99 }
100
101 if (status) *status = parse_res.status;
102
103 /* cleanup */
104 parser_api->reset (parser);
105
106 return res;
107 }
108
109 int32_t
btor_parse(Btor * btor,FILE * infile,const char * infile_name,FILE * outfile,char ** error_msg,int32_t * status,bool * parsed_smt2)110 btor_parse (Btor *btor,
111 FILE *infile,
112 const char *infile_name,
113 FILE *outfile,
114 char **error_msg,
115 int32_t *status,
116 bool *parsed_smt2)
117 {
118 assert (btor);
119 assert (infile);
120 assert (infile_name);
121 assert (outfile);
122 assert (error_msg);
123 assert (status);
124 assert (parsed_smt2);
125
126 const BtorParserAPI *parser_api;
127 int32_t idx, first, second, res;
128 uint32_t len;
129 char ch, *msg;
130 BtorCharStack prefix;
131 BtorMemMgr *mem;
132
133 idx = 0;
134 len = 40 + strlen (infile_name);
135 BTOR_NEWN (btor->mm, msg, len);
136 mem = btor_mem_mgr_new ();
137 BTOR_INIT_STACK (mem, prefix);
138 *parsed_smt2 = false;
139
140 if (has_compressed_suffix (infile_name, ".btor"))
141 {
142 parser_api = btor_parsebtor_parser_api ();
143 sprintf (msg, "parsing '%s'", infile_name);
144 }
145 if (has_compressed_suffix (infile_name, ".btor2"))
146 {
147 parser_api = btor_parsebtor2_parser_api ();
148 sprintf (msg, "parsing '%s'", infile_name);
149 }
150 else if (has_compressed_suffix (infile_name, ".smt2"))
151 {
152 parser_api = btor_parsesmt2_parser_api ();
153 sprintf (msg, "parsing '%s'", infile_name);
154 *parsed_smt2 = true;
155 }
156 else
157 {
158 first = second = 0;
159 parser_api = btor_parsebtor_parser_api ();
160 sprintf (msg, "assuming BTOR input, parsing '%s'", infile_name);
161 for (;;)
162 {
163 ch = getc (infile);
164 BTOR_PUSH_STACK (prefix, ch);
165 if (!ch || ch == EOF) break;
166 if (ch == ' ' || ch == '\t' || ch == '\r' || ch == '\n')
167 {
168 BTOR_PUSH_STACK (prefix, ch);
169 }
170 else if (ch == ';')
171 {
172 BTOR_PUSH_STACK (prefix, ';');
173 do
174 {
175 ch = getc (infile);
176 if (ch == EOF) break;
177 BTOR_PUSH_STACK (prefix, ch);
178 } while (ch != '\n');
179 if (ch == EOF) break;
180 }
181 else if (!first)
182 {
183 first = ch;
184 idx = BTOR_COUNT_STACK (prefix) - 1;
185 }
186 else
187 {
188 second = ch;
189 break;
190 }
191 }
192
193 if (ch != EOF && ch)
194 {
195 assert (first && second);
196 if (first == '(')
197 {
198 if (second == 'b')
199 {
200 parser_api = btor_parsesmt_parser_api ();
201 sprintf (
202 msg, "assuming SMT-LIB v1 input, parsing '%s'", infile_name);
203 }
204 else
205 {
206 parser_api = btor_parsesmt2_parser_api ();
207 *parsed_smt2 = true;
208 sprintf (
209 msg, "assuming SMT-LIB v2 input, parsing '%s'", infile_name);
210 }
211 }
212 else
213 {
214 do
215 {
216 ch = getc (infile);
217 if (ch == EOF) break;
218 BTOR_PUSH_STACK (prefix, ch);
219 } while (ch != '\n');
220 BTOR_PUSH_STACK (prefix, 0);
221 if (strstr (prefix.start + idx, " sort ") != NULL)
222 {
223 parser_api = btor_parsebtor2_parser_api ();
224 sprintf (
225 msg, "assuming BTOR2 input, parsing '%s'", infile_name);
226 }
227 (void) BTOR_POP_STACK (prefix);
228 }
229 }
230 }
231
232 res = parse_aux (btor,
233 infile,
234 &prefix,
235 infile_name,
236 outfile,
237 parser_api,
238 error_msg,
239 status,
240 msg);
241
242 /* cleanup */
243 BTOR_RELEASE_STACK (prefix);
244 btor_mem_mgr_delete (mem);
245 BTOR_DELETEN (btor->mm, msg, len);
246
247 return res;
248 }
249
250 int32_t
btor_parse_btor(Btor * btor,FILE * infile,const char * infile_name,FILE * outfile,char ** error_msg,int32_t * status)251 btor_parse_btor (Btor *btor,
252 FILE *infile,
253 const char *infile_name,
254 FILE *outfile,
255 char **error_msg,
256 int32_t *status)
257 {
258 assert (btor);
259 assert (infile);
260 assert (infile_name);
261 assert (outfile);
262 assert (error_msg);
263 assert (status);
264
265 const BtorParserAPI *parser_api;
266 parser_api = btor_parsebtor_parser_api ();
267 return parse_aux (
268 btor, infile, 0, infile_name, outfile, parser_api, error_msg, status, 0);
269 }
270
271 int32_t
btor_parse_btor2(Btor * btor,FILE * infile,const char * infile_name,FILE * outfile,char ** error_msg,int32_t * status)272 btor_parse_btor2 (Btor *btor,
273 FILE *infile,
274 const char *infile_name,
275 FILE *outfile,
276 char **error_msg,
277 int32_t *status)
278 {
279 assert (btor);
280 assert (infile);
281 assert (infile_name);
282 assert (outfile);
283 assert (error_msg);
284 assert (status);
285
286 const BtorParserAPI *parser_api;
287 parser_api = btor_parsebtor2_parser_api ();
288 return parse_aux (
289 btor, infile, 0, infile_name, outfile, parser_api, error_msg, status, 0);
290 }
291
292 int32_t
btor_parse_smt1(Btor * btor,FILE * infile,const char * infile_name,FILE * outfile,char ** error_msg,int32_t * status)293 btor_parse_smt1 (Btor *btor,
294 FILE *infile,
295 const char *infile_name,
296 FILE *outfile,
297 char **error_msg,
298 int32_t *status)
299 {
300 assert (btor);
301 assert (infile);
302 assert (infile_name);
303 assert (outfile);
304 assert (error_msg);
305 assert (status);
306
307 const BtorParserAPI *parser_api;
308 parser_api = btor_parsesmt_parser_api ();
309 return parse_aux (
310 btor, infile, 0, infile_name, outfile, parser_api, error_msg, status, 0);
311 }
312
313 int32_t
btor_parse_smt2(Btor * btor,FILE * infile,const char * infile_name,FILE * outfile,char ** error_msg,int32_t * status)314 btor_parse_smt2 (Btor *btor,
315 FILE *infile,
316 const char *infile_name,
317 FILE *outfile,
318 char **error_msg,
319 int32_t *status)
320 {
321 assert (btor);
322 assert (infile);
323 assert (infile_name);
324 assert (outfile);
325 assert (error_msg);
326 assert (status);
327
328 const BtorParserAPI *parser_api;
329 parser_api = btor_parsesmt2_parser_api ();
330 return parse_aux (
331 btor, infile, 0, infile_name, outfile, parser_api, error_msg, status, 0);
332 }
333