mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

include code for dumpign tptp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-05 13:53:53 -07:00
parent 835679b27d
commit e20945c743
1 changed files with 20 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/cmd_context/tptp_frontend.cpp
View file

@ -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);