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>
SLOW_DEBUG: after collect_relevant_clauses builds the kept set, assert that every dropped clause is provably inert — either satisfied by the unit-propagation assignment or in a variable component disjoint from the assumption units. A clause that is live and connected yet dropped is a keep-logic bug and would otherwise only surface downstream as a spurious SAT result. Test: a new test_interp_repair case pads the core CNF with a clause the assumption unit satisfies and a clause in a disconnected component, and checks compute_interpolant still returns an interpolant that passes the full-CNF A->I miter. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
collect_relevant_clauses seeds unit propagation with the original CNF's unit clauses. If such a unit clause forces a literal that contradicts an assumption unit, the refutation needs that clause — but the conflict was detected inside enqueue, which left conflict_cl at -1, so the kept set came out empty and the mini-CNF (assumption units alone) was satisfiable, tripping the "came back SAT" release_assert. Have enqueue record a falsified clause as the conflict anchor: the clause forcing the literal when it is an original clause, else the clause that forced the opposing value. conflict_cl stays -1 only when two assumption units contradict directly, where the units alone are UNSAT and no CNF clause is needed. Add a test_interp_repair case with a unit clause that the assumption unit falsifies. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The interp-repair min-var-repairs gate only delayed interpolation for under-repaired vars; it never contributed beyond the conflict-size and progress gates. Drop the flag, the config field, the do_interp check, and the fuzzer/sweep references. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
build_interp_branch_formula composes the must-flip branch b1 into the candidate formula and Tseitin-encodes it into the cex solver on every interpolant-driven repair. The b1-rewrite pass (full structural rewrite of b1 before encoding) and group-CSE (dedup Tseitin helpers for structurally identical sub-AIGs) both shrink that per-repair encoding, which directly slows cex-solver growth between rebuilds. Both were opt-in knobs defaulting off; flip them on. The fuzzer still randomises both values, so 0 stays covered. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
A sound Craig interpolant from the mini-CNF UNSAT proof cannot itself fail: it is always reconstructible from the proof trace, always FALSE on the CEX inputs, always satisfies A->I, and is never the constant TRUE. The only legitimate "no interpolant" outcomes are nothing-to-interpolate (empty/input-free conflict), an oversized AIG, or an exhausted conflict budget. Replace the bail-out branches and "verification failed / falling back" comments for these impossible cases with release_asserts, and drop the now-dead calls_quick_check_failed counter and the redundant interp \!= nullptr guards. Behaviour is unchanged on the real paths; a tracer/verifier bug now trips an assert instead of silently producing a wrong-but-accepted result. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Tighten the five oversized comment blocks (collect_relevant_clauses header, Pudlák selector, forced-literal conflict anchor, connectivity sweep, SLOW_DEBUG inert-clause check) to roughly half their length without losing any of the technical content. Comment-only change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
autarky.cpp/.h now use the ArjunInt::MetaSolver wrapper rather than a raw CMSat::SATSolver, so the autarky pass runs on the default CaDiCaL backend like the other MetaSolver-based passes. MetaSolver gains get_sum_conflicts(), which the autarky conflict-budget loop needs. For the CMS backend it delegates to CMS; for CaDiCaL it uses the newly added CaDiCaL::Solver::conflicts() accessor, so the 60k total conflict budget is honoured on both backends. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The definition-extraction interpolation path used three solvers per variable: CMS to prove UNSAT, PicoSAT (re-solving redundantly) just to get a clause-level UNSAT core, and CaDiCaL with a bespoke MyTracer to build the McMillan interpolant. PicoSAT is now gone. The doubled CMS-simplified CNF is loaded once into a persistent incremental CaDiCaL where every clause is guarded by a fresh selector literal; per test_var, assuming all selectors + the test_var assumptions and reading failed() back gives a true clause-level core, as small as PicoSAT's. That core feeds a fresh CaDiCaL solve with the shared InterpTracerMcMillan (MyTracer deleted). To make the tracer usable for the doubled-CNF partition (A = copy 1, B = copy 2 + indicators), InterpTracerMcMillan gains a b_local_from threshold: variables at/above it are B-local, so a resolution pivot on them is AND'd like a shared pivot. interp_repair leaves it at UINT32_MAX (no behaviour change); interpolant.cpp sets it to orig_num_vars. interp_repair's collect_relevant_clauses is extracted into a generic free function (its method now delegates to it); no behaviour change, test-interp-repair still passes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The summary, median, instance-stats, slowdown and solve-diff tables all stripped the "out-synth-" prefix down to "out-", so a directory like "out-synth-1595974-1" was displayed as "out-1595974-1". Show the real directory name instead. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
generate_interpolant proved each UNSAT instance three times per variable: once by CMS, once by the persistent selector-guarded core_solver to extract a clause-level core, and once by the tracer CaDiCaL. A perf profile of extend_synth showed the latter two solves at ~48% of runtime, all of it CDCL search -- the interpolant reconstruction itself was negligible. The core_solver pre-solve only trimmed which clauses fed the tracer, but a resolution proof already references only the clauses it uses, so clauses the refutation never touches never enter the interpolant anyway. Drop core_solver entirely and feed the whole doubled CNF (plus indicator units and the test_var assumptions, as clauses) straight to the fresh tracer-connected CaDiCaL: one solve instead of two, and the unbounded learned-clause growth of the persistent core_solver is gone. Correctness-safe: a proof over the full CNF yields a different but equally valid McMillan interpolant, verified downstream by check_extend. Verified: test-interp-repair, fuzz_synth (800), fuzz_interp_repair (800), fuzz_unate_def_rep (300), fuzz_aig_to_cnf (1000), fuzz_aig_rewrite (1000) all pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
generate_interpolant previously spun up a fresh CaDiCaL per variable and re-added the entire doubled CNF every call. A perf profile showed 33% of runtime in add_original_clause alone -- the McMillan tracer eagerly builds an AIG label for every clause it is told about, so re-adding the whole CNF each call rebuilt thousands of labels that never reach the proof. Worse, those labels used a stale input_vars, and the cost grew as input_vars grew, so extend_synth slowed down over its run. Switch to a single persistent incremental CaDiCaL + tracer for the whole extend_synth/backward loop: - fill_from_solver loads the doubled CNF into the persistent solver once and binds the tracer to the caller's live input_vars set. - add_unit_cl adds indicator units incrementally. - generate_interpolant is now one assumption-based solve: assume the test_var literals, solve, conclude(), reconstruct. The CNF is never re-added. Tracer changes: - add_original_clause no longer computes the per-clause label; labels are deferred to build_interpolant (new original_label()), built only for proof-core clauses and from the current input_vars. - add_assumption_clause / conclude_unsat handle assumption-based UNSAT; build_interpolant resolves the failing-assumption clause with the assumption units to reach the interpolant. - reset_per_solve clears per-solve scratch between solves. It is caller-driven rather than hooked to solve_query(), since cadical can derive the empty clause while clauses are still being added. - build_derived_label also tries the forward antecedent order. Verified: test-interp-repair, fuzz_synth (800), fuzz_interp_repair (800), fuzz_unate_def_rep (300), fuzz_aig_to_cnf (1000), fuzz_aig_rewrite (1000) all pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The new perf profile of extend_synth (after the persistent-incremental switch) showed build_interpolant at 11.4% with 2.76% of total in std::map _M_lower_bound walks, and memory climbing 256 MB -> 1434 MB over a 3000-solve run. Both come from the same place: the tracer's cls / antec / labels / b_clause_ids accumulate every clause from every solve forever (a derived clause kept by cadical can be the antecedent of a later proof, so naive pruning would break resolve_chain). Two changes, addressing both at once: 1. Periodic rebuild of the persistent solver + tracer. After conf.interp_rebuild_every interpolants (default 512), disconnect the tracer, recreate solver + tracer, reload the doubled CNF and the accumulated indicator units. Cheap, since add_original_clause is just a map insert now, and bounds the tracer maps to one batch's worth of derived clauses. 2. Switch cls / antec / labels to unordered_map and b_clause_ids to unordered_set. They are clause-id keyed and only point-accessed (resolve_chain etc.) — never iterated — so swapping keeps determinism and turns the O(log N) red-black-tree walks into O(1). The rebuild cadence is exposed as --interprebuildevery (default 512). fuzz_synth and fuzz_interp_repair now randomise it to 1..5 per iteration so the rebuild path is exercised by every fuzz run; the production default would otherwise never be hit on the tiny fuzz CNFs. Verified: test-interp-repair, fuzz_synth (400 with rebuild_every 1..5), fuzz_interp_repair (400 with rebuild_every 1..5) all pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
cnf-fuzz-brummayer occasionally emits a 1-var 'too many nodes' fallback CNF. The fuzzers' add_projection then projected on at least 1 var, which with nVars=1 covers every variable. file_read_helper sets all_indep=true in that case, and do_synthesis aborts with exit code 1 — which the fuzzer driver reports as a crash. Synthesis fundamentally requires at least one variable NOT in the projection (the var to be defined), so projecting the full set is a nonsense test case. In every fuzzer's add_projection: skip when nVars<2 and clamp the projection size to nVars-1 so the projection is always a proper subset. Wire the None return through gen_cnf/add_projection callers in fuzz_synth, fuzz_interp_repair, and fuzz_unate_def_rep (fuzz_repair already handled it). Also fix the misleading 'CNF had no indep set' error in do_synthesis: when all_indep is true, the CNF *has* an indep set covering everything — the actual issue is there are no defined vars left to synthesize. Reproducer (now skips cleanly): python3 scripts/fuzz_synth.py --seed 6474994302950164267 --num 1 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…pl deps sat_sweep merges functionally-equivalent AIG nodes. Two equivalent sub-trees can have different leaf-var sets — a leaf that's functionally irrelevant (cancels via internal contradiction) still appears as a t_lit in the rebuilt AIG. get_dependent_vars_recursive is purely structural, so the now-extra leaf surfaces as a real dependency, and if it (directly or via another def's cone) is a non-orig-sampl var, the next pass's defs_invariant / check_all_opt_sampl_vars_depend_only_on_orig_sampl_vars trips. Repro: fuzz_synth seed 15721965365509280309. After sat_sweep, opt_sampl_var 49's def gained leaf x10 whose own def has leaves x4, x7 — both undefined non-input — so var 49's recursive deps broke the invariant. Fix: after sat_sweep, snapshot pre-sweep defs and, per opt_sampl_var, walk current recursive deps; if any are non-orig-sampl, revert the entire pre-sweep cone for that orig. Pre-sweep state passed defs_invariant on entry, so reverting restores correctness without losing sat_sweep work on defs that didn't affect any opt_sampl_var. Iterate to a fixpoint — reverting one cone can re-expose another opt_sampl_var that shared a substituted sub-AIG. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Exposes a narrow extern-C surface (Field/FieldGen for MPZ and MPQ, SimplifiedCNF construction, set_lit_weight, sampling vars, standalone_minimize_indep, standalone_elim_to_file) so language bindings (C, Rust, etc.) can drive Arjun without depending on the C++ template machinery in arjun.h. The internal C++ struct layouts live in the installed-but-private arjun_c_priv.hpp so layered C wrappers (e.g. ganak_c) can reach the underlying objects. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
flake.lock held 3 copies of cadical (cadical, cadical_2, cadical_3) and 2 of cadiback (cadiback, cadiback_2): we declared cadical/cadiback ourselves, cadiback pulls in cadical, and cryptominisat pulls in its own cadiback (with its own cadical). These independent nodes could drift to different revisions. - cadical input now follows cadiback/cadical - cryptominisat's cadiback input now follows our cadiback (which, since cryptominisat's cadical already follows its cadiback/cadical, also collapses cadical_3) Result: a single pinned cadiback and a single pinned cadical. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The test-* executables were added unconditionally, but the top-level CMakeLists builds the library with -fvisibility=hidden whenever ENABLE_TESTING is OFF. That hides the internal ArjunInt symbols (InterpRepair etc.), so test-interp-repair — the only test that links an internal class — fails to link in that configuration. This broke `nix build`, which does not pass -DENABLE_TESTING=ON (unlike build_norm.sh / build_release.sh). Move all test-* target definitions inside the existing if(ENABLE_TESTING) block so they are simply not built when testing is disabled, matching add_test() which was already guarded. Also guard the CopyPublicHeaders dependency loop with if(TARGET ...) since test-synth may no longer exist. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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.