new news and format

Author: arminbiere

NEWS.md

@@ -1,3 +1,8 @@
+Version 1.9.4
+-------------
+
+- Simplified code by removing reimply again (but keeping ILB).
+
 Version 1.9.3
 -------------
 

src/assume.cpp

@@ -518,7 +518,8 @@ void Internal::reset_assumptions () {
 struct sort_assumptions_positive_rank {
   Internal *internal;
   const int max_level;
-  sort_assumptions_positive_rank (Internal *s) : internal (s), max_level (s->level + 1) {}
+  sort_assumptions_positive_rank (Internal *s)
+      : internal (s), max_level (s->level + 1) {}
 
   typedef int Type;
   // set assumptions first, then sorted by position on the trail
@@ -529,7 +530,7 @@ struct sort_assumptions_positive_rank {
     const Var &v = internal->var (a);
     uint64_t res = (assigned ? v.level : max_level);
     res <<= 32;
-    res |= (assigned ? v.trail : abs(a));
+    res |= (assigned ? v.trail : abs (a));
     return res;
   }
 };
@@ -550,8 +551,8 @@ void Internal::sort_and_reuse_assumptions () {
   if (assumptions.empty ())
     return;
   MSORT (opts.radixsortlim, assumptions.begin (), assumptions.end (),
-           sort_assumptions_positive_rank (this),
-           sort_assumptions_smaller (this));
+         sort_assumptions_positive_rank (this),
+         sort_assumptions_smaller (this));
 
   int max_level = 0;
   for (auto lit : assumptions) {

src/external_propagate.cpp

@@ -173,7 +173,8 @@ bool Internal::external_propagate () {
 #endif
         (void) res;
         bool trail_changed =
-            (num_assigned != assigned || level != level_before || propagated < trail.size ());
+            (num_assigned != assigned || level != level_before ||
+             propagated < trail.size ());
 
         if (unsat || conflict)
           break;
@@ -191,10 +192,9 @@ bool Internal::external_propagate () {
     }
 
 #ifndef NDEBUG
-    LOG (
-        "External propagation ends (decision level: %d, trail size: %zd, "
-        "notified %zd)",
-        level, trail.size (), notified);
+    LOG ("External propagation ends (decision level: %d, trail size: %zd, "
+         "notified %zd)",
+         level, trail.size (), notified);
 #endif
     if (!unsat && !conflict) {
       bool has_external_clause =
@@ -214,7 +214,8 @@ bool Internal::external_propagate () {
 
         add_external_clause (0);
         bool trail_changed =
-            (num_assigned != assigned || level != level_before || propagated < trail.size ());
+            (num_assigned != assigned || level != level_before ||
+             propagated < trail.size ());
 
         if (unsat || conflict)
           break;
@@ -426,7 +427,7 @@ void Internal::explain_external_propagations () {
   int open = 0; // Seen but not explained literal
 
   explain_reason (0, reason, open); // marks conflict clause lits as seen
-  int i = trail.size (); // Start at end-of-trail
+  int i = trail.size ();            // Start at end-of-trail
   while (i > 0) {
     const int lit = trail[--i];
     if (!flags (lit).seen)
@@ -690,7 +691,8 @@ bool Internal::external_check_solution () {
       size_t assigned = num_assigned;
       add_external_clause (0);
       bool trail_changed =
-          (num_assigned != assigned || level != level_before || propagated < trail.size ());
+          (num_assigned != assigned || level != level_before ||
+           propagated < trail.size ());
       added_new_clauses = true;
       //
       // There are many possible scenarios here:

src/internal.cpp

@@ -20,8 +20,8 @@ Internal::Internal ()
       tainted_literal (0), notified (0), probe_reason (0), propagated (0),
       propagated2 (0), propergated (0), best_assigned (0),
       target_assigned (0), no_conflict_until (0), unsat_constraint (false),
-      marked_failed (true), num_assigned (0),
-      proof (0), lratbuilder (0), opts (this),
+      marked_failed (true), num_assigned (0), proof (0), lratbuilder (0),
+      opts (this),
 #ifndef QUIET
       profiles (this), force_phase_messages (false),
 #endif

src/internal.hpp

@@ -243,7 +243,7 @@ struct Internal {
   vector<int> shrinkable;    // removable or poison in 'shrink'
   Reap reap;                 // radix heap for shrink
 
-  size_t num_assigned;        // check for satisfied
+  size_t num_assigned; // check for satisfied
 
   vector<int> probes;       // remaining scheduled probes
   vector<Level> control;    // 'level + 1 == control.size ()'
@@ -512,7 +512,6 @@ struct Internal {
     LOG (c, "watch %d blit %d in", lit, blit);
   }
 
-
   // Add two watches to a clause.  This is used initially during allocation
   // of a clause and during connecting back all watches after preprocessing.
   //

src/propagate.cpp

@@ -98,8 +98,6 @@ void Internal::build_chain_for_empty () {
   lrat_chain.push_back (conflict->id);
 }
 
-
-
 /*------------------------------------------------------------------------*/
 
 inline void Internal::search_assign (int lit, Clause *reason) {
@@ -566,5 +564,4 @@ void Internal::propergate () {
   }
 }
 
-
 } // namespace CaDiCaL

src/shrink.cpp

@@ -199,7 +199,8 @@ unsigned inline Internal::shrink_next (int blevel, unsigned &open,
     assert (pos < t->size ());
     const int uip = (*t)[pos];
     assert (val (uip) > 0);
-    LOG ("trying to shrink literal %d at trail[%u] and level %d", uip, pos, blevel);
+    LOG ("trying to shrink literal %d at trail[%u] and level %d", uip, pos,
+         blevel);
     return uip;
   } else {
     int uip;