1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 #ifndef TRACING_H_
20 #define TRACING_H_
21
22 #include "mcsat/plugin.h"
23 #include <stdio.h>
24
25 /** Check if the tag is enabled */
26 static inline
ctx_trace_enabled(const plugin_context_t * ctx,const char * tag)27 bool ctx_trace_enabled(const plugin_context_t* ctx, const char* tag) {
28 #ifndef NDEBUG
29 return (ctx->tracer != NULL && tracing_tag(ctx->tracer, tag));
30 #else
31 return false;
32 #endif
33 }
34
35 /** Check if the tag is enabled */
36 static inline
trace_enabled(tracer_t * tracer,const char * tag)37 bool trace_enabled(tracer_t* tracer, const char* tag) {
38 #ifndef NDEBUG
39 return (tracer != NULL && tracing_tag(tracer, tag));
40 #else
41 return false;
42 #endif
43 }
44
45 /** Return the file associated with the trace */
46 static inline
ctx_trace_out(const plugin_context_t * ctx)47 FILE* ctx_trace_out(const plugin_context_t* ctx) {
48 if (ctx->tracer != NULL && ctx->tracer->file != NULL) {
49 return ctx->tracer->file;
50 } else {
51 return stderr;
52 }
53 }
54
55 /** Return the file associated with the trace */
56 static inline
trace_out(tracer_t * tracer)57 FILE* trace_out(tracer_t* tracer) {
58 if (tracer != NULL && tracer->file != NULL) {
59 return tracer->file;
60 } else {
61 return stderr;
62 }
63 }
64
65 /** Print the term to a file */
66 void term_print_to_file(FILE* out, term_table_t* terms, term_t t);
67
68 /** Print the term to the trace (with newline) */
69 void trace_term_ln(tracer_t* tracer, term_table_t* terms, term_t t);
70
71 /** Print the term to the trace */
72 void ctx_trace_term(const plugin_context_t* ctx, term_t t);
73
74 /** Print to the trace */
75 void mcsat_trace_printf(tracer_t* tracer, const char* format, ...) __attribute__ ((format (printf, 2, 3)));
76
77 /** Print to the trace */
78 void ctx_trace_printf(const plugin_context_t* ctx, const char* format, ...) __attribute__ ((format (printf, 2, 3)));
79
80 /** String representation of the kind */
81 const char* kind_to_string(term_kind_t kind);
82
83 /** String representation of the type */
84 const char* type_to_string(type_kind_t kind);
85
86 #endif /* TRACING_H_ */
87