Allows FMB output to hold symbolic definitions and FMB's model_check mode to read a use them - #914
Open
quickbeam123 wants to merge 53 commits into
Open
Allows FMB output to hold symbolic definitions and FMB's model_check mode to read a use them#914quickbeam123 wants to merge 53 commits into
quickbeam123 wants to merge 53 commits into
Conversation
… symbolic ones; will crash in corner cases
Defect 1: the closing ")." of the function_<name> conjunction was printed outside the arity>0 branch, so every explicitly represented constant emitted a stray ")." line after its <name>_definition axiom, making the model syntactically invalid. Defect 2: the predicate printing loop never set first=false, so the conjuncts of predicate_<name> were printed without the "&" separators. Reproducer (before this commit both defects visible in the printed model): ./vampire -sa fmb -t 30 <problem with a constant and a unary predicate> e.g. fof(a1,axiom,p(c)). fof(a2,axiom,![X]:(p(X)=>p(f(X)))). fof(a3,axiom,?[X]:~p(X)). The printed model now parses (checked via --mode clausify on the model text). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ctionsAndPredicates Since initTables started marking usageCnt()==0 symbols as NOT_REPRESENTED, the four reencode loops in eliminateSortFunctionsAndPredicates still walked every signature symbol, tripping ASS_EQ(var,_f_offsets[f]) on the first unrepresented one (and, in release, indexing the old tables at SIZE_MAX). Such symbols have no table in either encoding, so they are now skipped (with an assert that representedness did not change). Also assert that the eliminated sort functions/predicates themselves are represented, and widen the linear reencoding counters from unsigned to size_t to match the offsets. Reproducer (assertion violation at FiniteModelMultiSorted.cpp:532 before this commit): script -q /dev/null ./vampire -sa fmb -t 30 --fmb_adjust_sorts function <file> on a TFF problem where updr eliminates a predicate definition (making q and f unrepresented) and a second sort is non-monotonic, e.g.: tff(s_type,type,s:$tType). tff(t_type,type,t:$tType). tff(c_type,type,c:s). tff(d1_type,type,d1:t). tff(d2_type,type,d2:t). tff(f_type,type,f:s>s). tff(p_type,type,p:s>$o). tff(q_type,type,q:s>$o). tff(r_type,type,r:t>$o). tff(a1,axiom,p(c)). tff(a2,axiom,![X:s]:(q(X)<=>p(f(X)))). tff(a3,axiom,?[X:s]:~p(X)). tff(a5,axiom,![Y:t]:(Y=d1|Y=d2)). tff(a6,axiom,r(d1)&~r(d2)). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The base-k "odometer" pattern for enumerating a symbol's argument tuples in table order (first position fastest, all-1s start, body running at least once so that constants/propositions are covered) was hand-rolled at ten places in FiniteModelMultiSorted.cpp and twice in FiniteModelBuilder::onModelFound. This introduces FMB/ArgsEnumerator.hpp with a do/while protocol, bounds derived either from an OperatorType plus sort sizes or given explicitly, and a nextAndRebind/bindAll variant that keeps a var->element substitution in sync (used by the restore loops and FORALL/EXISTS evaluation). Pure refactor: model output verified byte-identical on 40 satisfiable TPTP problems (-sa fmb -t 6 --fmb_adjust_sorts function), with a same-binary double-run diff first to rule out nondeterminism. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Replace the two monolithic interpretation arrays plus per-symbol offsets (_f_offsets/_f_interpretation, _p_offsets/_p_interpretation) by per-symbol tables (_f_tables/_p_tables); an empty table now *is* the "not represented" marker, retiring the NOT_REPRESENTED sentinel and the offset arithmetic. args2var becomes the offset-free tableIndex; full-table passes (restoreImplicitlyEliminated*, restoreGlobalPredicateFlip) become plain linear scans, and the table walks in toString and the sort-elimination reencoding run linearly with a debug assert tying the running index to tableIndex (resolving an old TODO). The per-symbol representation is also what later allows materializing a single symbol's table lazily without touching (or copying) any other. Pure refactor: model output verified byte-identical on the same 40 satisfiable TPTP problems as the previous commit (-sa fmb -t 6 --fmb_adjust_sorts function). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
evaluateTerm/evaluateLiteral used to index straight into a symbol's table; for an unrepresented (eliminated) symbol the table is empty, so any evaluation touching one -- e.g. a COND_FLIP condition mentioning an eliminated predicate during restoreEliminatedDefinitions -- crashed. Now evaluation falls back to the recorded symbolic definition (FunDef/ PredDef), binding the head variables to the argument values in a local substitution and recursing into the body (which may itself mention further symbolically defined symbols; the chain is acyclic by elimination order). An implicitly eliminated symbol without a record gets a trivial definition created and remembered on first demand, via the new symbolicFunDef/ symbolicPredDef helpers also used by toString -- so what is printed and what is evaluated always agree. Reproducer (before this commit: assertion "idx < tbl.size()" inside evaluateTerm/evaluateLiteral; after it the same run proceeds to the not yet supported flip-target write, fixed in the next commit): script -q /dev/null ./vampire -sa fmb -t 30 -updr off -bce on <sortelim.p> where sortelim.p is the TFF problem from the previous commit's message. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ls at the end of the replay A flip must write into an explicit table, so when a COND_FLIP targets an unrepresented predicate (e.g. one whose clauses BCE eliminated), its table is now materialized right before the flip -- allocated per-symbol (cheap, thanks to the subtables) and filled by evaluating the recorded symbolic definition, or trivially when there is none (materializeFun/materializePred; the fun variant will serve the upcoming model self-check). Recorded definitions referencing a later-flipped predicate are deliberately NOT frozen -- lazy evaluation reroutes through the post-flip values; the soundness argument per interference kind, including why GLOB_FLIPs (replayed first, now asserted) are exempt, is documented at restoreEliminatedDefinitions. The "restore implicitly eliminated symbols after each interference" loops are gone: reads of undefined table cells consistently return the default (function value 1 / false), all flip writes are absolute, and one defaulting pass at the end of the replay makes the leftovers explicit for printing. evaluate() now resets the undefined-symbol bookkeeping on entry, keeping its partial-model error (relevant in model_check mode) per-unit. Reproducer (before this commit: assertion "idx < tbl.size()", with tbl.size()==0, in restoreViaCondFlip): script -q /dev/null ./vampire -sa fmb -t 30 -updr off -bce on <sortelim.p> with sortelim.p from two commits ago; now produces a full model with q materialized, satisfying the original q(X) <=> p(f(X)). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…sage initTables gives no table to symbols with usageCnt()==0, but onModelFound still recorded a SAT value for every non-deleted symbol -- crashing (in debug; out-of-bounds in release) on symbols introduced during FMB's own preprocessing after the Property scan that counts usage, e.g. the fmbFreshConstant-s of SortInference or the fmbdef-s of DefinitionIntroduction. Such symbols are introduced() (never printed), cannot occur in the original formulas nor in recorded interference bodies, so their values cannot matter; skip them, mirroring initTables. (Monotonicity, by contrast, deliberately bumps the usage of the sort functions/predicates it introduces, so those do keep their tables, which eliminateSortFunctionsAndPredicates later reads.) Reproducer (before this commit, debug build: assertion "idx < tbl.size()" in addFunctionDefinition, on functor fmbFreshConstant90): script -q /dev/null ./vampire -sa fmb -t 20 Problems/TOP/TOP008-1.p Also fixes, among others, CAT020-4, KRS031+1, KRS045+1, GRP393-2, SWV920-10, SYN750-1, SYN769-1, SYN770-1 the same way. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Guarded by the (for now enabled) compile-time macro FMB_CHECK_MODEL_AGAINST_INPUT in FiniteModelMultiSorted.hpp -- an assert-like instrument for stress-testing the symbolic-definitions work, to be set to 0 (or removed) later; deliberately no option, no samplers entry, single-strategy mode only. Under the macro, preprocessProblem (vampire.cpp) snapshots the parsed input units into the Problem before preprocessing (units are immutable, so a list copy suffices), and onModelFound, after restoreEliminatedDefinitions, evaluates every original unit in the restored model: non-conjecture units must hold, the conjecture must not (the model witnesses its negation); a violation raises USER_ERROR (exit 4) naming the unit. Units our evaluator cannot handle (FOOL constructs in the un-preprocessed input) are skipped with a count. evaluate() now universally closes formula units, so implicitly quantified fof inputs check correctly. Detection verified by temporarily sabotaging the COND_FLIP replay (skip the flip): the check then fails exactly on the axiom whose satisfaction depends on the flip, ./vampire -sa fmb -t 30 -updr off -bce on <sortelim.p> -> "FMB model self-check FAILED on: ! [X0 : s] : (q(X0) <=> p(f(X0)))". Passes on the sampled satisfiable TPTP problems locally (incl. --random_polarities on, -bce on, --fmb_adjust_sorts variants); the full CNF/FOF/TF0 sweep is to run on the server. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Adds checks/fmb/sortelim.p, a compact problem exercising, per configuration:
symbolic model definitions for an updr-eliminated predicate (and the
implicitly eliminated function it takes along), sort-function/-predicate
elimination reencoding tables in the presence of unrepresented symbols
(--fmb_adjust_sorts function/predicate), GLOB_FLIP replay
(--random_polarities on), and blocked-clause COND_FLIP replay with target
materialization (-updr off -bce on).
Three SZS status checks give crash coverage; two check_exact_output entries
pin the entire printed model (with --statistics none the stdout is
deterministic), which is the strong end-to-end check: a model self-check
failure ("User error" after the SZS status line) or a wrong table shows up
as a diff, which the status grep alone would miss. Expected files generated
with a Release build of this commit's tree and verified byte-identical
against the debug build; all five checks pass when the helper functions are
sourced and run standalone.
The .out files contain the "% FMB model self-check passed" line of the
temporary FMB_CHECK_MODEL_AGAINST_INPUT instrument and need regenerating
when that macro is retired (noted in the sanity script).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
With -fmbes contour, the size of the found model is read back off the
sort marker variables ("retracted"), because the model may be smaller
than the assumed contour. For monotonic sorts, however, the markers say
nothing about the model: addNewInstances doesn't mark instances of a
monotonic sort at all and addNewTotalityDefs only emits the weakest
version of the totality clause, so all markers except the one being
assumed occur only in the marker ladder -- which "all false" satisfies.
Whether the solver happens to return such an assignment then decides
whether we print a bogus model: the domain gets shrunk to a size at
which no model exists (and out-of-domain values end up in the tables,
since onModelFound queries the solver within the un-retracted box).
Skip monotonic sorts in the retraction loop; the assumed contour value
is the size of the model we found.
Pre-fix reproducer (both options needed; also fails on master):
./vampire --decode fmb+10_1_sas=cadical:fmbes=contour_10 \
Problems/NLP/NLP200+1.p
reports "% TRYING [1]" ... "% TRYING [7]" -- i.e. sizes 1..6 are UNSAT --
and then prints a one-element model. See also the sanity check added in
a follow-up commit.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A model table is indexed by 1-based domain elements, and a function's value is a domain element too, but nothing checked either. The previous commit's bug wrote out-of-domain values into the tables and only showed up much later, as an out-of-range read of the domain-constant names while printing (Lib/DArray.hpp: "Condition n < _size was violated"). Check both on the spot: tableIndex asserts each argument is within its sort (an oversized argument in a non-final position can otherwise wrap into a perfectly valid row index) and addFunctionDefinition asserts the recorded value is a domain element of the result sort. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A two-line problem over a monotonic sort that needs two domain elements: before the fix two commits ago, -fmbes contour with -sas cadical printed a one-element model for it (and, in a debug build, tripped the new assertion with an out-of-domain value for b). Pin the whole model, and require both SAT solvers to produce it -- which of the two exposed the bug was pure luck of the assignment. As with fmb/sortelim*.out, the expected outputs were generated with a Release build and contain the "FMB model self-check passed" line of the temporary FMB_CHECK_MODEL_AGAINST_INPUT instrument; they need regenerating when that macro is retired. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The local variable "monotonic" is initialised from _assumeMonotonic and never updated with the result of Monotonicity::check(), so the guard "monotonic && !_assumeMonotonic" was unsatisfiable and the "Input sort X is monotonic" line could never be printed -- exactly the information one wants when debugging the monotonic-sort handling in the FMB encoding. Report based on what ended up in _monotonic_vampire_sorts instead. ./vampire --show_fmb_sort_info on -sa fmb checks/fmb/sortelim.p now says "Input sort s is monotonic" (and stays silent about t, which has positive variable equalities), where it used to say nothing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Pinning the entire printed model of fmb/sortelim.p makes every unrelated change to model printing a CI failure -- too fragile for what these checks are for. The problem file itself is worth keeping, so only the two check_exact_output entries and their .out files go; the SZS status checks stay, plus a new one for the -updr off -bce on configuration (COND_FLIP replay and materialization of the flip target), which was covered by the removed exact-output check alone. fmb/monotonic-contour.out stays: there check_szs_status genuinely cannot see the defect, since a model of the wrong domain size is still reported Satisfiable. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The model of a problem using only declared sorts still opened with a
one-element $i domain:
tff('declare_$i1',type,'fmb_$i_1':$i).
tff('finite_domain_$i',axiom, ! [X:$i] : ( X = 'fmb_$i_1' ) ).
although FMB never modelled $i there (see "% TRYING [1,1]" for
checks/fmb/sortelim.p: two distinct sorts, s and t). onModelFound
defaulted the size of every sort to 1 and only overrode it for sorts
sort inference had given a distinct sort to, and toString prints a
domain for every sort of nonzero size. Default to 0 instead -- "this
model says nothing about that sort" -- which is what the neighbouring
line already did for the unused interpreted sorts, and which toString
already skips. $o keeps its 1, so that boolean-sorted terms behave
exactly as before.
A represented symbol can never mention such a sort: del_f/del_p is
usageCnt()==0, which is also initTables' criterion for "not
represented", and sort inference walks precisely the non-deleted
symbols. Where a value of a domain-less sort is nevertheless called for
(the flip and materialization loops may enumerate over the sorts of an
eliminated symbol's variables), it now uniformly acts as a one-element
domain: that is what ArgsEnumerator's do/while already does with a 0
bound, and what tableSize already did with a 0-sized dimension, but
tableIndex would have made the stride of the following positions 0.
Both now go through a small domainSize() helper.
Also initialise ModelCheck's sortSizesArray, which is only written for
the sorts a model file mentions: models legitimately omit sorts now, and
the rest of the array was uninitialised memory.
./vampire --mode model_check <problem + its model> now round-trips a
model with no $i section; ./vampire -sa fmb checks/fmb/sortelim.p prints
the same model as before minus the $i block, under the default,
--fmb_adjust_sorts function/predicate and -updr off -bce on.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Reading an undefined table cell used to be recorded into
_implicitlyEliminatedFunctions/-Predicates and answered with a made-up
value (the first domain element, resp. a false atom); only once the
whole unit had been evaluated did a non-empty set become a generic
User error: Encountered an undefined symbol while evaluating a Unit
(a partial model?)
So the invented value could travel through an entire formula before
anything complained, the offending symbol was known at the point of the
read but thrown away, and the sets were never used for anything but
their emptiness.
Throw an UndefinedValueException carrying the symbol's name right where
the cell is read instead, and let the two callers of evaluate() say what
it means, which differs sharply between them: a model loaded from a file
is simply partial (a user error), while a model we have just built
ourselves being partial is our own bug (INVALID_OPERATION). Note this
also makes such a read an error during the interference replay, where it
used to be silently absorbed as a don't-care -- deliberately, since we
should never construct a partial model. It does not happen: 80 problems
x {default, -updr off -bce on} run clean.
Before: User error: Encountered an undefined symbol ... (a partial model?)
After: User error: The loaded model is partial: no value for p
(needed to evaluate the above)
reproducible by feeding --mode model_check a problem plus a model that
declares but never defines p (the "Checking <unit>..." line printed just
above names the unit).
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
CliqueFinder::findMaxCliqueSize searches downwards over the number of neighbours i, where a clique has size i+1, but stopped at i>1 -- so it could never report 2, and returned 1 for every triangle-free graph. FMB uses it on the "these constants are pairwise different" graph collected from ground unit disequalities, to lower-bound the model size. The bound was therefore only ever found for three or more mutually distinct constants: $ echo 'fof(a,axiom, a!=b).' > two.p $ ./vampire -sa fmb two.p % Detected minimum model sizes of [1] % TRYING [1] % TRYING [2] while the same file with a!=b & a!=c & b!=c correctly reported [3]. With i>0 the pair is found, and one round of the search is saved. This matters especially for $o: TheoryAxioms::applyFOOL adds $$true != $$false, so the boolean domain now comes out as min = max = 2 without any hardwiring, and FMB goes straight to the only size it can have. The new unit test fails on the previous commit (single_edge: 1 != 2). CliqueFinder.hpp also gains the includes it always used but relied on its includers for. NB: this changes FMB's starting sizes on every problem with two mutually distinct constants, so it wants a wide re-run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
$ cat chichi.p
tff(a, axiom, ![X:$o]:?[Y:$o]:(X=Y)).
$ ./vampire -sa fmb chichi.p
% Finite Model Found!
% SZS status Satisfiable for chichi
Condition n < _size at location ./Lib/DArray.hpp:102 was violated, as:
n == 1
_size == 0
The model itself was fine ($o of size 2, with $$false and $$true on its
two elements): it was toString that broke. Its sort loop skips every
sort with isInterpretedNonDefault, which covers $o, so cnames[$o] was
never filled -- and the function loop then printed the definitions of the
$$true / $$false constants and indexed that empty array. (The dead
sortNameLabel = isBoolCon(s) ? "bool" : sortName line just above the skip
suggests the loop was once meant to handle $o.)
FMB needs nothing special to model $o: FOOLElimination compiles the FOOL
away, and TheoryAxioms::applyFOOL supplies $$true != $$false together
with ![X:$o]: X = $$true | X = $$false, which is exactly what pins the
domain to two elements. So let $o through the skip and print it, with
its two elements named by FOOL's term-level booleans -- $true and $false,
via Signature::functionName, so -show_fool on still shows the internal
$$true / $$false. Which element is which is what the model says about
those two constants, so read it off there. No type declarations are
emitted for them (they are built-in), and their own definitions are
skipped in the function loop, being the tautologies $true = $true and
$false = $false. What remains announces that the boolean domain was
considered, and fixes how the tables spell its elements:
tff(finite_domain_bool,axiom,
! [X:$o] : (
X = $false | X = $true
) ).
tff(distinct_domain_bool,axiom,
$false != $true
).
tff(declare_g,type,g : ( $o * $i ) > $i).
tff(function_g,axiom,
g($false,'fmb_$i_1') = 'fmb_$i_2'
& g($true,'fmb_$i_1') = 'fmb_$i_1'
...
$o accordingly loses its exception in onModelFound's sort sizing: it is
now either genuinely modelled, and takes its size from sort inference
like everything else, or truly absent, and a size of 1 would make the new
branch try to print a one-element boolean domain. The printing also
moves inside the partial-model catcher, as it now evaluates.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
ModelCheck collects the domain constants of each sort into a Set<Term*> and then *enumerates* that set to number them 1..n -- which decides the whole of --mode model_check's output, and the table indices behind it. DefaultHash hashes a Term* by address, so the bucket layout, and with it the numbering, changed from run to run: $ for i in 1 2 3 4 5; do ./vampire --mode model_check b4.mc.p | md5; done 776ea9b7b1a9703b6e0fddc4c062149d 776ea9b7b1a9703b6e0fddc4c062149d 776ea9b7b1a9703b6e0fddc4c062149d 023347f8c9ff5c5c2e3706ba6b5ef526 dface64a6cb997ae98368a104f4556ec Hash the shared terms by Term::getId() instead (SharedTermHash, see the note in Kernel/Term.hpp), so the constants come out in the order the model file introduces them. The neighbouring DHMap<Term*,unsigned> is only ever looked up, never enumerated, so its hashing does not matter. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Neither the self-check instrument nor --mode model_check could deal with a $o problem, because the parser stores $true and $false in term position as a special FORMULA term (in TPTP they are formulas, and only FOOL lets them stand as terms), and the whole term-level FOOL fragment was simply refused: - checkModelAgainstOriginalInput reported "0 units checked, 3 skipped as not evaluable" for a problem whose every axiom mentions $true, i.e. it verified nothing on exactly the problems the previous commit enables; - --mode model_check SIGSEGVed on such a model or problem, calling functionArity on a special functor. evaluateTerm now evaluates a formula in term position and returns the domain element the corresponding FOOL constant sits on, and evaluateFormula gains the dual, BOOL_TERM. That covers more than $true and $false: a symbol declared f: $i > $o is a predicate to the parser, so "f(a) = $true" is an equality between two $formula(...) terms. The remaining FOOL constructs ($ite, $let, ...) now say so, through the USER_ERROR that evaluateFormula's default case already used. Where a model is read rather than evaluated -- ModelCheck's domain constants and definition arguments -- what is wanted is the constant, not its value, so a syntactic deFool() does that job; and a special term surviving it is reported instead of dereferenced. ModelCheck also has to count the FOOL constants as used before the model sizes its tables: the parser never builds them as constants, so nothing else does. Finally, the finite_domain axiom's disjuncts are now parenthesised. They have to be for $o, since our own parser reads ! [X:$o] : ( X = $false | X = $true ) as X = ($false | X = $true), which made our own printed model unreadable; doing it for every sort keeps one code path (and costs the pinned checks/fmb/monotonic-contour.out one line). ./vampire -sa fmb checks/fmb/bool.p now self-checks 3 units, and its model fed back through --mode model_check (checks/fmb/bool.check.p) says "All formulas evaluated to True!" -- on the previous commit it aborts by SIGSEGV. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
TheoryAxioms::applyFOOL returns before adding the boolean domain axiom ![X:$o]: X = $$true | X = $$false when FOOLParamodulation is on, leaving that job to the inference rule. FMB has no such rule, so it would happily build a boolean domain of three or more elements -- and until now it silently did: $ ./vampire -sa fmb -foolp on chichi.p % TRYING [1] % TRYING [2] % Finite Model Found! with no minimum/maximum sizes detected at all (with foolp off the same run detects min = max = 2 and goes straight there). Make it a hard constraint, in the shape of the neighbouring one for -sas z3. No samplers/*.smp change needed: only samplerFOL.smp and samplerFNT.smp sample sa=fmb, and both already gate foolp behind sa!=fmb. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
checks/fmb/bool.p uses $o as a result sort (f: $i > $o), as an argument sort (g: ($o * $i) > $i) and in the domain block, and keeps all three alive through preprocessing. Exact output, because the point of the preceding commits is precisely how the boolean domain and its two elements are printed; and a round-trip of that very model back through --mode model_check (checks/fmb/bool.check.p, regenerable from bool.out), because a printed model has to be re-readable -- the unbracketed finite_domain axiom was not. As for monotonic-contour, the "FMB model self-check passed" line in the .out comes from the temporary FMB_CHECK_MODEL_AGAINST_INPUT instrument and will need regenerating when that macro is retired. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
./vampire --decode fmb+10_1_sas=cadical:si=on:rpr=on:pels=off:bce=on:\
rp=on:peltl=2.81238:pel=on:random_seed=13:fmbsr=1.87847:nm=14:rtra=on_10 \
Problems/PRO/PRO007+4.p --random_seed 10
% SZS status CounterSatisfiable for PRO007+4
User error: FMB model self-check FAILED on: 15. ! [X0,X1] :
(? [X2] : (occurrence_of(X0,X2) & atomic(X2) & subactivity(X1,X2)) <=> atocc(X0,X1))
Two interferences meet here. PredicateDefinition halved axiom 15's <=>
into "atocc(X0,X1) => RHS" and recorded a CondFlip on atocc: wherever RHS
holds, set atocc true. Much later PredicateElimination eliminated atomic
and, posMulti being 0, built its definition fromPos -- a disjunction over
the 15 positive clauses, one of which is "~atocc(X0,X1) | atomic(sK7(X0))",
contributing "? [X1,X2] : (sK7(X1) = X0 & atocc(X1,X2))". So atomic's
recorded body reads atocc.
UPDR runs early and PEL late, so the atocc flip sits at the bottom of the
LIFO stack and is replayed last, with atomic already in _symbolicPreds.
restoreViaCondFlip then re-evaluates its condition per grounding, that
condition mentions atomic, and atomic reroutes into the very table the
loop is writing: it chases a moving target, and neither direction of
axiom 15 survives. (The same shape occurs a second time in that run: the
BCE flip targets root_occ, and sP0's recorded body reads root_occ.)
A flip's soundness argument is "the model differing from this one *only*
on p, as prescribed, is a model of the problem as it was before this
step". A lazily recorded definition reading p breaks that "only". So
prepareForFlip now materializes p's readers first; materializing changes
no values, it only stops them shifting under the flip. Direct readers
suffice -- once a reader is explicit, a definition reading *it* no longer
moves. FunDefs need nothing: their bodies are terms and cannot mention a
predicate. This is the fallback the comment above
restoreEliminatedDefinitions had been anticipating; its third bullet, the
fixed-point argument that was supposed to make the BCE case work out, is
what the run above refutes, so it is rewritten.
GLOB_FLIP goes through the same path, which also lets its two
ASS(...isEmpty()) guards go. But it keeps its old skip: Shuffling::
polarityFlip walks the whole signature, so it records flips for
predicates that no longer occur, and for a target with neither a table
nor a recorded definition materializing would be actively wrong --
symbolicPredDef would invent a trivial "p <=> $false" record, and the
real definition arriving later would find the key already taken (DHMap::
insert does not overwrite). Measured: doing that instead of skipping
turned axioms 16/19/26/27 of PRO007+4 false, leaf and next_subocc being
exactly such predicates.
Evidence, one binary, freeze switched on and off, 150 seeds of the decode
string above on PRO007+4: 34 self-check failures before, 22 after --
12 seeds fixed, none broken. ctest and checks/sanity unaffected.
Known residual, pre-existing and out of scope here: those remaining 22
fail on axioms 4 and 6, over activity/subactivity (recorded as trivial
"<=> $true" by pure predicate removal) and activity_occurrence. A
deterministic checks/ reproducer was attempted and abandoned -- pure
predicate removal and PEL between them simplify the required shape away.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
restoreEliminatedDefinitions skipped a flip whose target the model neither
represented nor had a record for. That is wrong whenever the flips are all the
model ever learns about a symbol, which blocked clause elimination produces
readily: if every clause of a predicate is blocked, its usageCnt drops to zero,
so it gets no table, and BCE records no definition for it -- only CondFlips.
Unlike a definition, a flip prescribes the value just on the arguments its
condition selects, so it needs a table to carve into.
Reproducer, deterministic (Axioms/LAT001-2.ax is
complement(X,Y) <=> (meet(X,Y) = n0 & join(X,Y) = n1) as three clauses, all
three of them blocked):
./vampire -sa fmb -pel on -bce on Problems/LAT/LAT057-1.p
User error: FMB model self-check FAILED on: 11.
meet(X0,X1) != n0 | join(X0,X1) != n1 | complement(X0,X1)
complement fell back to the trivial "<=> $false" invented by symbolicPredDef.
Added as checks/fmb/bceflip.p; it needs check_exact_output, since the defect
surfaces *after* the SZS status line -- as a SIGSEGV there, which neither
check_szs_status nor run_vampire's stderr grep can see.
So prepareForFlip now always materializes its target, and the reason the skip
was introduced is addressed at its source instead: a table used to outrank the
symbolic record permanently (evaluateLiteral consults the record only if
!predRepresented), so a definition replayed after a flip that had materialized
its symbol was silently dead. The FUN_DEF/PRED_DEF cases now discard such a
table, and record with DHMap::set rather than insert, so an arriving definition
overrides whatever the model said about its symbol so far. (The comment removed
here blamed insert's refusal to overwrite an occupied key; that was not the
mechanism -- materializePred ends with _symbolicPreds.remove, so the insert
did succeed.)
Discarding is safe because a definition body can only mention symbols that
still occurred at its own elimination step: any definition mentioning q was
recorded no later than q's own and is replayed after it, so nothing already
materialized was computed from the discarded values. Two assertions state the
corollary, that a table found in place at definition time came from a flip.
Measured on one binary over 422 sampled satisfiable TPTP problems,
-sa fmb -pel on -bce on with the self-check macro: self-check failures
31 -> 0. On PRO007+4 with the fmb+10_1 decode string of the previous commit,
150 seeds: 22 -> 0, which also settles the residual left open there -- those
seeds needed the discard, not the freeze. ctest 100/100, checks/sanity passes.
Known and left open, pre-existing on this branch (it reproduces at 4bf5d0f,
before the skip was introduced, and does not on master): materializing a
predicate of large arity is unallocatable, so SYN826-1, SYN831-1 and SYN841-1
die with std::bad_alloc on an arity-47 predicate over a two-element domain.
The skip happened to mask it. Those three showed a wrong model before this
commit and a crash after it.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…g it Since the previous commit a flip always materializes its target, which is necessary -- blocked clause elimination can blank a predicate entirely, and then its flips are all the model knows about it. But a materialized table is bounded only by the symbol's arity, where initTables' are bounded by the domain sizes FMB's own search settled on. SYN826-1, SYN831-1 and SYN841-1 ask for a table of 2^47 rows (an arity-47 predicate over a two-element domain) and abort: ./vampire -sa fmb -pel on -bce on Problems/SYN/SYN826-1.p % SZS status Satisfiable for SYN826-1 libc++abi: terminating due to uncaught exception of type std::bad_alloc Catching the bad_alloc is not the answer, and not just in principle: two handlers are already on that stack -- ProvingHelper.cpp:55 and vampire.cpp:747 -- and neither fires. The abort is inside __cxxabiv1::failed_throw, i.e. the throw never found a handler, in release and debug alike, while a USER_ERROR thrown a few lines away in the same function unwinds and is caught cleanly. Which is what one would expect of a failure path that itself needs memory: building the message, the stream, and libc++abi's demangling terminate handler all allocate. Nor is the exception reliable to begin with -- under overcommit the allocation succeeds and the process is killed while DArray::expand writes the rows, so there is nothing to catch -- and Vampire's own memory limit is advisory at best, setMemoryLimit's setrlimit being a silenced no-op on macOS. So decide before allocating: materializePred and materializeFun now check the row count against the memory limit and raise the INVALID_OPERATION that tableSize already uses for its overflow case, naming the symbol and the size. Nothing is allocated on the failure path. The check deliberately does not go into tableSize itself, which initTables also uses; that path is bounded already and has its own guard upstream. The three problems now report "Model too large to represent" and exit 4. The SZS status line precedes it, as it does for a self-check failure, because onModelFound prints the status early on purpose -- which is honest here: FMB did find a model, we merely cannot write this one down. checks/fmb/toolarge.p is a four-clause version of the same shape (arity 40, two elements), and needs check_exact_output because the message lands on stdout after the SZS status line, where neither check_szs_status nor run_vampire's stderr grep can see it. It fires in debug as well as release. ctest 100/100, checks/sanity passes, and the FMB entries were run against the debug build too, where the memory limit is 128 times tighter. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
restoreGlobalPredicateFlip mapped INTP_UNDEF to INTP_TRUE, the only place in the file that turns "we don't know" into a definite value -- and it picked the opposite of what the rest of the code would. Everywhere else an undefined cell is either propagated (the sort-elimination rebuild copies cells verbatim), raised on (evaluateLiteral throws UndefinedValueException, which onModelFound reports as a partial model), or resolved exactly once, at the end of restoreEliminatedDefinitions, where a cell nobody asked about defaults to INTP_FALSE. Deciding it early, and the other way, is inconsistent on both counts, and it hides rather than reports a hole in a model we built ourselves. This does not make us fail more eagerly: an undefined cell now fails only if something actually reads it, and is defaulted as before if nothing does. restoreViaCondFlip is deliberately left alone: writing a definite value over an undefined cell is right there, since a conditional flip prescribes the value for the arguments its condition selects whatever was there before, and flipped |= (before != after) still drives the fixpoint correctly. The branch looks unreachable today -- since the previous commits a flip's target is always materialized first, and both fill paths (addPredicateDefinition per grounding from the SAT assignment, restoreEliminatedPredDef over the full ArgsEnumerator) are total -- so this is a tightening against future holes rather than a fix. As expected, nothing moved: PRO007+4 with the fmb+10_1 decode string (rp=on, so global flips are actually replayed) still passes 150/150 seeds, checks/sanity passes including its -sa fmb --random_polarities on entry, and ctest is 100/100. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
removeUnusedDefinitions removes definitions in dependency order -- the toDo loop pops d, marks it REMOVED, and only the occurrences that drop away with d can make a further definition unused and push it -- but it *recorded* them by popping defStack afterwards, which is the order in which the clauses happened to be scanned. The two orders disagree whenever a definition is stated before the one it depends on. That matters because Problem::interferences is replayed backwards to rebuild a model of the original problem: a definition's body has to be evaluated in the model as it stood when the definition was eliminated, so its dependencies must be restored first. With the scan order, they are restored afterwards instead. Not observable today, because FiniteModelMultiSorted evaluates a recorded definition lazily and so ends up reading the final model either way. It becomes a wrong model as soon as a definition reads the model as of its own creation, which is what the layered model representation is about to do. Fix: record inside the toDo loop, right where the definition is marked REMOVED. Reproducer (checks/fmb/chaindef.p, now in checks/sanity): ./vampire --input_syntax tptp --statistics none -fde unused checks/fmb/chaindef.p prints, before this commit, define f(X0) := g(X0) define g(X0) := h(X0) i.e. f -- whose body reads g -- restored before g, and after it the other way round. Swapping the file's first two clauses hides the defect, which is why the check pins the exact output. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Preprocessing's transformations are undone one by one when a model of the preprocessed
problem is turned back into a model of the original one, and that replay is a sequence of
models -- model_0, model_1, ... -- in which model_j is defined in terms of model_{j-1}.
FiniteModelMultiSorted currently flattens that sequence: a symbol is represented *either*
by an explicit table *or* symbolically, and a step that has something new to say about a
symbol has to overwrite, discard or materialize what was there before.
Introduce the representation that can hold the sequence instead. Each symbol now carries a
stack of layers (FMB/ModelLayer.hpp); reading the model walks the stack from the top and
takes the first layer that has a value for the arguments at hand, so a layer with nothing
to say -- an explicit table with a hole -- falls through to the one below, and falling off
the bottom is the UndefinedValueException the table read used to throw by hand.
This commit only puts the structure in place: the sole layer kind is TABLE, every
represented symbol has exactly one, and everything else -- the symbolic definition maps,
materialization, prepareForFlip, printing -- keeps working through it unchanged. So does
eliminateSortFunctionsAndPredicates, which still rebuilds the base tables wholesale; it now
has to delete the layers it moved aside, since the model owns them.
No behavioural change. Verified byte-identical output on 150 sampled satisfiable TPTP
problems under -sa fmb -pel on -bce on (87 of which produce a model); the three files that
differed are unstable across two runs of the *same* binary, being cut off at different
points by the time limit, and none of them reaches a model. checks/sanity's FMB block is
unaffected (its one failure, --mode model_check on fmb/bool.check.p, predates this work and
only fires in a debug build).
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The replay in restoreEliminatedDefinitions walks preprocessing backwards, and each step
transforms model_{j-1} into model_j. Give that index a name: every layer records the step
that pushed it, and every read of the model carries an "as of" timestamp, seeing exactly
the layers born strictly earlier. The layers initTables builds are model_0; the replay
clock ticks once per interference.
Nothing reads as of anything but _now yet -- with a single layer per symbol, all of them
born at model_0, the timestamps cannot make a difference -- so this is scaffolding only.
It is what will let a definition read the model as it stood when the definition was
eliminated, instead of tracking whatever a later flip does to the symbols in its body.
No behavioural change: identical output on the same 150 sampled satisfiable TPTP problems
(87 models) as the previous commit, bar three runs cut off at a different point by the time
limit, none of which reaches a model. checks/sanity's FMB block is unchanged.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…mbol A symbol whose last occurrence disappeared with some other elimination is free to take any value at all, and until now the model discovered that lazily -- symbolicFunDef/symbolicPredDef invented a trivial definition on first demand, and whatever nobody demanded was filled in by a sweep over the tables at the very end of the replay. Make it a layer instead, pushed once, before the replay starts: installTrivialLayers gives every symbol with no explicit table a TRIVIAL layer, so model_0 already says something about every symbol on every argument tuple. A replay step is then a *correction* to a total model rather than a completion of a partial one, which is what the following commits need. Two consequences worth naming: - the end-of-replay defaulting sweep is gone. It was already a no-op -- both fill paths are total, as 5947102 noted -- and with it gone a table cell that somehow is undefined now reaches evalFun/evalPred and is reported as "FMB constructed a partial model" rather than quietly defaulted. toString reads through the evaluator for the same reason: it used to go to the cells directly, which is the only thing that made the sweep necessary. - a table now sits on *top* of a symbol's stack rather than at the bottom, so a materialization stacks over the trivial layer instead of replacing it, and discarding a table for an arriving definition uncovers the trivial layer instead of emptying the stack. A table hole therefore falls through to the trivial layer, which is the same value the old sweep would have written. installTrivialLayers runs after eliminateSortFunctionsAndPredicates, not before: sort elimination renumbers the domain elements and rebuilds every table, so nothing pushed earlier would survive it. ModelCheck does not call it at all -- a model read from a file is legitimately partial, and there an empty stack is exactly the exception to report. No behavioural change: identical output on 150 sampled satisfiable TPTP problems (87 models) under -sa fmb -pel on -bce on, bar three runs cut off at a different point by the time limit, none of which reaches a model. checks/sanity's FMB block is unchanged. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Replace _symbolicFuns/_symbolicPreds with DEF layers. A FUN_DEF or PRED_DEF now pushes a layer stamped with the replay step that replayed it, and evaluating that layer evaluates the definition's body *as of that step* -- in the model this step transforms, not in the model the replay ends up with. That is the point of the timestamps, and it is what the two rules the previous design needed were approximating: - "a definition overrides whatever the model said about its symbol" is now just shadowing. A definition is total, so a DEF layer answers for every argument tuple and nothing below it is ever consulted. The explicit discard of a table found in place is gone, and with it the ordering argument that justified the discard. - "a definition must not track a later flip" is now the as-of read. The LIFO replay makes birth order the reverse of preprocessing order, so a definition's body can only mention symbols whose layers are born earlier -- they were still live when the definition was recorded, hence eliminated later, hence replayed sooner -- while a flip recorded earlier in preprocessing is born later and is correctly invisible. Nothing has to be frozen for that. The freezing in prepareForFlip therefore has only one job left, and only until the flips themselves become layers: the flips still write into a table born at model_0, where a read as of any later time sees the change regardless of timestamps. So it stays, retargeted at DEF layers instead of the symbolic maps, and goes when the flips move. materializePred is now a snapshot rather than a fill-from-definition: it reads out what the model currently says about the predicate and pushes that as a table on top. Same values, but it no longer needs a definition to exist, so the invented trivial definitions -- and with them FunDef's may-be-null _body -- are gone; the trivial layer from the previous commit covers what they were for. materializeFun went with them; it had no caller. No behavioural change: identical output on the 87 satisfiable TPTP problems FMB models in this sample, 0 self-check failures, checks/sanity's FMB block unchanged (its one failure, --mode model_check on fmb/bool.check.p, predates this work and only fires in a debug build). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Undoing Shuffling::polarityFlip means negating the model on one predicate and changing nothing else. As a layer that is what it literally is: read the layer below, as of this layer's own birth, and return the opposite. No table to rewrite, and no table to allocate first when the model had nothing to say about the predicate -- the flip reads whatever was there, be it a trivial layer or a definition. The freezing prepareForFlip does is now needed only for conditional flips, which still write into a table born at model_0 and so are still visible to a read as of any later time. A global flip needs none of it: a definition whose body reads the flipped predicate was born earlier and cannot see this layer at all, which is exactly the "the model changes on its target alone" the flip's soundness argument asks for. toString now picks its shape from the *top layer's kind* rather than from funRepresented. The two used to coincide, because a flip's target was always materialized into a table first; with the flip a layer of its own, they do not -- a GLOBAL_FLIP layer has no table, so the representedness test sent it down the symbolic path, where it printed the value of the layer *below* the flip. On Problems/GRP/GRP027-2.p under -rp on that printed tff(equalish_symbolic_definition,axiom,![X0:$i, X1:$i]: (equalish(X0,X1) <=> $false)). for a predicate the model has reflexive. The extensional branch already reads through evalPred, so it renders a flip correctly and just had to be reached. Verified on 87 satisfiable TPTP problems that FMB models: identical output under -sa fmb -pel on -bce on, and under -rp on (where global flips are actually replayed) 87/87 models with 0 self-check failures, 0 assertion violations and 0 partial models -- the 12 runs that do not report a self-check are the time limit cutting a slow one short. checks/sanity's FMB block is unchanged. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…alized any more
A conditional flip prescribes its predicate's value on just the argument tuples its condition
selects and leaves it alone everywhere else -- which is a sparse map over a fall-through, not
a rewritten table. Making it a layer of that shape removes the last thing in the replay that
writes cells, and with it the whole materialization apparatus: prepareForFlip,
materializePred, mentionsPredicate and checkTableAffordable are all gone.
The freezing goes for good. Its job was to stop a definition tracking a flip, and the
timestamps do that already -- a definition born before the flip cannot see the flip's layer
at all. It only had to stay this long because the flip still wrote into a table born at
model_0, where a read as of any later time saw the change regardless.
Details worth recording:
- the layer is pushed before it is filled, and the fill reads as of _born + 1, i.e. the model
this step transforms *plus this layer itself*. That self-read is what the old code got from
writing into the table as it went, and it is not optional: the repair a blocked clause asks
for reads the model it is updating, and for a _fixedPoint flip -- whose clause carries both
polarities of the predicate -- iterating against a frozen model reaches no repair at all.
Nothing else is affected, since only this layer is born at _born.
- the map is keyed on the argument tuple, not on tableIndex. tableIndex multiplies out the
domain sizes with no overflow check; only tableSize has one, and tableSize is exactly what
we stop calling here. A conditional flip is also precisely where a symbol may be too wide
for a table to exist, so aliasing would be reachable rather than theoretical.
- definition layers now memoize. Materialization was doubling as memoization, and without it
Problems/NLP/NLP177-1.p went from 6s to 99s -- bodies nest, and an eliminated predicate's
body is a disjunction with existential prefixes, re-evaluated per read. A memo per layer
costs one entry per argument tuple actually asked about, rather than per tuple that exists,
and is safe because everything a definition reads is born before it and therefore fixed.
This was meant to be a separate follow-up; it is here because the commit is a large
regression without it.
- toString will not print a definition body whose symbols have acquired newer layers since,
as the body then describes an older model than the one being printed; such a symbol is
spelled out extensionally instead. Previously the freezing happened to guarantee this. The
proper fix is to print the older version under a name of its own, which is the priming work
still to come; this is no coarser than what it replaces.
- the explicit table is the bottom layer of a stack again, and funTable/predTable look there.
Moving it to the top was scaffolding for materializePred stacking a table over a trivial or
definition layer, and the justification given at the time ("a table hole falls through to
the trivial layer") was vacuous: installTrivialLayers only fills empty stacks, so a
represented symbol has nothing beneath it. With materializePred gone, initTables is the only
thing that builds a table and it does so before anything else exists.
checks/fmb/toolarge.p is no longer run by checks/sanity, and toolarge.out is deleted: with
nothing to allocate there is nothing to refuse up front, and the flip's condition ranges over
2^40 groundings, so the run is simply infeasible rather than wrong. The same holds for
SYN826-1 / SYN831-1 / SYN841-1, which before this commit died with "Model too large to
represent: a table for ssNder1_47... needs 140737488355328 rows" and now find a model and get
on with the replay.
Results on the 87 satisfiable TPTP problems FMB models, under -sa fmb -pel on -bce on:
82 models now print in full with a passing self-check, up from 75, and every model that
printed before prints identically. 0 self-check failures, 0 assertion violations, 0 partial
models. checks/sanity's FMB block passes, fmb/bceflip.p -- the blocked-clause flip that used
to force a table -- byte for byte; its one failure, --mode model_check on fmb/bool.check.p,
predates this work and only fires in a debug build.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A symbol that vanished during preprocessing without anything being recorded about it is claimed to be free to take any value. Giving every one of them the same value -- the first domain element, $false -- is the choice least likely to test that claim: a symbol that is not in fact free may well be satisfied by it anyway. So under FMB_CHECK_MODEL_AGAINST_INPUT a trivial layer answers with a splitmix64 hash of its arguments and a per-symbol salt drawn from Lib::Random, which makes the values junk but a genuine function of the arguments, and reproducible for a given -random_seed. Drawing in installTrivialLayers is safe: onModelFound runs after all search, so nothing downstream depends on the random stream. The salt is compiled out rather than switched off. With FMB_CHECK_MODEL_AGAINST_INPUT at 0 there is no salt member, no argument to the constructor and no hash call -- value() is a bare "return 1" / "return INTP_FALSE" -- so setting the macro to 0 leaves nothing of this behind. The macro itself moves to ModelLayer.hpp, the lowest header that now has to see it. Printing: junk has no formula rendering, so a trivial layer is printed extensionally while the salt is on. A symbol of arity 0 takes that path either way -- it has one value, and printing it *is* the formula -- so its rendering does not move when the macro is switched off. That is the only fixture change here: bceflip's n0 and n1 go from "n0_symbolic_definition" to "n0_definition", saying the same thing under the name a constant normally gets, and they will stay there when the self-check goes. On the 87 satisfiable TPTP problems FMB models, under -sa fmb -pel on -bce on: 87/87 models, 0 self-check failures, 0 assertion violations, 0 partial models. 22 of them now give an unconstrained symbol values that vary -- e.g. KRS034+1's xsd_string, uniformly false before and a mixed extension now -- so the claim is being tested rather than assumed. Output is identical across two runs of the same binary and differs between -random_seed 1 and 2, as intended. checks/sanity's FMB block passes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
FMB's conditional-flip layers are sparse maps from argument tuple to value with
a fall-through, and printing one as nested $ite gives a right-leaning tower that
closes with a wall of ')))))))' and has to be descended again when read back in
--mode model_check. $cond(c1,v1,...,cn,vn,e) -- arity 2n+1, n > 0, first match
wins -- is the flat form; this commit adds it to the kernel only, so nothing can
build one yet and no behaviour changes.
$match is the obvious thing to reuse and cannot be: it has neither an else nor
an ordering. Both back ends emit 'v = pi => result = bi' per case independently
(FOOLElimination.cpp, NewCNF::processMatch), so cases must be mutually exclusive
*and* exhaustive -- which is why SMTLIB2, its only producer, expands a variable
pattern into the missing constructors before building the term. Being exhaustive
over a finite domain means listing all n^k argument tuples, i.e. exactly the
dense table the layered-model work exists to avoid.
So COND is a separate functor with MATCH's *representation*: every argument an
ordinary TermList in args(), one sort in the special data, no formulas and no
binders hidden anywhere. Conditions are $o-sorted terms, normally a FORMULA
special term. That makes almost every one of the 24 SpecialFunctor switches a
shared 'case MATCH: case COND:' -- the rebuilding ones go through the new
Term::createMatchOrCond, the rest already say "args are handled below".
Clausification does not learn a new construct: Term::condToITE unfolds a $cond
into the nested $ite it abbreviates, and both FOOLElimination and NewCNF (in
findITEs and processBoolterm) recurse on that, the way NewCNF's LET case already
does.
headToString returns "$cond" without the parenthesis, deliberately unlike
"$match(". The heads that open their own parenthesis are doubly-parenthesised by
both callers -- './vampire --mode clausify --show_preprocessing on
Problems/ARI/ARI762_1.p' prints '$ite($less(X0,X1), (X1,X0)' -- and adopting
that convention would make $cond's output depend on a fix to that. This way it
prints correctly before and after.
Drive-bys on lines already being touched: operator<< printed MATCH as
"SPECIAL_FUNCTOR_LAST ", and getMatchedSort() had no assertion, which matters now
that a second variadic special term shares that union member.
UnitTests/tCond.cpp covers both printers (Term::toString and, via a literal,
TermList::asArgsToString -- they are separate implementations), the result sort,
and that condToITE puts the leftmost condition outermost.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Makes $cond reachable; everything downstream of the parser landed in the previous commit, so this is only the frontend plus its tests. The arity is not known until the closing parenthesis, and at a comma there is no way to tell another condition from the else. So funApp() reads a flat argument list with the ordinary ARGS/END_ARGS machinery, exactly as for a function application, and endCond() imposes the shape afterwards: an odd count of at least three, conditions at the even indices with sort $o, every value plus the else sharing one sort. Conditions need no sub-grammar of their own. TERM_INFIX already routes &, |, =>, ~, quantifiers and equalities through FORMULA_INSIDE_TERM, which yields exactly the $o-sorted term $cond wants -- but only once _insideEqualityArgument is out of the way, so funApp() suspends it across the argument list and endCond() restores it. That guard makes a connective *end* the term, so that "a = b & c" reads as "(a = b) & c"; inside $cond's parentheses there is no such ambiguity, since an argument ends at a comma or the closing parenthesis. Without suspending it "d = $cond(p(d) & q(d), a, b)" does not parse. One limitation, shared with every other term argument and so left alone: a condition whose *top-level* connective sits under an equality needs parentheses, "$cond((X = a & Y = b), c, d)" and not "$cond(X = a & Y = b, c, d)" -- the inner equality re-raises the guard for its own right-hand side. Exactly the same is true of "r(X = a & p(X))" today, and FMB printing controls its own output. $ite avoids it only by reading its condition with the FORMULA state. $cond is not offered in THF: holFormula() has no T_COND case, so a higher-order input gets a parse error rather than reaching HOL::toString, which asserts on any special term other than FORMULA and LAMBDA. checks/parse/cond.p is the end-to-end test, run through both clausification pathways. Its conditions deliberately overlap -- p(d) and q(d) both hold, and a != b is asserted -- so the conjecture is a theorem only if the first match wins. Verified to discriminate: with condToITE folding the pairs the other way both pathways report CounterSatisfiable instead of Theorem. It also carries the shape FMB model printing will emit, conditions that are conjunctions of argument equalities inside an equality argument. Checked over the 342 + 149 problems of problemsTX0/TX1 under --mode clausify: no new parse errors and no new assertions. (Four of them -- SYO934_1, CSR144_8, ITP277_3/4 -- violate ASS_REP(isNonSpecificInferenceRule) in Inference.cpp with rule "input", but so does the branch binary built at 52c55f4, so that one predates this work.) Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
FOOLElimination compiles both away long before FMB runs, but two places evaluate formulas that never went through preprocessing: the self-check reads the *un-preprocessed* input units, and --mode model_check reads a problem straight from a file. Neither could see a $cond, so this is what makes the construct usable for the model printing it was added for. evaluateTerm's special-term branch becomes a switch. $cond evaluates its conditions in order and only the winning branch, $ite picks a side; everything else still raises the same USER_ERROR as before. Two things the tests turned up, neither of them optional: - evaluableFormula/evaluableTerm in FiniteModelBuilder gate what the self-check looks at, and they still admitted only FORMULA. So the $cond unit was *skipped* rather than checked -- "3 units checked, 1 skipped as not evaluable" -- and the new evaluator case never ran. They have to move in step with evaluateTerm, and now say so. - A $cond in formula position arrives as a BOOL_TERM, which went through evaluateTerm and then compared against boolValue(true) -- and boolValue needs the domain element $true sits on, which only a FOOL problem's model has. So checking "? [X] : $cond(p(X),q(X),$false)" failed with "The loaded model is partial: no value for $true". That matters beyond this test: a conditional-flip layer for a predicate will print as "p(X0) <=> $cond(...)", and most models have no boolean domain. The new evaluateBooleanTerm decides such a term directly where it can -- FORMULA, $ite, $cond -- and falls back to the old expression otherwise, which is the same answer whenever the old one had one. checks/fmb/cond.p covers the self-check path and cond.check.p the model_check path; in both, the conditions deliberately overlap so the model only agrees with the input if the first match wins. Verified to discriminate: reversing the case order in the evaluator turns the first into "self-check FAILED on: 2. ! [X0] : f(X0) = $cond(p(X0),a,q(X0),b,c)". cond.p is checked by exact output, not by SZS status, because a self-check failure raises USER_ERROR only after the status line has been printed -- the same trap the bceflip comment above it records. Regression: the 87 model-producing satisfiable TPTP problems under -sa fmb -pel on -bce on are byte-identical to the run before this series, 87/87 models with no self-check failures, no violations and no partial models. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
headToString opened the parenthesis itself for these four and printed the
material that precedes args() -- $ite's condition, $let's type and binding,
$proj's index -- and then both of its callers added a '(' of their own. So one
parenthesis too many went in and one too few came out:
$ ./vampire --mode clausify --show_preprocessing on Problems/ARI/ARI762_1.p
[PP] input: 1. ! [X0:$int,X1:$int] : max(X0,X1) = $ite($less(X0,X1), (X1,X0)
Under a predicate rather than an equality it comes out balanced -- the caller's
own ')' happens to close it -- but no more parseable: "r($ite(p(a), (a,b))".
Now no head opens a parenthesis. The pre-args material moves to a new
Term::argsPrefixToString, which both callers emit right after their '(' and which
is empty for everything else -- so for any ordinary term the change adds an empty
string and nothing more. That is what keeps it away from the printing that
matters most, HOL applications included, which reach TermList::asArgsToString via
Literal::toString in every build.
UnitTests/tTermPrinting.cpp pins the result, and exists because there are *two*
printers here, reached differently and recursing differently: Term::toString goes
through headToString and Output::interleaved, while TermList::asArgsToString is a
separate stack machine that calls headToString on nested terms itself and only
re-enters Term::toString for arrow sorts. Fixing one while breaking the other is
the failure mode to guard against, so every shape is pinned under both -- and the
ordinary and $formula shapes are pinned too, to catch collateral damage. Before
this commit exactly the five broken shapes fail and the other three pass.
Separators inside the prefix become "," to match the argument separator the
generic printer uses, so a whole term now reads with one separator throughout:
"$ite(p(a),a,b)", "$let(g0: $i > $i,g0(X0) := f(X0,X0),g0(a))". Literal::toString
formats a $proj literal by hand without going through headToString at all; that
path was already correct and is untouched.
Verified: 102/102 unit tests, which include HOL_Printing and fifteen HOL
inference units; checks/sanity in full bar the arithmetic block, whose -t 1d
budgets are release performance guarantees a debug+UBSan build cannot meet
(alasca-integer-conversion needs 0.1s there and passes with -t 30); and the 87
model-producing FMB problems, byte-identical to the run before this series.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Brings in the TPTP parser work and, through it, master. Two of its commits meet $cond directly: - db226aa made every argument list record the delimiter that must close it, auditing the two ARGS-pushing sites that existed then; $cond is a third. Both that and the equality-argument guard $cond suspends by hand now live in openArgumentList(), so the $cond case is just a call to it and endCond() no longer restores anything. A textually clean merge would have left $cond pushing ARGS without a closing tag, whereupon its ')' would have popped the enclosing unit's and failed somewhere else entirely. - The termInfix and openArgumentList fixes together mean a $cond condition needs no parentheses any more: "g(X,Y) = $cond(X = a & Y = b, c, X = a, b, a)" now parses, which is the shape model printing will emit for a conditional-flip layer. And 06e98c3 stops a condition of the form "A & B = C" losing its "A &" -- "d = $cond(p & (q) = r, a, b)" read back as "d = $cond((q = r),a,b)" before. Conflicts, all from master's 9a3e820 / aef34f6 spelling container hashes out where the layered-model rewrite had restructured the same code. Resolved by keeping this branch's structure and adopting master's spelling, i.e. the substitution map becomes DHMap<unsigned,unsigned, FnvHash, IdentityHash> throughout (ArgsEnumerator too, and UnitTests/tCliqueFinder.cpp, which master could not update because it does not have it). What master's side still contained of _implicitlyEliminated*, getDomainConstant, partialEvaluate and evaluateOld is gone from this branch entirely, so those hunks are ours unchanged. One resolution is a judgement rather than a merge: ModelCheck's set of domain constants stays Set<Term*,SharedTermHash> and does not become Set<Term*,FnvHash>. Master's pass made an existing DefaultHash explicit, and for a Term* key that hashes the pointer; but this set's iteration order is what numbers the domain elements and so decides the whole output, which is exactly the reproducibility hazard CLAUDE.md describes. The domainConstantNumber map beside it does take master's spelling -- it is a pure lookup, never enumerated. The known debug-only ASS(shared()) on --mode model_check fmb/bool.check.p is unmoved by all this: same assertion, same place (Kernel/Term.hpp:749). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The merge brought in two parser fixes that between them close the gap these tests were written around: a term no longer ends at a connective that follows an equality, and the equality-argument guard no longer reaches into a nested argument list. So the shape model printing will emit for a conditional-flip layer g(X,Y) = $cond(X = a & Y = b, c, X = a, b, a) parses as written, and the parenthesized spelling that used to be the only way to say it now reads identically -- which tCond asserts, keeping both. Also adds the case for the third fix that reaches $cond: a condition of the form "A & B = C" used to lose its "A &" without a word, which the guard suspension had newly exposed inside $cond. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
--mode model_check has been dying in debug builds on its own sanity check,
checks/fmb/bool.check.p, since the domain-constant set started hashing terms by
Term::getId() rather than by address:
Condition at location Kernel/Term.hpp:749 violated: shared()
#5 Kernel::Term::getId
#8 FMB::ModelCheck::addDefinition at ModelCheck.hpp:269
The term is g($false,'fmb_$i_1'), the left-hand side of the model's first
definition. It is not a special term, so the isSpecial() check a few lines below
would never have caught it -- it is merely *unshared*, because deFool only
rewrites the top of a term and its $false argument is still a FOOL special term
at that point; the arguments are deFooled further down. getId() has nothing to
return for such a term.
Nothing was ever asking a sensible question here: every domain constant is an
ordinary shared constant, so an unshared term simply is not one. isDomainConstant()
says that, and the five places in addDefinition that consulted the set now go
through it. In release the same code read uninitialised memory for the id,
probed whatever bucket that named, found no matching Term* and answered "no" --
the right answer by luck, which is why CI never saw this.
Also removes the isVar() tests that guarded the contains() calls, now subsumed.
No new test: checks/sanity already runs
"check_exact_output fmb/bool.check.out --mode model_check fmb/bool.check.p",
which this makes pass in a debug build for the first time. With it, the whole of
checks/sanity is clean here bar the arithmetic block, whose -t 1d budgets are
release performance guarantees a debug+UBSan build cannot meet.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Four conflicts, all between master's mechanical fnType()/predType()/typeConType() -> type() collapse (3e8dce3) and the layered-model rewrite of the same FMB files: - FMB/FiniteModelMultiSorted.cpp (15 hunks) and .hpp: master's only change to these files since the branch point is that rename, so the resolution keeps the branch's code and reapplies the rename to it; the resulting diff against the pre-merge tip is exactly the 13 renamed call sites. - FMB/FiniteModelBuilder.cpp: same rename, plus a maxVarSizeBig bounding box that became dead when ArgsEnumerator replaced the manual argument enumeration; kept it deleted. - Kernel/Term.cpp: git aligned master's headToString() else-branch into the branch's new argsPrefixToString(). headToString() itself merged cleanly and already carries that block, so the hunk is dropped. 103/103 unit tests pass. checks/sanity passes apart from the arithmetic block, whose -t 1d (one decisecond) budgets a debug build cannot meet.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Some preprocessing steps are symbol eliminations which come with a model-theoretic argument on how to restore the symbol (essentially by defining it) when having a model for the formulas after elimination and wanting a model the formula before elimination. We replay these arguments in reverse order when coming from the SAT-solver constructed model and wanting to present a model for the original user input.
While we could always materialize the "truth tables" of these eliminated symbols in theory, sometimes the arities involved would cause an immediate out-of-memory or would lead to a degraded performance. So, instead, we here print whatever is reasonable to print only symbolically.
Vampire had (since Giles' time) a working model_check mode, which can read the FMB output and a list of formulas and check each against it. We extend this mode to support reading those very symbolic definitions we produce so that we can close the loop and verify our own models under the symbolic extension.
Some fixes along the way: