From 3200a3fffbcf350c485aa0062f5f33213ec20254 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sat, 16 Dec 2023 04:25:49 +0100 Subject: [PATCH 1/2] proper code quotes in NEWS.md --- NEWS.md | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/NEWS.md b/NEWS.md index be897d7f..11f58efb 100644 --- a/NEWS.md +++ b/NEWS.md @@ -1,7 +1,7 @@ Version 1.9.1 ------------- -- Fixed position of 'idrup' option. +- Fixed position of `idrup` option. Version 1.9.0 ------------- @@ -107,59 +107,59 @@ Version 1.6.0 Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider and Armin Biere. IPASIR-UP: User Propagators for CDCL. -- During decisions the phase set by 'void phase (int lit)' has now - higher precedence than the initial phase set by options 'phase' and - 'forcephase'. +- During decisions the phase set by `void phase (int lit)` has now + higher precedence than the initial phase set by options `phase` and + `forcephase`. Version 1.5.6 ------------- - Clang formatted all source code (and fixed one failing regression - test by disabling 'otfs' for it). + test by disabling `otfs` for it). -- Implementing OTFS during conflict analysis (--otfs). +- Implementing OTFS during conflict analysis (`--otfs`). -- The last literal set by vivification is instantiated (--vivifyinst). +- The last literal set by vivification is instantiated (`--vivifyinst`). -- more accurate tracking of binary clauses in watch lists by updating - the size in watch lists. +- More accurate tracking of binary clauses in watch lists by updating + the size in watch lists. Version 1.5.4 ------------- -- Picking highest score literal in assumed clause ('constrain') +- Picking highest score literal in assumed clause (`constrain`) and caching of satisfied literal by moving them to the front. -- Added 'bool flippable (int lit)' to API. +- Added `bool flippable (int lit)` to API. -- Fixed 'val' to return 'lit' or '-lit' and not just '-1' and '1'. +- Fixed `val` to return `lit` or `-lit` and not just `-1` and `1`. -- Allowing 'fixed' between 'constrain' in 'mobical'. +- Allowing `fixed` between `constrain` in `mobical`. - Fixed LZMA magic header. -- Added 'bool flip (int lit)' to API. +- Added `bool flip (int lit)` to API. - Fixed different garbage collection times with and without - clause IDs (with './configure -l' or just './configure'). + clause IDs (with `./configure -l` or just `./configure`). This solves issue #44 by John Reeves. At the same time made sure to trigger garbage collection independent on the number of clause header bytes by relying on the number of garbage literals instead. -- Fixed 'mmap' usage for FreeBSD (#48 issue of 'yurivict'). +- Fixed `mmap` usage for FreeBSD (#48 issue of `yurivict`). - Removed several compiler warnings when using newer compilers, including gcc-11, gcc-12, clang-14, and clang-15. -- Replaced 'sprintf' by 'snprintf' to avoid warning on MacOS +- Replaced `sprintf` by `snprintf` to avoid warning on MacOS (thanks to Marijn for bringing this up). -- Assigning a C 'FILE' pointer to 'stdout' during initialization +- Assigning a C `FILE` pointer to `stdout` during initialization fails on MacOS and thus separated declaration and initialization. - Fixed random seed initialization from MAC address issue #47 - as used by 'mobical' which produces segmentation faults + as used by `mobical` which produces segmentation faults (thanks to Sam Bayless for pointing this out). Version 1.5.2 @@ -172,7 +172,7 @@ Version 1.5.2 - More copyright updates in banner. -- Fixed MinGW cross-compilation (see 'BUILD.md'). +- Fixed MinGW cross-compilation (see `BUILD.md`). Version 1.5.1 ------------- @@ -182,7 +182,7 @@ Version 1.5.1 Version 1.5.0 ------------- -- Added 'constrain' API call described in our FMCAD'21 paper. +- Added `constrain` API call described in our FMCAD'21 paper. -- Replaced "`while () push_back ()`" with "`if () resize ()`" idiom +- Replaced `while () push_back ()` with `if () resize ()` idiom (thanks go to Alexander Smal for pointing this out). From 1eb2e414e9dd4f7e00a66a345a2905211bee3b3e Mon Sep 17 00:00:00 2001 From: Katalin Fazekas Date: Sat, 16 Dec 2023 09:27:32 +0100 Subject: [PATCH 2/2] mock propagtor fix external clause priorities --- src/mobical.cpp | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/src/mobical.cpp b/src/mobical.cpp index 19cb2304..380a7bb8 100644 --- a/src/mobical.cpp +++ b/src/mobical.cpp @@ -458,19 +458,13 @@ class MockPropagator : public ExternalPropagator { clause_redundancy = 0; - if (added_lemma_count > lemma_per_cb) { - added_lemma_count = 0; - MLOGC( "false (lemma per CB treshold reached)." << std::endl ); - return false; - } - - add_new_observed_var (); - if (external_lemmas.empty()) { MLOGC( "false (there are no external lemmas)." << std::endl ); return false; } + add_new_observed_var (); + if (must_add_clause) { must_add_clause = false; add_lemma_idx = must_add_idx; @@ -486,7 +480,16 @@ class MockPropagator : public ExternalPropagator { return true; } - assert (add_lemma_idx <= external_lemmas.size()); + if (added_lemma_count > lemma_per_cb) { + added_lemma_count = 0; + MLOGC( "false (lemma per CB treshold reached)." << std::endl ); + return false; + } + + // Final model check will force to jump over some lemmas without + // adding them. But if any of them is unsatisfied, it will force also + // to set back the add_lemma_idx to them. So we do not need to start + // the search here from 0. while (add_lemma_idx < external_lemmas.size()) { @@ -517,10 +520,12 @@ class MockPropagator : public ExternalPropagator { int cb_add_external_clause_lit () { int lit = external_lemmas[add_lemma_idx]->next_lit (); + + MLOG ("cb_add_external_clause_lit " << lit + << " (lemma " << add_lemma_idx << "/" + << external_lemmas.size() << ")" << std::endl); if (!lit) external_lemmas[add_lemma_idx++]->add_count++; - - MLOG ("cb_add_external_clause_lit" << lit << std::endl); return lit; }