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 #ifndef BTORTRAPI_H_INCLUDED
9 #define BTORTRAPI_H_INCLUDED
10 
11 #include "btorcore.h"
12 #include <stdio.h>
13 
14 #define BTOR_TRAPI_NODE_FMT "n%d@%p "
15 #define BTOR_TRAPI_SORT_FMT "s%d@%p "
16 
17 #define BTOR_TRAPI_NODE_ID(exp)                                               \
18   (btor_node_is_inverted (exp) ? -btor_node_real_addr (exp)->id : (exp)->id), \
19       btor_node_real_addr (exp)->btor
20 
21 #define BTOR_TRAPI_PRINT(args...)    \
22   do                                 \
23   {                                  \
24     if (!btor->apitrace) break;      \
25     btor_trapi_print (btor, ##args); \
26   } while (0)
27 
28 #define BTOR_TRAPI(args...)                  \
29   do                                         \
30   {                                          \
31     if (!btor->apitrace) break;              \
32     btor_trapi (btor, __FUNCTION__, ##args); \
33   } while (0)
34 
35 #define BTOR_TRAPI_AUX(fun, args...) \
36   do                                 \
37   {                                  \
38     if (!btor->apitrace) break;      \
39     btor_trapi (btor, fun, ##args);  \
40   } while (0)
41 
42 #define BTOR_TRAPI_RETURN(args...) \
43   do                               \
44   {                                \
45     if (!btor->apitrace) break;    \
46     btor_trapi (btor, 0, ##args);  \
47   } while (0)
48 
49 #define BTOR_TRAPI_UNFUN_EXT(exp, fmt, args...) \
50   BTOR_TRAPI (BTOR_TRAPI_NODE_FMT fmt, BTOR_TRAPI_NODE_ID (exp), ##args)
51 
52 #define BTOR_TRAPI_UNFUN(exp) \
53   BTOR_TRAPI (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (exp))
54 
55 #define BTOR_TRAPI_BINFUN(e0, e1)                      \
56   BTOR_TRAPI (BTOR_TRAPI_NODE_FMT BTOR_TRAPI_NODE_FMT, \
57               BTOR_TRAPI_NODE_ID (e0),                 \
58               BTOR_TRAPI_NODE_ID (e1))
59 
60 #define BTOR_TRAPI_TERFUN(e0, e1, e2)                                      \
61   BTOR_TRAPI (BTOR_TRAPI_NODE_FMT BTOR_TRAPI_NODE_FMT BTOR_TRAPI_NODE_FMT, \
62               BTOR_TRAPI_NODE_ID (e0),                                     \
63               BTOR_TRAPI_NODE_ID (e1),                                     \
64               BTOR_TRAPI_NODE_ID (e2))
65 
66 #define BTOR_TRAPI_RETURN_NODE(res)                                      \
67   do                                                                     \
68   {                                                                      \
69     if (res)                                                             \
70     {                                                                    \
71       BTOR_TRAPI_RETURN (BTOR_TRAPI_NODE_FMT, BTOR_TRAPI_NODE_ID (res)); \
72     }                                                                    \
73     else                                                                 \
74     {                                                                    \
75       BTOR_TRAPI_RETURN ("(nil)@%p");                                    \
76     }                                                                    \
77   } while (0)
78 
79 #define BTOR_TRAPI_RETURN_PTR(res) BTOR_TRAPI_RETURN ("%p", res)
80 
81 #define BTOR_TRAPI_RETURN_STR(res) BTOR_TRAPI_RETURN ("%s", res)
82 
83 #define BTOR_TRAPI_RETURN_INT(res) BTOR_TRAPI_RETURN ("%d", res)
84 
85 #define BTOR_TRAPI_RETURN_UINT(res) BTOR_TRAPI_RETURN ("%u", res)
86 
87 #define BTOR_TRAPI_RETURN_BOOL(res) \
88   BTOR_TRAPI_RETURN ("%s", (res) ? "true" : "false")
89 
90 #define BTOR_TRAPI_RETURN_SORT(sort) \
91   BTOR_TRAPI_RETURN (BTOR_TRAPI_SORT_FMT, sort, btor)
92 
93 void btor_trapi_print (Btor *btor, const char *msg, ...);
94 
95 void btor_trapi (Btor* btor, const char* fname, const char* msg, ...);
96 
97 void btor_trapi_open_trace (Btor* btor, const char* name);
98 #endif
99