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 "btortrapi.h"
10
11 void
btor_trapi_print(Btor * btor,const char * msg,...)12 btor_trapi_print (Btor *btor, const char *msg, ...)
13 {
14 assert (btor);
15 assert (btor->apitrace);
16
17 va_list args;
18 va_start (args, msg);
19 vfprintf (btor->apitrace, msg, args);
20 va_end (args);
21 fflush (btor->apitrace);
22 }
23
24 void
btor_trapi(Btor * btor,const char * fname,const char * msg,...)25 btor_trapi (Btor *btor, const char *fname, const char *msg, ...)
26 {
27 assert (btor);
28 assert (btor->apitrace);
29
30 va_list args;
31
32 if (fname)
33 {
34 /* skip boolector_ prefix */
35 fprintf (btor->apitrace, "%s", fname + 10);
36 /* skip functions that do not have 'btor' as argument */
37 if (strcmp (fname, "boolector_new") && strcmp (fname, "boolector_get_btor"))
38 fprintf (btor->apitrace, " %p", btor);
39 }
40 else
41 fputs ("return", btor->apitrace);
42
43 if (strlen (msg) > 0) fputc (' ', btor->apitrace);
44
45 va_start (args, msg);
46 vfprintf (btor->apitrace, msg, args);
47 va_end (args);
48 fputc ('\n', btor->apitrace);
49 fflush (btor->apitrace);
50 }
51
52 void
btor_trapi_open_trace(Btor * btor,const char * name)53 btor_trapi_open_trace (Btor *btor, const char *name)
54 {
55 assert (btor);
56 assert (name);
57
58 FILE *file;
59 char *cmd;
60 uint32_t len = strlen (name);
61
62 if (len >= 3 && !strcmp (name + len - 3, ".gz"))
63 {
64 len += 20;
65 BTOR_NEWN (btor->mm, cmd, len);
66 sprintf (cmd, "gzip -c > %s", name);
67 if ((file = popen (cmd, "w"))) btor->close_apitrace = 2;
68 BTOR_DELETEN (btor->mm, cmd, len);
69 }
70 else
71 {
72 if ((file = fopen (name, "w"))) btor->close_apitrace = 1;
73 }
74
75 if (file)
76 btor->apitrace = file;
77 else
78 printf ("[boolector] WARNING failed to write API trace file to '%s'", name);
79 }
80