Fixes soundness/completeness of the TPTP frontend for polymorphic (TF1/TH1)
problems, reducing TPTP-v9.2.1 BUG verdicts from 28 to 4.
* Treat regular-forall "! [A: $tType] : ..." as genuine type quantification
(bind A via mk_type_var) instead of monomorphizing it to the universe sort.
This is the standard THF/TH1 way to quantify over types, and monomorphizing
it silently prevented theory_polymorphism from instantiating the axioms.
* Use the plain smt solver (mk_smt_solver_factory) for problems that contain
type variables. The strategic solver's tactic preprocessing eliminates the
unconstrained conjecture instance before the core can link it to its
polymorphic axiom, yielding a spurious CounterSatisfiable.
* Detect value-indexed dependent type families ("T > $tType"), which the
parametric-polymorphism encoding cannot represent soundly, and downgrade
both sat and unsat verdicts to GaveUp (previously produced unsound Theorems,
e.g. SEV600/601/602).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
A double-quoted TPTP token such as "138" is a distinct object, and a
single-quoted '138' is a functor name; neither is an arithmetic numeral.
parse_name() strips the quotes, so the subsequent is_nonempty_digit_string
check was converting them into Int literals (then boxed Int->U),
mis-encoding distinct objects as equal numbers. Guard both numeral checks
(parse_term_primary and the atomic-formula parser) with !m_last_name_quoted
so only bare unquoted digit tokens become numerals.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Three translation defects in tptp_frontend.cpp caused spurious sat/unsat
verdicts (reported as SZS BUG against annotated status):
- Parenthesized negation bound the whole disjunction: ( ~ p | q ) parsed
as ~(p | q) instead of (~p) | q, flipping nearly every CNF/FOF clause.
Negate only the next unary unit, then resume precedence parsing via a
new parse_binary_rest helper.
- Quantifier bodies absorbed lower-precedence connectives: ! [X] : p(X) => g
parsed as ! [X] : (p(X) => g). TPTP quantifiers bind tighter than the
binary connectives, so parse the body at parse_expr(PREC_EQ).
- Mixed Int/Real equality coerced through an uninterpreted box function,
severing arithmetic semantics and yielding spurious models. Use the
arithmetic to_real/to_int conversions instead.
Add regression cases to src/test/tptp.cpp covering all three fixes.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
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>
Discussion #9524 reported systematic TPTP result polarity errors
(notably `Unsatisfiable/Theorem` cases returned as `Satisfiable`) and
timeout-path instability in the frontend. The dominant issue was
semantic: free variables in FOF/CNF formulas were parsed as constants
instead of implicitly universally quantified variables.
- **Parser semantics: free variables now follow TPTP rules**
- In `/home/runner/work/z3/z3/src/cmd_context/tptp_frontend.cpp`, free
variables encountered while parsing an annotated formula are now
collected in formula scope and wrapped with a top-level `forall`.
- This applies to both term and atomic-formula paths, so variable
occurrences are treated consistently.
- Explicitly bound quantifier variables continue to take precedence over
implicit ones.
- **Scoped implementation cleanup**
- Added scoped state for implicit-variable collection to avoid leaking
parser state across formulas.
- Kept variable binding order stable so quantifier construction is
deterministic.
- **Timeout-path robustness**
- Updated frontend exception catches to `const&` in the TPTP stream
entrypoint to make timeout/error handling behavior consistent with
thrown exception forms.
- **Regression tests**
- Extended `/home/runner/work/z3/z3/src/test/tptp.cpp` with focused
cases for:
- FOF free-variable implicit universal quantification.
- CNF free-variable implicit universal quantification.
```tptp
cnf(c1,axiom, p(X)).
cnf(c2,axiom, ~ p(a)).
```
This now maps to `forall X. p(X)` plus `~p(a)`, yielding `% SZS status
Unsatisfiable` as expected.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This PR targets the main TFF frontend parsing failures: bare numeric
atoms were being treated as uninterpreted terms (`U`) in formula
position, decimal literals were not parsed, and `$uminus` was not
recognized as an arithmetic builtin. These issues caused widespread
parse/type failures in arithmetic-heavy TPTP inputs.
- **Numeric atom parsing in formulas (TFF)**
- Added a shared numeric-literal parser path for term/formula contexts.
- In atomic formulas, numeric LHS now parses as arithmetic numerals
before `=`/`!=` handling, avoiding `U` vs `Int/Real` mismatches.
- **Decimal literal support**
- Extended numeral parsing to accept `d.d` forms and construct `Real`
numerals.
- Keeps existing integer (`d`) and rational (`d/d`) behavior on the same
code path.
- **`$uminus` builtin support**
- Added explicit handling for `$uminus(<arg>)` in term parsing.
- Enforces arity 1 and arithmetic-argument checks; maps directly to
arithmetic unary minus.
- **Focused regression coverage**
- Added/updated TPTP unit cases for:
- bare integer inequality: `31 != 12`
- decimal arithmetic literal usage
- `$uminus` in arithmetic predicates
Example of now-supported inputs:
```tptp
tff(c1,conjecture, 31 != 12).
tff(c2,conjecture, ~ $less(-3.25,-8.69)).
tff(c3,conjecture, $less($uminus(2),0)).
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
