always output TFF in TPTP proofs

[shalashaska117]

Fixes #730, taking the approach @MichaelRawson suggested there.

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 "does this proof need TFF". 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)).

Two related cases, both fixed here. ! [X: $int] : $is_int(X) gave an fof formula containing a typed quantifier:

fof(f1,conjecture,(
  ! [X0 : $int] : $is_int(X0)),
  file('quant.p',c1)).

And because type declarations are printed from the signature, which only grows, while the language choice came from the units, which shrink, one proof could contain both languages. checks/theory/let-tuple-bool.p already did this on master.

What changed

getFofString and ProofCheckPrinter::printStep print tff, or thf for higher-order problems, without consulting the property. TFF subsumes FOF, and Shell/TPTPPrinter.cpp already printed tff unconditionally.

getQuantifiedStr annotates a variable whose sort is not $i regardless of the property, which is the predicate Formula::toString already uses. That path only covers clause variables and I could not build a case where the old code misprinted, so treat it as consistency rather than part of the fix.

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

Testing

• checks/sanity passes, 68 checks, built against Z3 4.14.0.
• Unit tests: 96 of 97 pass. Inferences_HOL_Injectivity fails identically with and without this change on 3677326, so it is not from here.
• Captured -p tptp output for all 32 problems under checks/Problems, hol/hol1.p, the FOOL problems and three smtlib2 inputs, before and after. Every SZS status is unchanged. 36 outputs are byte identical, 16 differ only in fof( becoming tff(, and 3 differ only in clause numbering, which the unpatched binary also does when run twice on those problems.
• checks/ucore/test2.out still matches exactly.
• Higher-order output is still thf, and -p proofcheck is fixed the same way.
• The four new check_no_fof lines in checks/sanity all fail without this change and pass with it.

I do not have tptp4X to hand, so I have not checked the output against a strict TPTP parser. Worth noting Vampire's own parser accepts fof(f1,conjecture,($is_int(6))), so reading proofs back through Vampire does not catch the old behaviour.

[MichaelRawson]

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

[MichaelRawson]

In future we could consider just printing $i, it's not illegal any more because we never use fof.

[MichaelRawson]

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]

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]

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]

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

[shalashaska117]

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]

@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]

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]

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]

@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]

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.