From 1323530001e685f51eb9fa953f97a138690b92f5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Thu, 21 May 2026 08:55:10 -0700 Subject: [PATCH] tptp: share 0-arity decls across sorts to fix bare constant equality (#9587) Fix the TPTP frontend so that a bare name used in an equality refers to a single shared `func_decl`, regardless of how the surrounding context coerces its sort. ## Problem With the following input the conjecture was not proved: ```tptp fof(a1,axiom, ! [X] : (X = a)). fof(c1,conjecture, b = a). ``` `parse_atomic_formula` created bare names as 0-arity **Bool predicates**, and `coerce_eq` later retyped them by calling `m.mk_func_decl(...)` directly, without registering the result in `m_decls`. So the `a` used inside `! [X] : (X = a)` (coerced to sort `U`) and the `a` used inside `b = a` (left as Bool) ended up as two unrelated `func_decl`s sharing only the name. The axiom no longer constrained the conjecture. ## Fix In `src/cmd_context/tptp_frontend.cpp`: 1. Add `mk_zero_arity_decl(name, range)` / `coerce_zero_arity(app*, range)` helpers that memoize the 0-arity `func_decl` per `(name, target sort)` in `m_decls`, delegating to the existing `mk_decl_or_ho_const` for `U` and Bool targets. 2. Rewrite `coerce_eq` to use the new helpers and add an explicit Bool / non-Bool retyping branch so a bare-Bool side is recast to the other side's sort. 3. In `parse_atomic_formula`, when a bare name is immediately followed by `=` or `!=`, create it as a non-predicate (sort `U`). Terms in equalities are no longer first introduced as Bool predicates. 4. Reorder the constructor init-list so `m_univ` is initialized before the pinned ref vectors (matches declaration order; silences `-Wreorder`). Net effect: every reference to a given name at a given sort yields the same `func_decl`, eliminating duplicate-symbol bugs in equalities over bare TPTP constants. ## Test Added `fof-bare-constant-equality` to `src/test/tptp.cpp`. Without the C++ change the new case asserts; with it, `./build/release/test-z3 /seq tptp` reports `PASS`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/cmd_context/tptp_frontend.cpp | 51 ++++++++++++++++++++++--------- src/test/tptp.cpp | 4 +++ 2 files changed, 40 insertions(+), 15 deletions(-) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index aab7278ec..d5dc49152 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -966,6 +966,25 @@ class tptp_parser { return parse_term_primary(); } + func_decl* mk_zero_arity_decl(symbol const& name, sort* range) { + std::string name_str = name.str(); + if (range == m_univ) + return mk_decl_or_ho_const(name_str, 0, false); + if (m.is_bool(range)) + return mk_decl_or_ho_const(name_str, 0, true); + std::string key = mk_decl_key(name_str, 0, 'c') + "\x1f" + std::to_string(range->get_id()); + auto it = m_decls.find(key); + if (it != m_decls.end()) return it->second; + func_decl* f = m.mk_func_decl(name, 0, static_cast(nullptr), range); + m_pinned_decls.push_back(f); + m_decls.emplace(key, f); + return f; + } + + expr_ref coerce_zero_arity(app* a, sort* range) { + return expr_ref(m.mk_const(mk_zero_arity_decl(a->get_decl()->get_name(), range)), m); + } + // Build an arithmetic expression from a TPTP function name and arguments // Coerce two expressions to have the same sort for equality. // If sorts already match, returns lhs unchanged. Otherwise coerces the @@ -973,28 +992,25 @@ class tptp_parser { // coerces both to m_univ. expr_ref coerce_eq(expr_ref lhs, expr_ref& rhs) { if (lhs->get_sort() == rhs->get_sort()) return lhs; - // Try coercing one side (0-arity constants can be reinterpreted) + if (is_app(lhs) && to_app(lhs)->get_num_args() == 0 && m.is_bool(lhs->get_sort()) && !m.is_bool(rhs->get_sort())) + return coerce_zero_arity(to_app(lhs), rhs->get_sort()); + if (is_app(rhs) && to_app(rhs)->get_num_args() == 0 && m.is_bool(rhs->get_sort()) && !m.is_bool(lhs->get_sort())) { + rhs = coerce_zero_arity(to_app(rhs), lhs->get_sort()); + return lhs; + } if (is_app(lhs) && to_app(lhs)->get_num_args() == 0 && lhs->get_sort() != rhs->get_sort()) { - func_decl* fd = m.mk_func_decl(to_app(lhs)->get_decl()->get_name(), 0, static_cast(nullptr), rhs->get_sort()); - m_pinned_decls.push_back(fd); - return expr_ref(m.mk_const(fd), m); + return coerce_zero_arity(to_app(lhs), rhs->get_sort()); } if (is_app(rhs) && to_app(rhs)->get_num_args() == 0 && lhs->get_sort() != rhs->get_sort()) { - func_decl* fd = m.mk_func_decl(to_app(rhs)->get_decl()->get_name(), 0, static_cast(nullptr), lhs->get_sort()); - m_pinned_decls.push_back(fd); - rhs = m.mk_const(fd); + rhs = coerce_zero_arity(to_app(rhs), lhs->get_sort()); return lhs; } // Last resort: coerce both to m_univ if (is_app(lhs) && to_app(lhs)->get_num_args() == 0) { - func_decl* fd = m.mk_func_decl(to_app(lhs)->get_decl()->get_name(), 0, static_cast(nullptr), m_univ); - m_pinned_decls.push_back(fd); - lhs = m.mk_const(fd); + lhs = coerce_zero_arity(to_app(lhs), m_univ); } if (is_app(rhs) && to_app(rhs)->get_num_args() == 0) { - func_decl* fd = m.mk_func_decl(to_app(rhs)->get_decl()->get_name(), 0, static_cast(nullptr), m_univ); - m_pinned_decls.push_back(fd); - rhs = m.mk_const(fd); + rhs = coerce_zero_arity(to_app(rhs), m_univ); } return lhs; } @@ -1072,6 +1088,11 @@ class tptp_parser { return expr_ref(args.empty() ? m.mk_const(f) : m.mk_app(f, args.size(), args.data()), m); } + if (args.empty() && (is(token_kind::equal_tok) || is(token_kind::neq_tok))) { + func_decl* f = mk_decl_or_ho_const(n, 0, false); + return expr_ref(m.mk_const(f), m); + } + func_decl* pred = mk_decl_or_ho_const(n, args.size(), true); if (!args.empty()) coerce_args(pred, args); return expr_ref(args.empty() ? m.mk_const(pred) : m.mk_app(pred, args.size(), args.data()), m); @@ -1372,10 +1393,10 @@ public: m(m_cmd.m()), m_arith(m), m_array(m), + m_univ(m.mk_uninterpreted_sort(symbol("U"))), m_pinned_sorts(m), m_pinned_decls(m), - m_pinned_exprs(m), - m_univ(m.mk_uninterpreted_sort(symbol("U"))) { + m_pinned_exprs(m) { m_pinned_sorts.push_back(m_univ); sort* tType = m.mk_uninterpreted_sort(symbol("$tType")); m_pinned_sorts.push_back(tType); diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp index 6b7bdf1b7..3f611cf30 100644 --- a/src/test/tptp.cpp +++ b/src/test/tptp.cpp @@ -73,6 +73,10 @@ fof(c1,conjecture, p(a)).)", R"(cnf(c1,axiom, p(X)). cnf(c2,axiom, ~ p(a)).)", "% SZS status Unsatisfiable"}, + {"fof-bare-constant-equality", +R"(fof(a1,axiom, ! [X] : (X = a)). +fof(c1,conjecture, b = a).)", + "% SZS status Theorem"}, {"tff-negative-literal", R"(tff(c1,conjecture, $less(-2,2)).)", "% SZS status Theorem"},