summaryrefslogtreecommitdiff
path: root/proofs/lfsc_checker/print_smt2.h
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/lfsc_checker/print_smt2.h')
-rw-r--r--proofs/lfsc_checker/print_smt2.h17
1 files changed, 17 insertions, 0 deletions
diff --git a/proofs/lfsc_checker/print_smt2.h b/proofs/lfsc_checker/print_smt2.h
new file mode 100644
index 000000000..c70b1dfa4
--- /dev/null
+++ b/proofs/lfsc_checker/print_smt2.h
@@ -0,0 +1,17 @@
+#ifndef PRINT_SMT2_H
+#define PRINT_SMT2_H
+
+#define PRINT_SMT2
+
+#include "expr.h"
+
+#ifdef PRINT_SMT2
+void print_smt2( Expr* p, std::ostream& s, short mode = 0 );
+
+bool is_smt2_poly_formula( Expr* p );
+short get_mode( Expr* p );
+
+#endif
+
+
+#endif
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback