Merge branch 'development' of github.com:arminbiere/cadical into deve…

…lopment

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).

src/mobical.cpp

@@ -461,19 +461,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;
@@ -489,7 +483,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()) {
 
@@ -520,10 +523,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;
   }