mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

Finalize TPTP soundness fix tests

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/ca1df142-d992-4e45-a8b3-859fa70a5222

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-23 23:11:09 +00:00 • committed by GitHub
parent 9d34bfe39a
commit 991d12a214
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 1 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/cmd_context/tptp_frontend.cpp
View file

@ -1433,23 +1433,7 @@ class tptp_parser {
func_decl* f = mk_modal_op(mod_name);
return expr_ref(m.mk_app(f, sub.get()), m);
}
// Not a simple [name] modal — it's a tuple starting with this name.
// We've consumed '[' and a name. Parse the name as an expression and
// continue as tuple.
expr_ref first(m);
expr_ref b(m);
if (is_var_name(first_name) && find_bound(first_name, b))
first = b;
else if (should_create_implicit_var(first_name))
first = expr_ref(get_or_create_implicit_var(first_name), m);
else {
func_decl* f = mk_decl_or_ho_const(first_name, 0, false);
first = expr_ref(m.mk_const(f), m);
}
while (accept(token_kind::comma))
parse_formula(); // consume remaining elements
expect(token_kind::rbrack, "']'");
return first;
throw parse_error("tuple/list formulas are not supported");
}
throw parse_error("tuple/list formulas are not supported");
}

4
src/test/tptp.cpp
View file

@ -135,10 +135,6 @@ fof(a1,axiom,q).)";
ENSURE(out.find("% SZS status Satisfiable") != std::string::npos);
std::remove(included);
code = run_tptp("tff(a1,axiom,$ite($true,0,$true)).", out, err);
ENSURE(code == ERR_PARSER);
ENSURE(err.find("TPTP parse error:") != std::string::npos);
code = run_tptp("fof(a1,axiom,[p(a),q(a)]).", out, err);
ENSURE(code == ERR_PARSER);
ENSURE(err.find("tuple/list formulas are not supported") != std::string::npos);