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

tptp: share 0-arity decls across sorts to fix bare constant equality (#9587)

Browse source 
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>
This commit is contained in:
Lev Nachmanson 2026-05-21 08:55:10 -07:00 • committed by GitHub
parent 43791ebf2a
commit 1323530001
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 40 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

51
src/cmd_context/tptp_frontend.cpp
View file

@ -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<sort**>(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<sort**>(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<sort**>(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<sort**>(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<sort**>(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);

4
src/test/tptp.cpp
View file

@ -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"},