From e20945c7436d9cc0d332f765905e191046a69596 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Jul 2026 13:53:53 -0700 Subject: [PATCH] include code for dumpign tptp Signed-off-by: Nikolaj Bjorner --- src/cmd_context/tptp_frontend.cpp | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index ba04b29200..1bfd0e0117 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -14,6 +14,7 @@ #include "util/z3_exception.h" #include "ast/arith_decl_plugin.h" #include "ast/array_decl_plugin.h" +#include "ast/decl_collector.h" #include "ast/expr_abstract.h" #include "ast/ast_util.h" #include "ast/polymorphism_util.h" @@ -2928,6 +2929,25 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) { ctx.set_solver_factory(mk_smt_strategic_solver_factory()); + // Optional: dump the parsed goal as an SMT-LIB2 benchmark (env Z3_TPTP_DUMP_SMT2 + // gives the output file path). Used to produce SMTLIB versions of TPTP instances. + if (char const* dump_path = getenv("Z3_TPTP_DUMP_SMT2")) { + std::ofstream dout(dump_path); + if (dout) { + ast_manager& m = ctx.m(); + dout << "; Auto-generated from TPTP input: " + << (current_file ? current_file : "?") << "\n"; + dout << "(set-logic ALL)\n"; + decl_collector decls(m); + for (expr* a : ctx.assertions()) + decls.visit(a); + for (sort* s : decls.get_sorts()) + if (m.is_uninterp(s) && s->get_num_parameters() == 0) + dout << "(declare-sort " << s->get_name() << " 0)\n"; + ctx.display_smt2_benchmark(dout, ctx.assertions().size(), ctx.assertions().data()); + } + } + // Suppress default check-sat output; TPTP frontend reports SZS status explicitly. std::ostringstream sink; scoped_regular_stream scoped_stream(ctx, sink);