Conversation
|
coverage: 67.079% (+0.4%) from 66.687% — mcsat-tuples-support into master |
disteph
changed the title
|
|
||
| term_t mcsat_get_unsat_model_interpolant(mcsat_solver_t* mcsat) { | ||
| return mcsat->interpolant; | ||
| return preprocessor_unblast_term(&mcsat->preprocessor, mcsat->interpolant); |
There was a problem hiding this comment.
why do you need this?
isn't mcat->interplant already unblasted?
There was a problem hiding this comment.
Good catch. The code wasn't being very clean there. Fixed in commit c7e51e8: Now mcsat->interpolant is in the blasted world. Asking for it via the getter does the unblasting,
There was a problem hiding this comment.
Let me roll that back. It is cleaner to keep mcsat->interpolant in the pre-blast world where the user-written assertions and assumptions also belong. New commits enforce that.
disteph
force-pushed
the
mcsat-tuples-support
branch
from
40404e9 to
c7e51e8
Compare
Blast tuple-typed VARIABLE terms so Yices frontend tuple declarations go through the same MCSAT tuple encoding as API-created uninterpreted terms. Keep stored MCSAT interpolants in the internal preprocessed world and unblast only through the public getter. Add API and Yices frontend regressions for tuple selectors, updates, disequality, tuple-typed variables, tuple function domains/ranges, and interpolant reconstruction.
…riant Centralize interpolant handling so mcsat->interpolant is always already in the public/postprocessed world (tuple-blasted leaves substituted back to accessors over original atoms). Writers go through mcsat_set_interpolant_from_internal for conflict-analysis values, or assign directly when the value is already public (false_term, label-substituted result). The getter mcsat_get_unsat_model_interpolant becomes a plain field read. Replace mcsat_set_unsat_result with mcsat_set_unsat_result_from_labeled_interpolant: callers now pass the temporary Boolean labels and the original assumptions; the routine performs label->assumption substitution before storing. Update context_solver.c and no_mcsat.c accordingly. Document the invariant on the interpolant field with the contract callers must respect.
Both helpers are pure functions of the type, recurse along function/tuple type structure, and were previously called repeatedly during tuple-blasting (once per visit to any term whose type involves tuples or functions). Cache the result on the preprocessor; type IDs are stable for the life of the type table so the cache never needs invalidation. Take a preprocessor_t* instead of a type_table_t*, threading caches through. All call sites updated.
… path Two related changes that together cut preprocessing cost on large or deep formulas with mostly tuple-free sub-DAGs: (M3) tuple_blast_term short-circuits sub-DAGs that contain no tuple type anywhere. The new memoized helper term_has_tuples_in_subdag walks the DAG iteratively (using tuple_blast_children to enumerate sub-terms) and caches a 0/1 answer per term index in pre->term_has_tuples_cache. When the answer is false the term blasts to itself in one step, with no descent. (M4) tuple_blast_term is now an iterative bottom-up driver instead of recursing through C stack. The recursive body is renamed tuple_blast_term_body and is invoked once per term after all its tuple_blast_children have been blasted. C stack depth is O(1) regardless of input DAG depth, eliminating a stack-overflow risk on deeply nested terms. tuple_blast_children mirrors exactly the descent in tuple_blast_term_body for every kind it handles; that contract is documented above the helper. Defensive iteration caps in both while loops trip an assertion long before any pathological input could hang a debug build.
When the blasted interpolant references the per-leaf functions of a function-valued tuple atom, preprocessor_unblast_term substitutes each leaf function with a lambda of the form (lambda v. (select j (f (tuple v_0 ... v_{k-1})))). Whatever wraps this substitution must then beta-reduce applications ((lambda v. body) args) so that no YICES_LAMBDA_TERM escapes into the public, unblasted term world that is returned by yices_get_model_interpolant.
Before this commit the three interpolant tests only checked that the original tuple/function atom name reappeared and that the interpolant was boolean. A residual lambda wrapper would satisfy both checks while still being a bug.
Add assert_interpolant_has_no_lambda_residue, a bounded recursive walk over the interpolant that aborts on any YICES_LAMBDA_TERM constructor. Plug it into the three existing function-tuple interpolant tests. Addresses review item H2.
The function had two cleanup labels, done_orig_maps and done. orig_maps
was initialized late (right before the loop that populated it), so the
earlier `goto done` branches in the leaf-processing loop had to skip
the delete_ivector(&orig_maps) in the cleanup. This works today but
silently leaks if:
- the init of orig_maps ever moves above the first `goto done`, or
- a new error branch that should delete orig_maps is added and gets
routed through `done` instead of `done_orig_maps`.
Move the init of orig_maps up with the other unconditional inits
(flat_dom, unique_offsets, unique_args), drop the done_orig_maps
label, and always delete orig_maps in the single done cleanup.
leaf_maps still uses its maps_init counter because its init is
interleaved with error branches in the first loop. The resulting
invariant -- "every goto done sees all scratch ivectors already
initialized" -- is now local and self-evident instead of having to be
reasoned about across two labels.
Behaviour is unchanged; all three build modes (debug, sanitize,
release) still pass the 31 api tests. Addresses review item M5.
The existing tests/regress/mcsat/tuples/ directory covers four
scenarios: (i) distinct tuples with equal components, (ii) tuple of
(function, int), (iii) tuple selectors inside arithmetic and bitvector
terms, (iv) tuple-update under push/pop. Several important blasting
paths that are only exercised by tests/api/mcsat_tuples.c have no
coverage in the language-level regression suite, so a regression that
only surfaces through the yices text frontend would go unnoticed.
Add four focused .ys tests that each pin down one such path:
- tuple_nested_ite.ys: tuple-of-tuple with mk-tuple inside both
branches of an ite, followed by two-level selection.
- tuple_update_rewrite.ys: (tuple-update x 2 true) must behave as
the tuple (mk-tuple (select x 1) true) once blasted and
reconstructed in the model.
- tuple_function_range_unsat.ys: function int -> Pair (scalar
domain, tuple range) sitting behind a tuple selector; an unsat
instance that forces the postprocessor to reconstruct a function
whose codomain is a tuple.
- tuple_function_domain_unsat.ys: function Pair -> int (tuple
domain, scalar range) behind a tuple selector; the dual case.
Each test is under 20 lines and produces a single-word sat/unsat gold
output, matching the style of the existing tests in the directory.
All four pass against the current mcsat build.
Addresses review item M6.
Many call sites inside tuple_blast_term_body only read the blasted leaves of a sub-term. They currently pay a malloc + memcpy per sub-term by construction: init_ivector(&v, 0); tuple_blast_get(pre, x, &v); use v.data, v.size; delete_ivector(&v); Add tuple_blast_peek, which returns (data_ptr, size) pointing directly into tuple_blast_data. The pointer is live only until the next operation that can grow tuple_blast_data -- most notably a subsequent tuple_blast_term call; this invariant is spelled out in the helper's doc-comment and repeated at every use site. Convert the three hot read-only sites called out in the review: * tuple_blast_collect_arg (called from APP / UPDATE / composites) * ITE (three leaf vectors per ITE sub-term) * DISTINCT (two leaf vectors per (i,j) pair, O(n^2)) * EQ (two leaf vectors per equality) Also tighten tuple_blast_eq_vector's signature to take (a, b, n) directly so it can consume peek output without re-wrapping in an ivector. Call sites that call tuple_blast_term AGAIN after getting the leaves (APP/UPDATE scan loops, composite/pprod/poly child loops) still use the copying tuple_blast_get; peek would be unsafe there and rewriting those to defer the tuple_blast_term calls would balloon the diff. All three build modes (debug, sanitize, release) still pass the 31 api tests, and all eight tuple .ys regressions (the four pre-existing plus the four added in M6) still match their gold output. Addresses review item L3.
preprocessor_build_tuple_model has three paths along which a
tuple-blasted atom can quietly fail to appear in the reconstructed
model:
1. one of the blasted leaf variables has no value in the trail,
2. the function-type merge in merge_blasted_function_value returns
null_value for one of several structural reasons (leaf value is
neither a function nor an update object, a map's arity does not
match the flattened domain, or a sub-call to build_value_from_flat
could not rebuild a codomain / domain / default value),
3. the non-function tuple merge in build_value_from_flat itself
returns null_value.
Under the previous code each of these branches just `continue`'d or
returned null_value and the caller conditionally invoked
model_map_term only on success. A user inspecting (show-model) would
see the atom missing with no signal anywhere as to why.
Emit a short line under the existing "mcsat::preprocess" trace tag at
each drop site:
- the leaf-missing case in preprocessor_build_tuple_model names the
atom and the leaf index that is unassigned;
- merge_blasted_function_value records a short reason string at each
of its five `goto done` exits (via a local fail_reason variable
set immediately before the jump), and emits it from the single
cleanup label; the caller then adds the concrete atom term;
- the tuple (non-function) branch in preprocessor_build_tuple_model
names the atom and notes that the leaves did not decompose.
trace_enabled is a no-op in NDEBUG, so release builds pay nothing at
runtime. mcsat_trace_printf and trace_term_ln are already used from
this file under the same tag, so no new headers or dependencies.
No semantic change to the rebuilt model; the 31 api tests and the 8
tuple .ys regressions still pass in debug, sanitize, and release.
Adds tests/regress/mcsat/tuples/tuple_show_model.ys, the first .ys gold test that exercises the (show-model) printer on tuple-typed free variables under MCSAT. The constraints fully determine both components of two free Pair tuples via select-only assertions, so the printed model is deterministic across debug, release, and sanitize builds (verified). This covers the post-unblast model reconstruction path for plain (int x bool) tuples and pins the on-disk syntax of (mk-tuple ...) values that callers of (show-model) see. Addresses review item \xC2\xA74.3.
Convert the remaining tuple_blast_get call sites whose only use of the returned snapshot is a (size==1, data[0]) read to tuple_blast_peek: NOT, SELECT, OR/XOR, POWER_PRODUCT, ARITH_POLY, ARITH_FF_POLY, BV64_POLY, BV_POLY, and the generic-composite combine. Each site already followed a uniform pattern -- tuple_blast_term, then get into a one-shot ivector, then check size==1 and read data[0] -- so nine independent malloc+memcpy+free triples per blasted DAG node go away. The peek pointer is consumed within the same loop iteration before any subsequent tuple_blast_term, preserving the lifetime invariant documented on tuple_blast_peek. The remaining tuple_blast_get callers (APP, UPDATE, top-level substitution in tuple_blast_apply, model reconstruction in preprocessor_build_tuple_model and the substitution-walk loop) all need a snapshot that survives further tuple_blast_term calls and stay on the copying path. The peek doc-comment is updated to spell out the split. Verification: all 31 api tests pass in debug, release, and sanitize (the unrelated type_macros UAF preexisting on master is unchanged); all 691 mcsat regression tests pass in all three modes.
disteph
force-pushed
the
mcsat-tuples-support
branch
from
51a8ba2 to
7a3358d
Compare
|
Review by Windsurf/Opus4.7: Review:
|
The preprocessor maintains three opportunistic memoization caches keyed on raw term/type IDs: - type_is_tuple_free_cache (key: type_t) - type_leaf_count_cache (key: type_t) - term_has_tuples_cache (key: index_of(t)) Previously their lifetime was "lifetime of the term/type table" on the assumption that IDs are stable forever. That assumption is wrong: Yices recycles type IDs in indexed_table_free (src/terms/types.c) and term indices in src/terms/terms.c after a GC sweep. preprocessor_gc_mark explicitly marks tuple_blast_map / preprocess_map / equalities / purification entries, but a term visited only as an *interior* node during classification (e.g. a select traversed by term_has_tuples_in_subdag while walking a top-level atom) is not in those root sets. Once such a term's index is freed and reused, the cached classification entry inherited by the new term could send the iterative tuple-blast dispatch down the wrong arm: either treating a tuple-containing term as tuple-free and forwarding an un-blasted SELECT to the old preprocessor, or returning a stale leaf count that doesn't match the new tuple's shape. Fix: reset all three caches at the top of preprocessor_gc_mark, before the marking loop and well before the sweep that follows. The caches repopulate on first use after GC; cost is negligible relative to GC itself. Test: tests/api/mcsat_tuples.c gains test_tuple_preprocessing_then_gc, which solves a Pair=(int,bool) problem (populating the caches), runs yices_garbage_collect with no roots so the relevant types/terms are swept and their IDs eligible for reuse, then solves a differently-shaped Triple=(bool,int,int) problem and validates the model. Also updates the doc-comments on the three cache fields in src/mcsat/preprocessor.h to describe the new GC-reset contract.
The iterative tuple-blast driver dispatches on term_kind. The dispatch
in tuple_blast_term_body and the parallel descent in
tuple_blast_children were missing several kinds that can carry a
SELECT-of-tuple subterm:
- BIT_TERM (a bv-typed operand under bit-extract)
- ARITH_IS_INT_ATOM (unary, real -> bool)
- ARITH_FLOOR (unary, real -> int)
- ARITH_CEIL (unary, real -> int)
- ARITH_ABS (unary, arith -> arith)
- ARITH_FF_EQ_ATOM (unary, ff -> bool, "t == 0")
- ARITH_FF_BINEQ_ATOM (binary, ff x ff -> bool, "t1 == t2")
Worse, BIT_TERM was bucketed with the *constant* leaf cluster:
case CONSTANT_TERM:
case ARITH_CONSTANT:
...
case BIT_TERM:
ivector_push(&result, t);
so its bv operand was never recursed into. The companion comment in
tuple_blast_children's default branch even called BIT_TERM "atomic",
which is wrong -- it carries one bv argument.
The runtime effect was that `(<op> (select x i))` would be classified
tuple-free by term_has_tuples_in_subdag (which uses the same descent),
the iterative driver would short-circuit through the tuple-free fast
path, and the original term -- still containing an un-blasted SELECT --
would be forwarded to the rest of preprocessing, where the BV/NRA/NIA
plugins reject SELECT_TERM via MCSAT_EXCEPTION_UNSUPPORTED_THEORY. So
the failure was clean (no crash) but it artificially narrowed the set
of tuple-component formulas mcsat could solve.
Fix:
1. tuple_blast_children gets per-kind cases that push the right
children, using bit_term_arg, arith_*_arg, and
arith_ff_bineq_atom_desc. The default-branch comment is corrected
so it no longer calls BIT_TERM atomic.
2. tuple_blast_term_body gets bespoke dispatch arms for each kind:
blast the operand(s), peek the result, require size==1 (any
tuple-typed operand here is meaningless and reports
UNSUPPORTED_THEORY exactly like the existing composite cluster),
and rebuild via the appropriate term_manager builder
(mk_bitextract / mk_arith_is_int / mk_arith_floor / mk_arith_ceil
/ mk_arith_abs / mk_arith_ff_term_eq0 / mk_arith_ff_eq).
BIT_TERM is removed from the constant-leaf cluster -- it was the
only non-leaf in there.
Tests:
- tests/api/mcsat_tuples.c: new
test_tuple_blast_bit_over_tuple_component, exercising
`(bit i (select x j))` over a (tuple int (bitvector 4)).
- tests/regress/mcsat/tuples/tuple_bit_select.ys: same coverage at
the .ys frontend level.
- tests/regress/mcsat/tuples/tuple_unary_arith.ys: covers
is-int / floor / abs over a (tuple int real).
The ARITH_FF_EQ_ATOM / ARITH_FF_BINEQ_ATOM cases share the dispatch
shape with the unary-arith cases above; they cannot be exercised at
.ys level (no FF arithmetic in the native frontend) and SMT2 has no
tuple types, so they have no targeted regression. The dispatch entries
themselves are reviewed against the existing FF kinds in get_composite
and term_manager.c.
Pin the property that interpolants over function-valued tuple components remain lambda-free, so future changes that rewrite interpolants in terms of blasted leaves -- and therefore start producing naked (lambda (v0) (...)) residues that fail to eta-reduce -- get caught here rather than at user-facing call sites. The "naked" path is currently doubly guarded: - Single-leaf function ranges: mk_lambda's eta-reduction fast path in term_manager.c collapses (lambda (v0) (f v0)) to f at construction time. - Multi-leaf function ranges (range is itself a tuple): the per-slice lambda body (select ((select x 1) v0) i) is not eta-reducible, but MCSAT interpolation in this configuration returns the original asserted formula rather than a leaf-level rewrite, so unblast never substitutes the leaf inside the interpolant. The new test asserts (= fx fy) against (distinct fx fy) over a multi-leaf function range and uses assert_interpolant_has_no_lambda_residue on the result. No source change is needed -- this is a guard rail.
Two related fixes to preprocessor model reconstruction so that
yices_get_model(ctx, 0) -- i.e. keep_subst=false -- no longer drops
tuple atoms whose blasted leaves are unconstrained.
1. preprocessor_build_model:
The existing code unconditionally called
model_add_substitution(model, eq_var, ...) for every solved
equality. That asserts has_alias in debug builds and silently
leaves eq_var unmapped in release builds when the caller passed
keep_subst=0. Split into two arms:
- has_alias=true: keep the existing alias-based lazy binding.
- has_alias=false: concretely evaluate eq_subst with a lazily
initialized evaluator and model_map_term(eq_var, v). Fall
back to vtbl_make_object only if eval_in_model fails (e.g.
eq_subst transitively depends on another not-yet-mapped
eq_var).
This matches the spirit of context_build_model_for_real's
handling of eliminated variables without introducing new aliases.
2. preprocessor_build_tuple_model:
When a blasted tuple leaf has no value in the trail model --
typical for unconstrained tuple components once the keep_subst=0
path disables the alias-based default-completion in
eval_uninterpreted -- fall back to vtbl_make_object on the leaf's
declared type rather than dropping the parent tuple atom. Only
truly uninhabitable types (should not occur in well-formed input)
still take the drop path, now with a more accurate trace message.
Regression test test_partial_tuple_model_no_keep_subst: asserts
(= (select x 1) 5) over x : (tuple int int), calls
yices_get_model(ctx, 0), and checks that component 1 evaluates to 5
and the whole tuple reconstructs. Pre-fix debug builds hit the
has_alias assertion; release builds silently lost the x mapping and
reported (select x 1) = 0.
The previous header claimed the .ys file covered ARITH_CEIL alongside ARITH_FLOOR / ARITH_IS_INT_ATOM / ARITH_ABS, but no ceil assertion was present. The original assumption was that mcsat's nra plugin could not solve any (= (ceil x) k) constraint and so ceil could only be reviewed for dispatch by inspection. That assumption is wrong: mcsat *does* route and answer ceil queries. Separately, mcsat's nra plugin has a real semantic bug where (ceil x) is treated like (floor x) for a range of rationals (e.g. it answers sat for `(ceil 7/2) = 3` and unsat for `(ceil 7/2) = 4`). That bug is unrelated to the tuple-blast dispatch fix in 9fefa45 and out of scope for this PR. So we add a deliberately *lax* ceil constraint over a tuple component -- (<= (ceil (select x 2)) 100) -- which holds under both the correct and the buggy interpretation. This exercises the ARITH_CEIL dispatch arm end-to-end without depending on ceil's exact value, restoring the header's accuracy. Update the matching note in mcsat_tuples.c to point at the .ys file's header for the ceil-semantics caveat.
disteph
force-pushed
the
mcsat-tuples-support
branch
from
857eb72 to
995ec36
Compare
|
Code review by OpenCode/GPT5.5 about commit 995ec36: Findings No current findings. The prior issues are addressed: H1 dispatch gap: fixed for missing term kinds. mcsat_tuples passes in debug. |
|
Summary of changes since Code review of 7a3358d: Branch summary:
|
disteph
force-pushed
the
mcsat-tuples-support
branch
from
f3417f5 to
b450750
Compare
Review of
|
The comment claimed the substitution runs 'before popping the temporary context frame', but the caller in context_solver.c pops first, then calls this helper. Rewrite the comment to match the actual ordering and spell out why the temporary labels are still valid post-pop (mcsat_pop does not invoke term_table_gc). No behaviour change.
|
Code review for entire PR by Codex/GPT5.5: Findings Summary The test coverage is substantial for the changed behavior: API tests cover tuple/function models, tuple selectors under arithmetic/BV contexts, push/pop scoping, GC, Tests Run
Result: 31 passed, 0 failed. |
3 participants
This branch adds end-to-end tuple support in MCSAT by eliminating tuples before solving and reconstructing results in terms of the original problem.
It includes:
Main changes
Preprocessor: tuple blasting
Model reconstruction
Interpolants
Backtracking/GC behavior
Tests
tests/api/mcsat_tuples.cwith MCSAT-only guards (#ifdef HAVE_MCSAT+ runtimeyices_has_mcsat()).