Conversation
The orchestrator was ~890 lines with seven captured-state lambdas. Pull the per-pass mutable state into a Unate::RepPass struct and split the function into a roster of private helpers (lazy true-lits, Tseitin encoders, Y'-side def copy, indicators, f_solver build, base-assumps build, aux-set build, per-test loop body, deferred materialize, summary log). Each helper body is a near-verbatim move of the original block (s/s/p.s, lambda calls become member calls); no logic changes. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Pull the per-pass machinery out of Unate entirely. UnateDefRep lives in
its own header/cpp pair and owns the per-pass state as plain class
members instead of routing through a RepPass struct. setup_f_not_f
becomes a free helper in unate_def_common.{h,cpp} so synthesis_unate_def
and UnateDefRep can both call it without sharing a class. Unate's
synthesis_unate_def_rep is now a 2-line wrapper.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Split the ~480-line process_test_var into a small orchestrator plus four helpers: log_progress_periodic, try_commit_h (miter-UNSAT branch: feasibility check + commit), process_cex (miter-SAT branch: F-solve + pattern build + H refine), and log_per_var_summary. Per-var diagnostics move into a private PerVarStats struct. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
UnateDefRep was already in ArjunInt; Unate sat at global scope, which forced synthesis_unate_def_rep to live outside the file's ArjunInt block as a bridge. Now both live in ArjunInt and the bridge folds into the existing namespace block. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Replaces the anonymous-namespace translate_to_orig in unate_def_rep.cpp and the two ad-hoc AIG::transform<aig_ptr> remap lambdas in manthan.cpp (fill_var_to_formula_with, BVE rebuild) with a single static helper on class AIG. The manthan call sites now use AIG::new_const(true) instead of aig_mng.new_const(true); per arjun.h:587 the manager is "a convenience, not a canonical source", so this is a no-op. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Replaces four hand-rolled `AIG::transform<Lit>` visitors that all emit the same `(~h ∨ l), (~h ∨ r), (h ∨ ~l ∨ ~r)` clauses and only differ in solver, true-lit factory, and leaf-var → SAT-Lit map: - unate_def.cpp: aig_to_copy_visitor in synthesis_unate_def - unate_def_rep.cpp: aig_to_copy_visitor in setup_yprime_backward_defs - unate_def_rep.cpp: encode_h_in_miter - unate_def_rep.cpp: encode_h_in_f The new helper takes the solver, a lazy true-lit thunk (so callers can keep deferring their TRUE-helper allocation), the leaf map, and optional visit/and-emit counters to preserve `rep_stats` telemetry. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
standalone_unate_def_rep now constructs UnateDefRep directly instead of going through Unate::synthesis_unate_def_rep, which was just a one-line wrapper around UnateDefRep::run. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Pull the Y'-side backward-def loop, the indicator-clause loop, the conditional-probe scratch setup, the per-test loop body, and the final log block out of synthesis_unate_def into setup_y_prime_backward_defs, build_indicators, build_cond_state, process_test_var, and log_pass_summary respectively. The per-call transient state (s, cnf pointer, true_lit, new_to_orig, assumps, etc.) moves to private members so the helpers can share it without parameter plumbing, and try_cond_unate_def now takes only `test`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The conditional unate-def candidate list ranked candidates by clause first-seen order, which carries no signal. Rank by number of shared clauses instead — inputs that co-occur with the to-define var more often are more likely single-literal definers. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Removes the --unatedefcondrel option and the conf.unate_def_cond_relfirst toggle; the related-inputs prefix is now always tried before the rest of the input list. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
try_cond_unate_def now considers non-input vars (to-define plus already-tested non-backward-defined) as candidate L after the input list is exhausted. The conditional-probe argument is independent of L being shared between Y and Y' — non-input candidates have an indicator pinning y_L = y_L', so a single Y-side assumption suffices. Order is strictly [related_inputs, related_noninputs, all_inputs, all_noninputs]; inputs always run first. Non-input L is only committed when L is currently defined and deps_recursive(L_orig) is a subset of orig_sampl_vars (and excludes test_orig), so the resulting BW chain stays well-ordered for Manthan's recompute pass. Gated by --unatedefcondnoninp (default 1). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Port Manthan's `minimize_conflict` to the unate_def_rep CEX path. After extracting the initial input/aux pattern from the F-only conflict, iteratively try dropping each pattern lit and re-solving with the remaining lits + force_wrong assumed. UNSAT-with-~force_wrong-still- in-conflict ⇒ replace with the smaller conflict; otherwise pin and move on. Aux lits sort to the front so we drop aux first — input-only patterns make smaller H AIGs at commit and avoid the Y-side encode entirely. New knobs --unatedefrepminim (default 1) and --unatedefrepminbud (default 32). New stats: minim_attempts/succeeded/solver_calls/ lits_in/lits_out plus per-var minim trace. amba3b5y: avg_hit_aig 16.7 → 12.3, total 21.85s → 20.74s. nxquery: iters 346 → 305, total 15.94 → 16.18 (≈noise). bob: less aggressive — fewer hits but still faster overall (13.09 → 11.90). Fuzzers updated.
Manthan's "input-only conflict first" trick. Before assuming aux pins on the F-only solver, try with X assumed alone + force_wrong. UNSAT- with-~force_wrong-in-conflict ⇒ keep the input-only pattern: it lives purely over inputs, gives a smaller H (no aux leaves), and avoids the Y-side encode at commit (h_aux_leaf_count==0 reuses h_enc_lit). Falls back to the standard input+aux call on SAT or budget. Off when aux mode is 0 since the aux set is empty. Knob --unatedefrepinpfirst (default 2 = only when aux_vars non-empty; 1 = always; 0 = off). Stats: inpfirst_attempts/unsat/sat/undef. amba3b5y: 15/187 input-only UNSATs, 21.85s baseline → 19.19s (vs 20.74s after commit 1). bob/nxq roughly neutral. Fuzzers updated.
Manthan's "drop y-vars from conflict" — one SAT call dropping every aux lit from the (post-minim) pattern. UNSAT-with-~force_wrong-in- conflict ⇒ replace pattern with the input-only conflict. Saves the greedy O(n) loop when aux is jointly redundant. Cheap: skipped when pattern already input-only or empty after minim. On the three benchmarks the trigger fires 19–116 times per run but finds no joint aux redundancies (greedy already removed them); kept on as a fallback for benchmarks where greedy hits its budget. Knob --unatedefrepdropaux (default 1). Stats: dropaux_attempts/ succeeded/lits_dropped. Fuzzers updated.
After miter SAT, collect up to K-1 additional CEX models by adding fresh-activation-gated blocking clauses on (input ∪ aux) projections, then re-solving the miter under base + act + ~act_block_*. Activation lits are pinned TRUE before returning so blocking is permanently inert for subsequent iters. Per iter: score each model via a single input-only F-only probe and pick the model with the smallest input-only conflict (or first if no model gives input-only UNSAT). Refines H using the chosen model. Default K=1 (off) — the simple "smallest input-only conflict" heuristic didn't pick up gains on amba/bob/nxq (the first model already gave the smallest input-only conflict in 100% of cases on these benchmarks), and the per-iter overhead (K-1 miter solves, K F-only probes) cost 20–80% extra unate_def_rep time. Kept as a knob the fuzzer exercises (1, 2, 3, 5, 8) since it may help harder instances. Knob --unatedefrepmulticex (default 1). Stats: multicex_attempts / models_collected / extra_solves / picked_nonfirst / time_multicex_solve.
Add a manthan-style per-iter trace line that shows, for every guess+
refine iter: var, iter index, miter outcome, CEX models collected,
pattern size, minim attempt/dropped count, H AIG nodes before vs
after, and the action taken (BREAK / CONT / REFINE).
Gated by --unatedefrepiterverb (default 4) so it only fires under
--verb >=4. Fuzzer randomizes the threshold across {0, 1, 4, 99} to
exercise both fired and silent paths.
Useful for debugging refinement loops where H grows fast or stalls.
Track per-NEW-var conflict-pattern frequency (manthan's
`var_conflict_freq`) — bumped each time a var appears in an
extracted (post-minim, post-drop_aux) pattern. Stored across iters
in member `pattern_freq`, sized once at run() entry.
When --unatedefrepfreqsort=1, sort minim drop order by ascending
pattern frequency within the aux/input bucket. Less-frequent vars
are CEX-specific and more likely removable, so dropping them first
maximises the budget's expected yield.
Default 0 (off): on bob the freq sort produces aux-heavy H AIGs
that Manthan struggles to repair downstream (bob 13s → 19s with
freq_sort=1, even though unate_def_rep itself finds 5 hits vs 1).
Fuzzer randomises {0, 1} so the path is exercised.
Add invariant checks and tracing for the new code paths: - minimize_pattern: SLOW_DEBUG release_assert that all entry/exit lits live in input ∪ aux and that the post-minim pattern never grows. - drop_aux_oneshot: SLOW_DEBUG release_assert post-drop pattern is strictly input-only. - collect_cex_models: SLOW_DEBUG check that every pair of collected models differs on at least one (input ∪ aux) value (the blocking clauses must guarantee this; a duplicate would mean the activation gating broke). - VERBOSE_DEBUG entry/exit prints in minim, drop_aux, multi-cex, inpfirst paths (gated by `verbose_debug_enabled`). Also fix a pre-existing typo in the SLOW_DEBUG block of try_commit_h: stray ':' instead of ';' after release_assert(bad == 0) plus unqualified `cout`/`endl`. The block was unreachable in default builds but blocked any --define SLOW_DEBUG build of unate_def_rep.cpp. Verified by enabling SLOW_DEBUG locally and running 50 iters of fuzz_unate_def_rep — all checks pass. No runtime cost in release builds (SLOW_DEBUG_DO / VERBOSE_DEBUG_DO expand to no-ops).
Manthan's "extra minim passes for hot variables" — after the main
greedy loop converges, reverse the lit order, clear the pin set, and
sweep again. The greedy result depends on iteration order, so a
different sweep can find additional removable lits even when the
first pass hit a fixed point.
Each extra pass shares the same minim_budget; bail when budget hits 0.
Knob --unatedefrepminextra (default 0). Off by default because on amba
extra passes shrink patterns harder, but the resulting H grows more
across iters before miter UNSAT (avg_hit_aig 16.5 → 50.5, total
19.30 → 22.61) — net loss on this benchmark. Kept as a knob the
fuzzer randomises across {0, 1, 3, 10}; may help different inputs.
Stats: minim_extra_pass_calls.
When --unatedefrepmultipat=1 and multi-cex collected K>=2 models, run
process_cex on every non-chosen model after the chosen-model call.
Each yields its own (X, aux) pattern; H grows by all of them per
miter SAT instead of just one. Manthan's batched-repair analogue —
trades extra F-only minim work for faster H growth and earlier
miter UNSAT.
On amba+--multicex 3 --multipat 1: hits 4 → 9 (more!) but
avg_hit_aig 16.5 → 95 (much bigger H), total 19.30 → 27.15 (slower
overall). Off by default — the bigger H confuses Manthan downstream
on these benchmarks. Fuzzer randomises {0, 1}.
Stats: multipat_refine_calls.
Parse the [unate_def_rep] Done. and time-breakdown lines from each arjun run, accumulate per-knob stat totals across iterations, and print a coverage summary at the end. Lets the user see at a glance that the random knob choices actually exercise all the new code paths (minim, inpfirst, dropaux, multicex), and how often each fires / succeeds. Sample 300-iter run reports: total iters: 154 (rep tests: 50, hits: 8) minim: in=278 out=276 (-2, 0.7%) inpfirst: att=164 UNSAT=160 (97.6%) multicex: att=126 models=652 (avg 5.2 models/iter) If e.g. minim_sz_in == minim_sz_out for every run, the minim path is broken or never fires; this gives the user a quick sanity signal.
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.
No description provided.