mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 23:25:36 +00:00
Code Activity

Polish TPTP frontend keys/path checks and deduplicate skip logic

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/ba80bc5a-d80f-4d9f-8ed4-a962f697697c

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-08 17:28:27 +00:00 • committed by GitHub
parent 4ac41292d6
commit 91e864914a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 14 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/shell/main.cpp
View file

@ -134,8 +134,8 @@ static bool validate_is_ulong(char const* s) {
}
static bool is_tptp_extension(char const* ext) {
static char const* exts[] = {"p", "tptp", "fof", "cnf", "tff", "thf"};
for (char const* known_ext : exts) {
static char const* tptp_extensions[] = {"p", "tptp", "fof", "cnf", "tff", "thf"};
for (char const* known_ext : tptp_extensions) {
if (strcmp(ext, known_ext) == 0)
return true;
}

20
src/shell/tptp_frontend.cpp
View file

@ -322,7 +322,7 @@ class tptp_parser {
}
static std::string mk_decl_key(std::string const& name, unsigned arity, char tag) {
return std::to_string(name.size()) + ":" + name + ":" + std::to_string(arity) + ":" + tag;
return std::to_string(name.size()) + ":" + name + "\x1f" + std::to_string(arity) + "\x1f" + tag;
}
static std::string mk_typed_key(std::string const& name, unsigned arity) {
@ -432,6 +432,15 @@ class tptp_parser {
}
}
void skip_balanced(token_kind open_k, token_kind close_k) {
int depth = 1;
while (depth > 0 && !is(token_kind::eof_tok)) {
if (accept(open_k)) ++depth;
else if (accept(close_k)) --depth;
else next();
}
}
z3::expr parse_term();
z3::expr parse_term_primary() {
@ -612,7 +621,7 @@ class tptp_parser {
static bool is_absolute_path(std::string const& name) {
return !name.empty() &&
(name[0] == '/' ||
(name.size() > 2 && std::isalpha(static_cast<unsigned char>(name[0])) && name[1] == ':'));
(name.size() >= 2 && std::isalpha(static_cast<unsigned char>(name[0])) && name[1] == ':'));
}
std::string dirname(std::string const& f) const {
@ -638,12 +647,7 @@ class tptp_parser {
std::string file = parse_name();
if (accept(token_kind::comma)) {
if (accept(token_kind::lbrack)) {
int depth = 1;
while (depth > 0 && !is(token_kind::eof_tok)) {
if (accept(token_kind::lbrack)) ++depth;
else if (accept(token_kind::rbrack)) --depth;
else next();
}
skip_balanced(token_kind::lbrack, token_kind::rbrack);
}
else {
skip_annotations_until_rparen();