output proofs in the TPTP fragment of the input problem by shalashaska117 · Pull Request #884 · vprover/vampire

shalashaska117 · 2026-07-25T14:22:54Z

Fixes #730.

InferenceStore chose between fof and tff using Problem::hasNonDefaultSorts(). That property is recomputed from the current unit list (refreshProperty calls Property::scan(_units)), so it answers "do the units I am holding right now mention a non-$i sort" rather than "which fragment was the input problem in". Preprocessing can delete the last unit mentioning a sort, and the property then reports an untyped problem while the proof still contains typed formulas.

The eight problems listed in #730 hit this. The conjecture normalizes to ~$true, the arithmetic disappears, and the proof comes out as:

fof(f1,conjecture,(
  $is_int(6)),
  file('ARI496_1.p',mixed_types_problem_1)).

What changed

The first version of this PR printed tff unconditionally, as @MichaelRawson suggested in #730. It is now the union of that and @mezpusz's counter-proposal on fix-output-tptp-fragment:

Problem records initiallyHasNonDefaultSorts and initiallyHigherOrder when the input problem is set, and the proof printers pick fof, tff or thf from those flags. A pure FOF problem keeps its fof proof.
Variable annotations use a per-formula test (t != defaultSort() || initiallyHasNonDefaultSorts()) in getQuantifiedStr and Formula::toString, so a $int variable surviving in a proof step never prints bare and reads back as $i.
The getQuantifiedStr overload without a sort map is gone. It passed a static DHMap that nothing ever filled, and printGeneralSplittingComponent went through it: ALWAYS(t_map.find(var,t)) on an empty map is undefined behaviour in release, and the general splitting definitions printed their variables without sorts either way. The definition printer now collects the sorts from the clause.
FunctionRelationshipInference swaps the main problem twice during FMB sort bound detection, which runs after preprocessing, so the flags got recomputed from the preprocessed units and the bug came back for fmb strategies. Those two calls now skip the recording (isInputProblem=false).
outputSymbolTypeDeclarationIfNeeded follows the saved flags, and the proof printers skip type declarations entirely when the recorded fragment is fof. The signature can hold a typed symbol that no unit ever used, and its declaration would put a tff line in front of an fof proof.

-p on, -p smtcheck and -p smt2_proofcheck are untouched, and SAT steps from AVATAR still print as cnf.

Testing

