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