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

…lopment

NEWS.md

@@ -1,3 +1,20 @@
+Version 1.9.2
+-------------
+
+- Important fixes for ILB, trail-reuse and external propagation with
+  assumptions.
+
+- Restored effectiveness of Mobical and improved external mock
+  propagator.
+
+- Forced garbage collection of binary clauses before restore.
+
+- Merge internal status and state encodings and made them consistent.
+
+- Disabled non-verbose message if empty clause found in input.
+
+- Improved support for IDRUP.
+
 Version 1.9.1
 -------------
 

VERSION

@@ -1 +1 @@
-1.9.1-dev.3
+1.9.2-dev.1

src/analyze.cpp

@@ -392,7 +392,8 @@ void Internal::clear_analyzed_literals () {
   }
   analyzed.clear ();
 #ifndef NDEBUG
-  if (unit_analyzed.size ()) return;
+  if (unit_analyzed.size ())
+    return;
   for (auto idx : vars) {
     Flags &f = flags (idx);
     assert (!f.seen);
@@ -512,7 +513,8 @@ inline int Internal::otfs_find_backtrack_level (int &forced) {
 inline int Internal::find_conflict_level (int &forced) {
 
   assert (conflict);
-  assert (opts.chrono || opts.otfs || external_prop || (opts.reimply && multitrail_dirty != level));
+  assert (opts.chrono || opts.otfs || external_prop ||
+          (opts.reimply && multitrail_dirty != level));
 
   int res = 0, count = 0;
 
@@ -928,12 +930,14 @@ void Internal::analyze () {
     }
   }
 
-  if ((!opts.reimply && opts.chrono) || external_prop || (opts.reimply && multitrail_dirty != level)) {
+  if ((!opts.reimply && opts.chrono) || external_prop ||
+      (opts.reimply && multitrail_dirty != level)) {
 
     int forced;
 
     const int conflict_level = find_conflict_level (forced);
-    assert (conflict_level == multitrail_dirty || !opts.reimply || external_prop);
+    assert (conflict_level == multitrail_dirty || !opts.reimply ||
+            external_prop);
 
     // In principle we can perform conflict analysis as in non-chronological
     // backtracking except if there is only one literal with the maximum

src/assume.cpp

@@ -7,7 +7,8 @@ namespace CaDiCaL {
 // adds an assumption literal onto the assumption stack.
 
 void Internal::assume (int lit) {
-  if (level && !opts.ilbassumptions) backtrack ();
+  if (level && !opts.ilbassumptions)
+    backtrack ();
   else if (val (lit) < 0)
     backtrack (max (0, var (lit).level - 1));
   Flags &f = flags (lit);
@@ -541,8 +542,9 @@ void Internal::sort_and_reuse_assumptions () {
                if (!val (litA) && !val (litB))
                  return litA < litB;
                assert (val (litA) && val (litB));
-	       LOG ("%d -> %zd", litA, ((uint64_t) var (litA).level << 32) +
-               (uint64_t) var (litA).trail);
+               LOG ("%d -> %" PRIu64, litA,
+                    ((uint64_t) var (litA).level << 32) +
+                        (uint64_t) var (litA).trail);
                return ((uint64_t) var (litA).level << 32) +
                           (uint64_t) var (litA).trail <
                       ((uint64_t) var (litB).level << 32) +
@@ -560,18 +562,20 @@ void Internal::sort_and_reuse_assumptions () {
   assert ((size_t) level == control.size () - 1);
   LOG (assumptions, "sorted assumptions");
   int target = 0;
-  for (int i = 1, j = 0; i < size; ) {
+  for (int i = 1, j = 0; i < size;) {
     const Level &l = control[i];
     const int lit = l.decision;
     const int alit = assumptions[j];
     const int lev = i;
-    target = lev-1;
-    if (val (alit) && var (alit).level < lev) { // we can ignore propagated assumptions
+    target = lev - 1;
+    if (val (alit) &&
+        var (alit).level < lev) { // we can ignore propagated assumptions
       ++j;
       continue;
     }
     ++i, ++j;
-    if (!lit || var (lit).level != lev) { // removed literals or pseudo decision level
+    if (!lit || var (lit).level !=
+                    lev) { // removed literals or pseudo decision level
       if (val (alit) > 0 && var (alit).level < lev)
         continue;
       break;

src/backtrack.cpp

@@ -134,9 +134,7 @@ void Internal::backtrack (int new_level) {
 #endif
       trail[j] = lit;
       v.trail = j++;
-#ifdef LOGGING
       reassigned++;
-#endif
     }
   }
   trail.resize (j);

src/ccadical.cpp

@@ -174,16 +174,15 @@ int ccadical_frozen (CCaDiCaL *ptr, int lit) {
   return ((Wrapper *) ptr)->solver->frozen (lit);
 }
 
-int ccadical_trace_proof (CCaDiCaL * ptr, FILE * file, const char * path) {
+int ccadical_trace_proof (CCaDiCaL *ptr, FILE *file, const char *path) {
   return ((Wrapper *) ptr)->solver->trace_proof (file, path);
 }
 
-void ccadical_close_proof (CCaDiCaL * ptr) {
+void ccadical_close_proof (CCaDiCaL *ptr) {
   ((Wrapper *) ptr)->solver->close_proof_trace ();
 }
 
-void ccadical_conclude (CCaDiCaL * ptr) {
+void ccadical_conclude (CCaDiCaL *ptr) {
   ((Wrapper *) ptr)->solver->conclude ();
 }
-
 }

src/ccadical.h

@@ -7,8 +7,8 @@ extern "C" {
 #endif
 /*------------------------------------------------------------------------*/
 
-#include <stdio.h>
 #include <stdint.h>
+#include <stdio.h>
 
 // C wrapper for CaDiCaL's C++ API following IPASIR.
 

src/checker.hpp

@@ -158,7 +158,7 @@ class Checker : public StatTracer {
   void delete_clause (uint64_t, bool, const vector<int> &) override;
 
   void finalize_clause (uint64_t, const vector<int> &) override {} // skip
-  void report_status (int, uint64_t) override {}            // skip
+  void report_status (int, uint64_t) override {}                   // skip
   void begin_proof (uint64_t) override {}                          // skip
   void add_assumption_clause (uint64_t, const vector<int> &,
                               const vector<uint64_t> &) override;

src/collect.cpp

@@ -543,7 +543,8 @@ void Internal::check_clause_stats () {
 
 /*------------------------------------------------------------------------*/
 
-// only delete binary clauses from watch list that are already mark as deleted.
+// only delete binary clauses from watch list that are already mark as
+// deleted.
 void Internal::remove_garbage_binaries () {
   if (unsat)
     return;
@@ -555,22 +556,23 @@ void Internal::remove_garbage_binaries () {
   Watches saved;
   for (auto v : vars) {
     for (auto lit : {-v, v}) {
-      assert (saved.empty());
+      assert (saved.empty ());
       Watches &ws = watches (lit);
       const const_watch_iterator end = ws.end ();
       watch_iterator j = ws.begin ();
       const_watch_iterator i;
       for (i = j; i != end; i++) {
         Watch w = *i;
         Clause *c = w.clause;
-	if (c->reason && c->collect ()) {
-	  assert (c->size == 2);
-	  backtrack_level = min (backtrack_level, var(c->literals[0]).level);
-	  LOG ("need to backtrack to before level %d", backtrack_level);
-	}
+        if (c->reason && c->collect ()) {
+          assert (c->size == 2);
+          backtrack_level =
+              min (backtrack_level, var (c->literals[0]).level);
+          LOG ("need to backtrack to before level %d", backtrack_level);
+        }
         if (c->collect ())
           continue;
-	assert (!c->moved);
+        assert (!c->moved);
         w.size = c->size;
         const int new_blit_pos = (c->literals[0] == lit);
         LOG (c, "clause in flush_watch starting from %d", lit);
@@ -595,7 +597,6 @@ void Internal::remove_garbage_binaries () {
   STOP (collect);
 }
 
-
 /*------------------------------------------------------------------------*/
 
 bool Internal::arenaing () { return opts.arena && (stats.collections > 1); }

src/extend.cpp

@@ -210,7 +210,8 @@ bool External::traverse_witnesses_backward (WitnessIterator &it) {
       clause.push_back (lit);
     assert (!lit);
     --i;
-    const uint64_t id = ((uint64_t) *(i-1) << 32) + static_cast<uint64_t>(*i);
+    const uint64_t id =
+        ((uint64_t) * (i - 1) << 32) + static_cast<uint64_t> (*i);
     assert (id);
     i -= 2;
     assert (!*i);
@@ -243,7 +244,8 @@ bool External::traverse_witnesses_forward (WitnessIterator &it) {
       assert (!lit);
       assert (i != end);
       assert (!*i);
-      const uint64_t id = ((uint64_t) *i << 32) + static_cast<uint64_t>(*(i + 1));
+      const uint64_t id =
+          ((uint64_t) *i << 32) + static_cast<uint64_t> (*(i + 1));
       assert (id > 0);
       i += 3;
       assert (*i);

src/external.cpp

@@ -392,7 +392,13 @@ void External::reset_observed_vars () {
   // Shouldn't be called if there is no connected propagator
   assert (propagator);
   reset_extended ();
-  assert ((size_t) max_var + 1 == is_observed.size ());
+
+  internal->notified = 0;
+  LOG ("reset notified counter to 0");
+
+  if (!is_observed.size ()) return;
+
+  assert (!max_var || (size_t) max_var + 1 == is_observed.size ());
 
   for (auto elit : vars) {
     int eidx = abs (elit);
@@ -405,8 +411,8 @@ void External::reset_observed_vars () {
       melt (elit);
     }
   }
-  internal->notified = 0;
-  LOG ("reset notified counter to 0");
+
+
 }
 
 bool External::observed (int elit) {
@@ -785,7 +791,9 @@ bool External::traverse_all_non_frozen_units_as_witnesses (
     int unit = tmp < 0 ? -idx : idx;
     const int ilit = e2i[idx] * (tmp < 0 ? -1 : 1);
     // heurstically add + max_var to the id to avoid reusing ids
-    const uint64_t id = internal->opts.lrat ? internal->unit_clauses[internal->vlit (ilit)] : 1;
+    const uint64_t id = internal->opts.lrat
+                            ? internal->unit_clauses[internal->vlit (ilit)]
+                            : 1;
     assert (id);
     clause_and_witness.push_back (unit);
     if (!it.witness (clause_and_witness, clause_and_witness, id + max_var))

src/external_propagate.cpp

@@ -182,7 +182,8 @@ bool Internal::external_propagate () {
         (void) res;
         bool trail_changed =
             (num_assigned != assigned || level != level_before ||
-             (opts.reimply && multitrail_dirty < level) || (!opts.reimply && propagated < trail.size()));
+             (opts.reimply && multitrail_dirty < level) ||
+             (!opts.reimply && propagated < trail.size ()));
 
         if (unsat || conflict)
           break;
@@ -230,7 +231,8 @@ bool Internal::external_propagate () {
         add_external_clause (0);
         bool trail_changed =
             (num_assigned != assigned || level != level_before ||
-             (opts.reimply && multitrail_dirty < level) || (!opts.reimply && propagated < trail.size()));
+             (opts.reimply && multitrail_dirty < level) ||
+             (!opts.reimply && propagated < trail.size ()));
 
         if (unsat || conflict)
           break;
@@ -763,7 +765,8 @@ bool Internal::external_check_solution () {
       add_external_clause (0);
       bool trail_changed =
           (num_assigned != assigned || level != level_before ||
-           (opts.reimply && multitrail_dirty < level) || (!opts.reimply && propagated < trail.size()));
+           (opts.reimply && multitrail_dirty < level) ||
+           (!opts.reimply && propagated < trail.size ()));
       added_new_clauses = true;
       //
       // There are many possible scenarios here:

src/file.cpp

@@ -35,8 +35,8 @@ File::File (Internal *i, bool w, int c, int p, FILE *f, const char *n)
 #if !defined(QUIET) || !defined(NDEBUG)
       writing (w),
 #endif
-      close_file (c), child_pid (p), file (f), _name (strdup (n)), _lineno (1),
-      _bytes (0) {
+      close_file (c), child_pid (p), file (f), _name (strdup (n)),
+      _lineno (1), _bytes (0) {
   (void) w;
   assert (f), assert (n);
 }
@@ -98,7 +98,7 @@ bool File::writable (const char *path) {
 bool File::piping () {
   struct stat stat;
   int fd = fileno (file);
-  if (fstat (fd,  &stat))
+  if (fstat (fd, &stat))
     return true;
   return S_ISFIFO (stat.st_mode);
 }

src/file.hpp

@@ -2,8 +2,8 @@
 #define _file_hpp_INCLUDED
 
 #include <cassert>
-#include <cstdio>
 #include <cstdint>
+#include <cstdio>
 #include <cstdlib>
 #include <vector>
 
@@ -68,7 +68,7 @@ class File {
   static bool writable (const char *path);     // can write to that file?
   static size_t size (const char *path);       // file size in bytes
 
-  bool piping ();		// Is opened file a pipe?
+  bool piping (); // Is opened file a pipe?
 
   // Does the file match the file type signature.
   //

src/idruptracer.cpp

@@ -152,7 +152,7 @@ void IdrupTracer::insert () {
 
 /*------------------------------------------------------------------------*/
 
-inline void IdrupTracer::flush_if_piping () { 
+inline void IdrupTracer::flush_if_piping () {
   if (piping)
     file->flush ();
 }
@@ -245,9 +245,8 @@ void IdrupTracer::idrup_add_original_clause (const vector<int> &clause) {
   // flush_if_piping ();
 }
 
-
 void IdrupTracer::idrup_delete_clause (uint64_t id,
-                                      const vector<int> &clause) {
+                                       const vector<int> &clause) {
   if (find_and_delete (id)) {
     assert (imported_clause.empty ());
     if (binary)
@@ -429,7 +428,8 @@ void IdrupTracer::add_original_clause (uint64_t id, bool,
   }
   assert (restored);
   if (find_and_delete (id)) {
-    LOG (clause, "IDRUP TRACER the clause was not yet weakened, so no restore");
+    LOG (clause,
+         "IDRUP TRACER the clause was not yet weakened, so no restore");
     return;
   }
   LOG (clause, "IDRUP TRACER tracing addition of restored clause");