checks/sanity passes. The new checks test both directions: no fof in the proofs of ARI496_1 and mixed-language.p, only fof for PUZ001+1 and for a problem whose signature holds an unused typed symbol, and sort annotations on the gsp definitions (checks/proof/gsp-typed.p fails on master).
97/97 unit tests pass in debug, plus assertion-enabled runs including -sa fmb -fmbdsb on.
-p tptp over the checks problems against master: ARI496_1, let-bool.p and mixed-language.p change fof( to tff(, unused-typed-symbol.p drops the unused declaration, every SZS status is unchanged, and the remaining outputs are identical up to the clause renumbering master already shows between runs.

I still have not checked the output against a strict TPTP parser like tptp4X; Vampire's own parser accepted the broken proofs, so round-tripping through Vampire does not catch the old behaviour.

The proof output language was chosen with hasNonDefaultSorts(), which Problem recomputes from its current unit list. Preprocessing can remove the last unit mentioning a sort, and the property then reports an untyped problem while the proof still contains typed formulas. For the problems in vprover#730 the conjecture normalizes to ~$true, so the arithmetic disappears and the proof is printed as fof even though it contains $is_int. Type declarations are printed from the signature, which only grows, so the two could also disagree inside one proof, giving a tff type declaration followed by fof formulas. TFF subsumes FOF, so print tff unconditionally, or thf for higher-order problems, and drop the property test. TPTPPrinter already did this. Also annotate a quantified variable whose sort is not $i even when the property is false, to match Formula::toString.

MichaelRawson

Cool! I intend to merge after asking a few people about it.

MichaelRawson · 2026-07-29T07:52:22Z

Unit tests: 96 of 97 pass. Inferences_HOL_Injectivity fails identically with and without this change on 3677326, so it is not from here.

This doesn't seem good: CI passes this test. What system are you using?

shalashaska117 · 2026-07-29T07:54:22Z

Unit tests: 96 of 97 pass. Inferences_HOL_Injectivity fails identically with and without this change on 3677326, so it is not from here.

This doesn't seem good: CI passes this test. What system are you using?

I don't understand it either, I get the same error on main, I used Ubuntu latest version, now I'm not at the computer so can't see the exact version

MichaelRawson · 2026-07-29T08:07:43Z

Uh-oh. Experience suggests that a compiler upgrade finally found a bug that was lurking - if you can, please try to debug the unit test. Otherwise I guess we'll let it play out.

MichaelRawson · 2026-07-29T08:08:22Z

(but it's independent of this change of course, don't worry!)

shalashaska117 · 2026-07-29T08:09:18Z

Uh-oh. Experience suggests that a compiler upgrade finally found a bug that was lurking - if you can, please try to debug the unit test. Otherwise I guess we'll let it play out.

I will work on it today.

shalashaska117 · 2026-07-29T12:05:13Z

@MichaelRawson success_3's expected clause was wrong (copy-pasted from success_2), and clang only hides it because it evaluates the two sides of the != in the opposite order to gcc, which makes the produced clause share a subterm with the expected one, and the test comparator returns true on identical subterms without checking that the variable renaming is consistent.

mezpusz · 2026-07-29T13:48:48Z

I also like the fix, but I think the issue could also happen for thf problems, and we probably don't want to go full thf if we don't have to. I'm proposing to instead save the initial value of the flags that are used to output fof/tff/thf. More generally, we could do a per formula scanning before printing to use the weakest possible fragment we need, but this is probably expensive. Anyways, going weaker is currently allowed by Geoff Sutcliffe, while going stronger is not, so we should be careful here.

I will open a separate PR with my proposed solution, so that we can discuss.

shalashaska117 · 2026-07-29T18:09:49Z

I also like the fix, but I think the issue could also happen for thf problems, and we probably don't want to go full thf if we don't have to. I'm proposing to instead save the initial value of the flags that are used to output fof/tff/thf. More generally, we could do a per formula scanning before printing to use the weakest possible fragment we need, but this is probably expensive. Anyways, going weaker is currently allowed by Geoff Sutcliffe, while going stronger is not, so we should be careful here.

I will open a separate PR with my proposed solution, so that we can discuss.

I am very curious about your solution, I will look into it

shalashaska117 · 2026-07-29T21:07:37Z

@mezpusz do you have any test idea that I could try to verify your claim about thf problems? trying something but I don't know how to check for all cases to be honest, so if you have better ideas to try to point to errors that I could not find

mezpusz · 2026-07-30T07:31:42Z

I've checked it now with an "unsound" preprocessing step that just replaces all units with $false. The point is that we have to remove all higher-order constructs already in preprocessing. As expected the output contained fof in all output lines (except for type declarations, where we get tff).

I pushed the changes for the alternative solution to fix-output-tptp-fragment, I will run some tests before opening a PR.

shalashaska117 · 2026-08-03T13:02:50Z

@mezpusz any news about how to solve this problem?

mezpusz · 2026-08-03T13:41:57Z

@shalashaska117 This is my proposed solution but I need to clear out a few other TPTP issues before I can verify that it works.

@mezpusz

Problem::hasNonDefaultSorts() and Problem::isHigherOrder() are recomputed from the current unit list, so when preprocessing removed the last typed or higher-order unit the proof came out in the wrong language. Instead of always printing tff, record both flags when the parsed problem is set as the main problem and pick fof, tff or thf from the recorded values. The proof stays in the fragment of the input: untyped problems keep fof, and originally higher-order problems keep thf even when preprocessing removes every higher-order construct. Recording the flags was suggested by @mezpusz in the vprover#884 discussion. Variable sort annotations keep the per-formula test (annotate whenever the sort is not $i), so a typed variable is never printed bare, and symbol type declarations follow the same recorded flag as the proof steps, so one proof cannot mix languages. FunctionRelationshipInference temporarily swaps the main problem during FMB sort bound detection, which runs after preprocessing; its two setMainProblem calls pass isInputProblem=false so the recorded fragment survives the swap.

printGeneralSplittingComponent passed getQuantifiedStr a static sort map that nothing ever filled, so the variables of a definition introduced by -gsp on printed without sorts, and a $int variable read back as $i. Collect the sorts from the clause instead, and remove the map-less overload, which is now unused. The proof printers also printed symbol type declarations when the proof itself is fof: the signature can hold a typed symbol that no unit ever used, and its declaration put a tff line in front of an fof proof. Skip the declarations when the recorded fragment is fof.

shalashaska117 · 2026-08-05T20:09:03Z

@mezpusz I went through fix-output-tptp-fragment and I think the two fixes combine well: your saved flags decide the fof/tff/thf header, and the per-formula test from this PR keeps the variable annotations right. I've pushed the union to this branch. Three things I ran into while reading your diff:

getQuantifiedStr still reads env.getMainProblem()->hasNonDefaultSorts() while its comment says initiallyHasNonDefaultSorts, so clause printing keeps the stale-property bug: a proof step that still contains a $int variable prints it bare, and it reads back as $i. I used the per-formula test (t != defaultSort() || initiallyHasNonDefaultSorts()) there and in Formula::toString, so a typed variable never loses its annotation.
ALWAYS(t_map.find(var,t)) fails on -gsp on proofs: the getQuantifiedStr overload without a map passed a static DHMap that nothing ever filled, and printGeneralSplittingComponent went through it. In release ALWAYS(Cond) is if (!(Cond)) __UNREACHABLE, so a failed find is undefined behaviour. The empty map was a bug of its own: general splitting definitions printed their variables without sorts, checks/proof/gsp-typed.p shows it. The definition printer now collects the sorts from the clause, and the map-less overload is gone.
FunctionRelationshipInference swaps the main problem twice during FMB sort bound detection, which runs after preprocessing, so the saved flags got recomputed from the preprocessed unit list and the bug came back for fmb strategies. Those two calls now skip the recording (isInputProblem=false).

Two more changes in the same area: outputSymbolTypeDeclarationIfNeeded now follows the saved flag, otherwise an originally higher-order problem whose constructs are all eliminated in preprocessing prints thf steps with tff type declarations. And the proof printers skip type declarations entirely when the recorded fragment is fof, since the signature can hold a typed symbol that no unit ever used, whose declaration would put a tff line in front of an fof proof.

checks/sanity now tests both directions: no fof in the proofs of ARI496_1 and mixed-language.p, only fof for PUZ001+1 and for the unused typed declaration, and sort annotations on the gsp definitions. Against master, -p tptp over the checks problems changes ARI496_1, let-bool.p and mixed-language.p (fof to tff) and unused-typed-symbol.p (drops the declaration of the unused symbol); every SZS status is unchanged and the remaining outputs are identical up to the clause renumbering master already shows between runs. 97/97 unit tests pass.

mezpusz · 2026-08-06T07:47:50Z

getQuantifiedStr still reads env.getMainProblem()->hasNonDefaultSorts() while its comment says initiallyHasNonDefaultSorts

Good catch!

ALWAYS(t_map.find(var,t)) fails on -gsp on proofs

The point of this assertion was to enforce callers to fill the map, otherwise @MichaelRawson might know why we want UB in case the assertion fails in release.

I used the per-formula test (t != defaultSort() || initiallyHasNonDefaultSorts()) there and in Formula::toString, so a typed variable never loses its annotation.

I think it should never happen that initiallyHasNonDefaultSorts()==false and we introduce non-default sorts during preprocessing, so this should rather be an assertion too.

shalashaska117 · 2026-08-06T07:55:26Z

ALWAYS(t_map.find(var,t)) fails on -gsp on proofs

The point of this assertion was to enforce callers to fill the map, otherwise @MichaelRawson might know why we want UB in case the assertion fails in release.

Wouldn't this create more problems?

I used the per-formula test (t != defaultSort() || initiallyHasNonDefaultSorts()) there and in Formula::toString, so a typed variable never loses its annotation.

I think it should never happen that initiallyHasNonDefaultSorts()==false and we introduce non-default sorts during preprocessing, so this should rather be an assertion too.

I can check this easily, but in my test it never occurred. Easy fix to the code.

MichaelRawson · 2026-08-06T13:53:54Z

The point of this assertion was to enforce callers to fill the map, otherwise @MichaelRawson might know why we want UB in case the assertion fails in release.

I defined ASS and friends to hint unreachability in a release build because it allows certain optimisations (or did something at the time, I'm not sure now). There was a small performance improvement, but I'm not attached to it - so if you prefer it can go.

Consider e.g.

void f(int x) {
  if(x < 0) throw Exception("expected positive integer");
  // ....
}

void g(int y) {
  ASS(y > 0)
  f(y);
  // ...
}

When inlining f into g, the optimiser can reason that y > 0 (otherwise UB), so the conditional branch and the exception setup can disappear altogether.

shalashaska117 · 2026-08-06T16:29:35Z

@mezpusz agreed on the assertion. I'll add

ASS(t == AtomicSort::defaultSort() || env.initiallyHasNonDefaultSorts());

at the two sites of the per-formula test (InferenceStore.cpp and Formula::toString). I'd keep the disjunction as the print condition though: in release ASS compiles to {} (Debug/Assertion.hpp), so it costs nothing, and if some future preprocessing rule does introduce a non-default sort into an initially untyped problem, a release build prints the variable with its sort instead of dropping the annotation, which is the failure mode this PR is about. Debug builds fail the assertion and the rule gets found.

I could not come up with a counterexample either: theory axioms, induction and FOOL elimination all need the sorts to be in the problem already. For some confidence beyond that I'll run a debug build with the assertion over checks/ and a batch of TPTP FOF problems with -gsp on, -newcnf on and -sa fmb -fmbdsb on before pushing.

On ALWAYS(t_map.find(var,t)): dropping the map-less overload keeps the contract, it just moves it to compile time. Every caller now has to build a filled map, and the ALWAYS in the remaining overload holds because printGeneralSplittingComponent collects the sorts from the clause.

@MichaelRawson thanks for the explanation. One detail: in release only ALWAYS/NEVER/ASSERTION_VIOLATION expand to __UNREACHABLE, plain ASS is {}, so the optimisation only concerns those three. Either way it looks independent of this PR, so I left the macros alone.

A non-default sort should never appear in a proof step of an initially untyped problem: every preprocessing step that builds sorted terms (theory axioms, induction, FOOL elimination) needs the sorts to be in the input already. Assert this in getQuantifiedStr and Formula::toString instead of relying on it silently. The disjunction stays as the print condition: ASS compiles to nothing in release, and if a future rule ever breaks the invariant, a release build prints the variable with its sort instead of dropping the annotation and changing the formula, while a debug build fails the assertion and points at the rule.

shalashaska117 · 2026-08-06T16:50:48Z

Pushed the assertion in 5bf5aa6: ASS(t == AtomicSort::defaultSort() || env.initiallyHasNonDefaultSorts()) now guards both per-formula sites, and the disjunction stays as the release print condition as discussed above.

Validation: 97/97 unit tests in debug, checks/sanity with both the debug and the release build, and a sweep of the debug build over 158 problems in four configs (default, -gsp on, -newcnf on, -sa fmb -fmbdsb on, all with -p tptp -t 10): 42 bushy MPTP2078 FOF problems, 53 typed and mixed TPTP problems, and the 63 files under checks/. Of the 632 runs, 220 printed refutations and 5 printed finite models; the new assertion never fired.

The sweep did surface two debug assertion failures that already exist on master (reproduced at 3677326), so they are not from this PR:

UIHelper.cpp:546, ASS(!s_expecting_unsat): some bushy MPTP2078 problems whose header says Status : Theorem come out CounterSatisfiable (MPT0651+1 by saturation even in the default config, MPT1151+1 / MPT1451+1 / MPT1501+1 / MPT1751+1 as fmb models). If those problems are really countersatisfiable the headers are at fault rather than the solver, but either way a debug build dies on the mismatch instead of reporting it.
LispParser.hpp:109, ASS(e->isList()): when auto input_syntax fails to parse a file as TPTP (for example tuples without -newcnf on, or thf) and falls back to SMTLIB2, the lisp parser asserts on the non-SMTLIB text instead of raising a user error.

I can open issues for these if they are not already known.

The previous run died before starting: the job was never acquired by a hosted runner.

MichaelRawson · 2026-08-07T08:24:54Z

@MichaelRawson thanks for the explanation. One detail: in release only ALWAYS/NEVER/ASSERTION_VIOLATION expand to __UNREACHABLE, plain ASS is {}, so the optimisation only concerns those three. Either way it looks independent of this PR, so I left the macros alone.

Oops, yes - evaluating the ASS condition in release is more expensive than it's worth. Whereas the semantics of ALWAYS and so on requires evaluating the condition anyhow.

shalashaska117 mentioned this pull request Jul 25, 2026

Wrong TPTP output for arithmetic problems #730

Open

shalashaska117 force-pushed the tff-proof-output branch from cc068d0 to f7b3617 Compare July 25, 2026 14:27

shalashaska117 changed the title ~~always output TFF rather than FOF in TPTP proofs~~ always output TFF in TPTP proofs Jul 25, 2026

MichaelRawson approved these changes Jul 29, 2026

View reviewed changes

Comment thread Kernel/InferenceStore.cpp Outdated

shalashaska117 mentioned this pull request Jul 29, 2026

eqModACRect accepts clauses that are not equal up to renaming; Injectivity success_3 fails on gcc #889

Closed

shalashaska117 added 3 commits August 5, 2026 21:17

Merge remote-tracking branch 'origin/master' into tff-proof-output-union

b53ef2c

shalashaska117 changed the title ~~always output TFF in TPTP proofs~~ output proofs in the TPTP fragment of the input problem Aug 5, 2026

retrigger ci

ba33e5a

The previous run died before starting: the job was never acquired by a hosted runner.

Uh oh!

Conversation

shalashaska117 commented Jul 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What changed

Testing

Uh oh!

MichaelRawson left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

MichaelRawson commented Jul 29, 2026

Uh oh!

shalashaska117 commented Jul 29, 2026

Uh oh!

MichaelRawson commented Jul 29, 2026

Uh oh!

MichaelRawson commented Jul 29, 2026

Uh oh!

shalashaska117 commented Jul 29, 2026

Uh oh!

shalashaska117 commented Jul 29, 2026

Uh oh!

mezpusz commented Jul 29, 2026

Uh oh!

shalashaska117 commented Jul 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

shalashaska117 commented Jul 29, 2026

Uh oh!

mezpusz commented Jul 30, 2026

Uh oh!

shalashaska117 commented Aug 3, 2026

Uh oh!

mezpusz commented Aug 3, 2026

Uh oh!

shalashaska117 commented Aug 5, 2026

Uh oh!

mezpusz commented Aug 6, 2026

Uh oh!

shalashaska117 commented Aug 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MichaelRawson commented Aug 6, 2026

Uh oh!

shalashaska117 commented Aug 6, 2026

Uh oh!

shalashaska117 commented Aug 6, 2026

Uh oh!

MichaelRawson commented Aug 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

shalashaska117 commented Jul 25, 2026 •

edited

Loading

shalashaska117 commented Jul 29, 2026 •

edited

Loading

shalashaska117 commented Aug 6, 2026 •

edited

Loading