mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-21 06:25:50 +00:00
Code Activity

update release.yml and tptp_frontend

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-14 11:16:47 -07:00
parent e2b9e3a6dc
commit c4cb5bbc15
2 changed files with 14 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/cmd_context/tptp_frontend.cpp
View file

@ -1508,7 +1508,7 @@ class tptp_parser {
// For function-style definitions, wraps value in lambdas over the parameter variables.
std::pair<std::string, expr_ref> parse_single_let_defn() {
std::string name = parse_name();
std::vector<app*> param_vars;
ptr_vector<app> param_vars;
std::unordered_map<std::string, app*> param_scope;
if (accept(token_kind::lparen)) {
if (!accept(token_kind::rparen)) {
@ -2947,13 +2947,9 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) {
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());
dout << "(set-param :pi.avoid_skolems false)\n";
ctx.get_solver()->display(dout);
dout << "(check-sat)\n";
}
}