build $let definitions of Boolean symbols as formulas

[shalashaska117]

Fixes #863.

TPTP::endLet built the definition with Term::create(symbol, args). When the $let binds a Boolean symbol, symbol is a predicate number, so Term::create looked it up in the function half of the signature: Signature::functionArity then indexed past the end of the function stack. In a debug build it trips the bounds assertion in Lib::Stack::operator[], in a release build it segfaults.

SMTLIB2::parseLet already handles this, with a comment about preserving the term-formula boundary, so this makes the TPTP parser do the same thing.

Shadowing is not the cause

The issue puts it down to shadowing, and SWX006_1.p does shadow bad, max and i repeatedly, but shadowing turns out to be irrelevant. This is enough on its own:

tff(c,conjecture, $let(p: $o, p := $true, p ) ).

Any $let over a Boolean symbol crashes on master, shadowing or not, fresh name or not. SWX006_1.p is just the first problem anyone ran into that contains one.

With the fix, SWX006_1.p gives SZS status Theorem, which matches its TPTP header, and --show_everything on no longer dies while printing.

A separate problem this uncovers

Once the crash is gone, -newcnf on gives a wrong answer for a conjecture holding two or more Boolean $lets. It reports CounterSatisfiable for this theorem:

tff(q,type, q: $o ).
tff(c,conjecture,
    ( $let(b: $o, b := ( q | ~ q ), b )
    & $let(d: $o, d := ( q | ~ q ), d ) ) ).

That one predates this change and I have left it alone. NewCNF gets the same shape from the SMT-LIB parser, which has always built Boolean let definitions this way, so it reproduces on master with no parser change at all:

(set-logic ALL)
(declare-fun q () Bool)
(assert (not (and (let ((b (or q (not q)))) b) (let ((d (or q (not q)))) d))))
(check-sat)

vampire --input_syntax smtlib2 -newcnf on answers Satisfiable, on master and with this branch alike, where the default clausifier answers Unsatisfiable. A single Boolean $let is fine in both. Worth its own issue, and I am happy to file one with the reduction if that helps.

The regression tests below therefore use one Boolean $let per file, so they pass in all four clausifier configurations instead of encoding the NewCNF bug as expected behaviour.

Testing

• checks/theory/let-bool.p (nullary) and checks/theory/let-bool-pred.p (arity 1), each shadowing a global of the same name, both under the default clausifier and -newcnf on, with and without -ile off. All eight combinations give Theorem with the fix and segfault without it. checks/theory/let-bool-simultaneous.p covers two symbols bound in one $let, so endLet builds a definition per symbol; on master that one is a sort error rather than a crash.
• Other shapes I ran by hand, each Theorem in default, -newcnf on and -ile off, each a segfault on master: predicate of arity 2, a Boolean $let nested in another one's definition, a Boolean $let under an outer quantifier whose definition uses the bound variable, a Boolean $let whose body rebinds the same name again, and two Boolean symbols bound simultaneously.
• Two shapes I could not get to the changed code at all: $let(p: !>[A: $tType]: A > $o, ...) and its implicit form $let(p: A > $o, ...). Both are rejected earlier with a User error, identically on master and on this branch. So the iTypeArgs part of the new args.size() is not covered by anything I could construct, and I have left that path as it was.
• checks/sanity passes, 74 checks, built against Z3 4.14.0.
• Unit tests: 96 of 97 pass. Inferences_HOL_Injectivity fails the same way with Parse/TPTP.cpp reverted, so it is not from here.
• Debug build, assertions on, over the new tests and the existing theory/let-*.p ones. Nothing fires on the new tests. theory/let-tuple-bool.p in default mode does trip Shell/LispParser.hpp:109, but it does so on master too: the TPTP parser raises its own "set --newcnf on if using tuples" error, auto mode then falls back to SMT-LIB, and the Lisp parser asserts on the way out. That is presumably why checks/sanity only runs the tuple tests with -newcnf on.

[mezpusz]

Sorry for not being able to look at this earlier. My tests suggests that this solves 5 TPTP crashes. Great work!

[mezpusz]

@shalashaska117 Regarding the issue with -newcnf on in the section "A separate problem this uncovers", could you please file an issue?

[shalashaska117]

@shalashaska117 Regarding the issue with -newcnf on in the section "A separate problem this uncovers", could you please file an issue?

I will, being Vampire a project so big I thought that issues in non-main branches were not worth being published

[mezpusz]

I will, being Vampire a project so big I thought that issues in non-main branches were not worth being published

As far as I understand this already affects master when using SMTLIB, but merging this will also affect it when parsing TPTP, right?

[shalashaska117]

I will, being Vampire a project so big I thought that issues in non-main branches were not worth being published

As far as I understand this already affects master when using SMTLIB, but merging this will also affect it when parsing TPTP, right?

Yes, just it was not exposed

[mezpusz]

For full closure I ran some tests with -newcnf on too and there are 33 problems that previously crashed but now they don't. 🎉