Rebasing - #1
Open
m-fleury wants to merge 829 commits into
Open
Conversation
…nd resolve_clauses - Replace switch/case pattern with simpler if-chain in calc_data_for_heuristic and calc_occ_data (the switch only has 2 real cases) - Remove stale commented-out code block in calc_data_for_heuristic - Use range-based for with const auto& instead of copy-by-value - Modernize printOccur to use range-based for - Clean up resolve_clauses: remove unused cl1/cl2 variables that were only used for the freed() check Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Fix sizeof(char) -> sizeof(Lit) in mem_used() for dummy vector (was underreporting memory usage) - Modernize Stats::clear() to use value-initialization like BVEStats - Remove commented-out debug print block in order_vars_for_elim() Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Extract the duplicated sampling-neighbor check for positive and negative literal into a lambda. Removes ~40 lines of duplicated code and eliminates commented-out debug prints. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Replace the less-idiomatic insert(end, count, value) pattern with resize() and push_back(), which is clearer about intent. Also use false instead of 0 for bool vector. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Fix "Cleark" typo -> "Clear" in find_xor_gate - Replace verbose parities_found.find()==end() with .count() - Remove commented-out debug cout blocks in find_ite_gate/find_xor_gate Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Replace manual count-then-insert pattern with direct operator[] which default-constructs the vector automatically on first access. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Put the constructor before operator() (conventional order), and use more compact formatting for this simple comparator struct. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…pers The isBin()/isClause() checks in add_pos_lits_to_dummy_and_seen and add_neg_lits_to_dummy_and_seen are mutually exclusive, so use else-if to make this clear and skip the unnecessary second check. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
InitLuby/NextLuby, restart_factor, luby vector, next_restart, and oracle_lit_to_dimacs were all unused — vestiges of a prior Luby-based restart scheme replaced by Glucose-style EMA restarts. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…arning - Replace goto end with break in handle_added_long_cl (same behavior, the cleanup loop runs either way) - Remove commented-out code in backw_sub_str_long_with_bins_watch and backw_sub_str_long_with_bins - Remove commented-out cout in find_subsumed - Fix -Wshadow: rename Stats::print_short parameter to avoid shadowing the enclosing class's solver member Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add [[maybe_unused]] for variables only used in assert(), and inline trivial assert-only variables (val, cl) directly into the assert expressions where possible. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
After the l_Undef check with continue, the remaining code path only runs for l_True/l_False, so the second conditional checking for l_True || l_False was always true and can be removed. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…uches - Invert the condition and continue early to reduce nesting depth - Replace resize+assign+sort with min/max initialization - Replace duplicated n_occurs/touch calls for tmpLits[0] and [1] with a loop over tmpLits Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Replace 4 separate if-blocks with cleaner logic: use isBin() difference for bin-vs-clause ordering, then handle same-type cases. Also make operator() const and constructor explicit. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Replace 'goto end' timeout escape with a timed_out flag checked at loop boundaries. Also remove commented-out size filter and clean up the comment about size==1 resolvents. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Separate bin and clause handling with early continue, reducing nesting. Use VERBOSE_PRINT macro consistently instead of raw #ifdef VERBOSE_DEBUG. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Replace manual clear+push_back loop with assign() for tmp_tern_res. Remove commented-out backw_sub_str_with_impl call in ternary resolution. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Remove 3 commented-out sub_str_with_added_long_and_bin calls - Remove commented-out PicoSAT debug output - Fix typo: "defineed" -> "defined" Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Prefetch actual Watch struct in Assign() instead of vector header - Add clause data prefetch in SetAssumpLit() watch loop - Hoist base pointer in SatByCache() to avoid repeated index arithmetic - Remove bounds-checked at() in OracleLS::pick_var() CCD loop - Add clause prefetch in OracleLS::flip() inner loop Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…MSPS) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This reverts commit 9fe3eb5.
This reverts commit b1f14e0.
Replace inline std::atoi/atof/atoll(a.c_str()) in the option parser with fc_int/fc_double/fc_ll helpers that validate the parse and throw invalid_argument naming the offending input. atoi and friends silently return 0 on garbage like `--verb stuff`; with the wrappers the user now sees `not an integer: stuff` and a usage message.
cadical was declared both as our own input and (transitively) by cadiback, producing two separate nodes in flake.lock (cadical and cadical_2) that could drift to different revisions. Make our cadical input a follows-alias of cadiback/cadical so there is a single pinned cadical revision. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…libs The previous fix (8433727) tried to strip 'gcc_s' / 'gcc_s_asneeded' / 'atomic_asneeded' from CMAKE_<LANG>_IMPLICIT_LINK_LIBRARIES by name, but the exact name in those lists varies by distro and GCC version (Arch CXX has 'gcc_s' twice; Ubuntu CI was still emitting '-lgcc_s -lgcc_s'), turning this into whack-a-mole. Root cause: CMake probes the compiler without -static at configure time and captures the *shared* variants of libgcc/libatomic into the implicit link lib lists, then re-appends them on every later link line — under -static the linker can't find their nonexistent .a counterparts. The problem was latent before e5887a1 (which made Threads PRIVATE on cryptominisat5); having -pthread on the consumer link line had been satisfying CMake's 'runtime already covered' heuristic. Standard recipe for fully-static binaries on Linux: pair -static with -static-libgcc -static-libstdc++ so the gcc/clang driver itself links libgcc.a + libgcc_eh.a + libstdc++.a (and stops asking for libgcc_s). With the driver providing the full C/C++ runtime, CMake's implicit list isn't needed at all — clear it outright so future distro changes can't re-introduce the bug. Both flags work on gcc and on clang+libstdc++ (the default clang config on Linux). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
These declarations had no corresponding definition in cryptominisat.cpp (or anywhere else), so any external caller using them would hit a link error. Removed: get_decisions_reaching_model, get_vsids_scores, serialize_solution_reconstruction_data, create_extend_solution_setup, extend_solution, delete_extend_solution_setup. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
set_up_for_arjun in the C header was missing the cmsat_ prefix, while the implementation in cryptominisat_c.cpp exports cmsat_set_up_for_arjun, so a C client linking against the lib would see an unresolved symbol. Renamed the header decl to match. Also removed cmsat_set_polarity_auto and cmsat_set_yes_comphandler, which were declared in the header but had no implementation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two related fixes to the [simp-stats] BEFORE/AFTER log lines used by ganak's preprocessing-time analysis: 1. backbone_simpl was invisible to the chart because direct callers (arjun's puura.cpp) bypassed the print_simp_stats wrapping that the strategy-token dispatch in execute_inprocess_strategy applies. Wrap inside Solver::backbone_simpl itself so every caller is covered. 2. During occ-* steps, irred long clauses are moved from solver->longIrredCls into OccSimplifier::clauses by fill_occur(), leaving longIrredCls.size() == 0 in the log. Add Solver::get_num_long_irred_cls() that sums longIrredCls.size() and OccSimplifier::num_irred_long_cls_in_occur() (which counts live, non-red entries in OccSimplifier::clauses), and use it in the print_simp_stats macro. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two changes to make the ganak preprocessing-time chart attribute work
correctly without double-counting.
1. Track wrapper nesting depth. Many existing wrappers (e.g.
oracle-vivif-veryfast) internally invoke Solver::simplify("must-scc-vrepl,
must-renumber, ..."), which emits its own per-token simp-stats. Summing
both the outer and inner records double-counts.
Split the print_simp_stats(when, tok) macro into
print_simp_stats_before(tok) / print_simp_stats_after(tok). BEFORE emits
the current depth then increments; AFTER decrements then emits. The
counter lives on Solver::simp_stats_depth. The emitted line now ends
with " depth N" so the parser can filter to depth=0 top-level steps.
2. Wrap OccSimplifier::finish_up's reattachment phase with
print_simp_stats_before/after("occ-finishup"). This is the post-occ
phase that reattaches surviving clauses, runs propagation, and may
collapse 3-lit clauses into bins. Place AFTER past clauses.clear()
because add_back_to_solver() leaves the same offsets in both
OccSimplifier::clauses and solver->longIrredCls; get_num_long_irred_cls()
would double-count until OccSimplifier::clauses is dropped.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
zlib.net DNS resolution fails in CI; download the identical zlib-1.3.1 tarball from the madler/zlib GitHub release instead. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… Windows (#831) PicoSAT's inc_max_var() can realloc ps->lits when new variables are encountered mid-clause. Although fix_added_lits() patches buffered Lit* pointers in ps->added, the realloc is layout-sensitive: under heavy 8-thread allocation pressure the patch can miss a pointer, causing a dereference of a stale/corrupt Lit* in trivial_clause(). Fix: pre-register all variables with picosat_inc_max_var() before any picosat_add(...literal...) opens a clause, so ps->lits is fully grown before any Lit* pointers are buffered. Added: Co-authored-by: GregoryMorse <gregorymorse@users.noreply.github.com>
* Add Ctrl+C support to Python module Co-authored-by: Gregory Morse <gregory.morse@live.com> Co-authored-by: GregoryMorse <gregorymorse@users.noreply.github.com>
Thanks to @GregoryMorse for the idea and the initial work.
Co-Authored-By: Claude Opus 4.8 (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
5 participants
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.