From d819fc29f4e88960e35dcd9c64f3daf2b1c71aa6 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sun, 17 Dec 2023 11:42:31 +0100 Subject: [PATCH 01/11] bumped version --- VERSION | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/VERSION b/VERSION index edf53098..cbb07ba9 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -1.9.1-dev.3 +1.9.2-rc.1 From 77ac74751e61a0eb10c40bf04bcb58dc2c202c88 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sun, 17 Dec 2023 11:43:10 +0100 Subject: [PATCH 02/11] formatted --- src/analyze.cpp | 12 +- src/assume.cpp | 18 ++- src/ccadical.cpp | 7 +- src/ccadical.h | 2 +- src/checker.hpp | 2 +- src/collect.cpp | 19 +-- src/extend.cpp | 6 +- src/external.cpp | 4 +- src/external_propagate.cpp | 9 +- src/file.cpp | 6 +- src/file.hpp | 4 +- src/idruptracer.cpp | 8 +- src/internal.cpp | 22 +-- src/internal.hpp | 2 +- src/mobical.cpp | 288 ++++++++++++++++++++----------------- src/propagate.cpp | 5 +- src/restart.cpp | 8 +- src/subsume.cpp | 2 +- src/tracer.hpp | 6 +- src/vivify.cpp | 3 +- 20 files changed, 237 insertions(+), 196 deletions(-) diff --git a/src/analyze.cpp b/src/analyze.cpp index 6c3ae80b..947abed8 100644 --- a/src/analyze.cpp +++ b/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 diff --git a/src/assume.cpp b/src/assume.cpp index a0775af9..89bfa0fa 100644 --- a/src/assume.cpp +++ b/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 -> %zd", 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; diff --git a/src/ccadical.cpp b/src/ccadical.cpp index 1e122a12..88ab164a 100644 --- a/src/ccadical.cpp +++ b/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 (); } - } diff --git a/src/ccadical.h b/src/ccadical.h index bcb9f70d..6d1b3ff0 100644 --- a/src/ccadical.h +++ b/src/ccadical.h @@ -7,8 +7,8 @@ extern "C" { #endif /*------------------------------------------------------------------------*/ -#include #include +#include // C wrapper for CaDiCaL's C++ API following IPASIR. diff --git a/src/checker.hpp b/src/checker.hpp index 79c5f60a..a6179801 100644 --- a/src/checker.hpp +++ b/src/checker.hpp @@ -158,7 +158,7 @@ class Checker : public StatTracer { void delete_clause (uint64_t, bool, const vector &) override; void finalize_clause (uint64_t, const vector &) 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 &, const vector &) override; diff --git a/src/collect.cpp b/src/collect.cpp index dd1b73ed..6255cbb2 100644 --- a/src/collect.cpp +++ b/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,7 +556,7 @@ 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 (); @@ -563,14 +564,15 @@ void Internal::remove_garbage_binaries () { 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); } diff --git a/src/extend.cpp b/src/extend.cpp index 8440a61d..20165e1e 100644 --- a/src/extend.cpp +++ b/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(*i); + const uint64_t id = + ((uint64_t) * (i - 1) << 32) + static_cast (*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(*(i + 1)); + const uint64_t id = + ((uint64_t) *i << 32) + static_cast (*(i + 1)); assert (id > 0); i += 3; assert (*i); diff --git a/src/external.cpp b/src/external.cpp index 8d6bf7ce..fc5feee3 100644 --- a/src/external.cpp +++ b/src/external.cpp @@ -785,7 +785,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)) diff --git a/src/external_propagate.cpp b/src/external_propagate.cpp index 8cf4959b..0e1fa68a 100644 --- a/src/external_propagate.cpp +++ b/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: diff --git a/src/file.cpp b/src/file.cpp index 970b20f5..ae163eb6 100644 --- a/src/file.cpp +++ b/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); } diff --git a/src/file.hpp b/src/file.hpp index bab113db..17e15a9d 100644 --- a/src/file.hpp +++ b/src/file.hpp @@ -2,8 +2,8 @@ #define _file_hpp_INCLUDED #include -#include #include +#include #include #include @@ -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. // diff --git a/src/idruptracer.cpp b/src/idruptracer.cpp index 7d55640c..d3d54df7 100644 --- a/src/idruptracer.cpp +++ b/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 &clause) { // flush_if_piping (); } - void IdrupTracer::idrup_delete_clause (uint64_t id, - const vector &clause) { + const vector &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"); diff --git a/src/internal.cpp b/src/internal.cpp index 12a062f6..2b26dfcd 100644 --- a/src/internal.cpp +++ b/src/internal.cpp @@ -787,7 +787,7 @@ int Internal::restore_clauses () { report ('*'); } else { report ('+'); - remove_garbage_binaries(); + remove_garbage_binaries (); external->restore_clauses (); internal->report ('r'); if (!unsat && !level && !propagate ()) { @@ -917,7 +917,7 @@ void Internal::dump () { /*------------------------------------------------------------------------*/ bool Internal::traverse_constraint (ClauseIterator &it) { - if (constraint.empty() && !unsat_constraint) + if (constraint.empty () && !unsat_constraint) return true; vector eclause; @@ -927,15 +927,15 @@ bool Internal::traverse_constraint (ClauseIterator &it) { LOG (constraint, "traversing constraint"); bool satisfied = false; for (auto ilit : constraint) { - const int tmp = fixed (ilit); - if (tmp > 0) { - satisfied = true; - break; - } - if (tmp < 0) - continue; - const int elit = externalize (ilit); - eclause.push_back (elit); + const int tmp = fixed (ilit); + if (tmp > 0) { + satisfied = true; + break; + } + if (tmp < 0) + continue; + const int elit = externalize (ilit); + eclause.push_back (elit); } if (!satisfied && !it.clause (eclause)) return false; diff --git a/src/internal.hpp b/src/internal.hpp index c49d90d1..e2aef88d 100644 --- a/src/internal.hpp +++ b/src/internal.hpp @@ -1051,7 +1051,7 @@ struct Internal { int next_propagation_level (int last); vector *next_trail (int l); int next_propagated (int l); - Clause *propagation_conflict (int *l, Clause *c, bool exact=false); + Clause *propagation_conflict (int *l, Clause *c, bool exact = false); int conflicting_level (Clause *c); void elevate_lit (int lit, Clause *reason); int elevating_level (int lit, Clause *reason); diff --git a/src/mobical.cpp b/src/mobical.cpp index 380a7bb8..4f2cff9d 100644 --- a/src/mobical.cpp +++ b/src/mobical.cpp @@ -220,33 +220,34 @@ class MockPropagator : public ExternalPropagator { bool tainting; bool propagation_reason; - int literals[]; //variadic size + int literals[]; // variadic size - int * begin () { return literals; } - int * end () { return literals + size; } + int *begin () { return literals; } + int *end () { return literals + size; } int next_lit () { - if (next < size) return literals[next++]; + if (next < size) + return literals[next++]; else { next = 0; return 0; } } }; - + // The list of all external lemmas (including reason clauses) - std::vector external_lemmas; - + std::vector external_lemmas; + // The reasons of present external propagations std::map reason_map; - + // Next lemma to add size_t add_lemma_idx = 0; // Forced lemme addition (falsified lemma in model) bool must_add_clause = false; size_t must_add_idx; - + // Next decision to make size_t decision_loc = 0; @@ -254,21 +255,21 @@ class MockPropagator : public ExternalPropagator { std::set observed_variables; std::vector new_observed_variables; std::deque> observed_trail; - + // Helpers size_t added_lemma_count = 0; size_t nof_clauses = 0; std::vector clause; bool new_ovars = false; - size_t add_new_lemma(bool forgettable) { - assert (clause.size() <= (size_t) INT_MAX); + size_t add_new_lemma (bool forgettable) { + assert (clause.size () <= (size_t) INT_MAX); assert (external_lemmas.size () <= (size_t) INT_MAX); size_t size = clause.size (); size_t bytes = sizeof (struct ExternalLemma) + size * sizeof (int); - ExternalLemma * lemma = (ExternalLemma*) new char [bytes]; + ExternalLemma *lemma = (ExternalLemma *) new char[bytes]; lemma->id = external_lemmas.size (); lemma->add_count = 0; @@ -278,8 +279,8 @@ class MockPropagator : public ExternalPropagator { lemma->tainting = true; lemma->propagation_reason = false; - int * q = lemma->literals; - for (const auto& lit : clause) + int *q = lemma->literals; + for (const auto &lit : clause) *q++ = lit; external_lemmas.push_back (lemma); @@ -287,15 +288,27 @@ class MockPropagator : public ExternalPropagator { return lemma->id; } - // Helper to print very verbose log during debugging + // Helper to print very verbose log during debugging - #ifdef LOGGING - #define MLOG(str) do { if (logging) std::cout << "[mock-propagator] " << str; } while( false ) - #define MLOGC(str) do { if (logging) std::cout << str; } while( false ) - #else - #define MLOG(str) do { } while ( false ) - #define MLOGC(str) do { } while ( false ) - #endif +#ifdef LOGGING +#define MLOG(str) \ + do { \ + if (logging) \ + std::cout << "[mock-propagator] " << str; \ + } while (false) +#define MLOGC(str) \ + do { \ + if (logging) \ + std::cout << str; \ + } while (false) +#else +#define MLOG(str) \ + do { \ + } while (false) +#define MLOGC(str) \ + do { \ + } while (false) +#endif public: // It is public, so it can be shared easily between different propagators @@ -312,23 +325,24 @@ class MockPropagator : public ExternalPropagator { /*-----------------functions for mobical -----------------------------*/ void push_lemma_lit (int lit) { - if (lit) clause.push_back (lit); + if (lit) + clause.push_back (lit); else { nof_clauses++; - + MLOG ("push lemma to position " << external_lemmas.size () << ": "); - for (auto const &l : clause) { - (void)l; + for (auto const &l : clause) { + (void) l; MLOGC (l << " "); } - MLOGC ( "0" << std::endl ); - - add_new_lemma(false); + MLOGC ("0" << std::endl); + + add_new_lemma (false); clause.clear (); } } - void add_observed_lit (int lit) { + void add_observed_lit (int lit) { // Zero lit indicates that the new observed variables start here if (!lit) { assert (!new_ovars); @@ -356,7 +370,7 @@ class MockPropagator : public ExternalPropagator { observed_variables.insert (lit); s->add_observed_var (lit); - + return lit; } return 0; @@ -368,26 +382,27 @@ class MockPropagator : public ExternalPropagator { } bool is_observed_now (int lit) { - return (observed_variables.find(abs(lit)) != observed_variables.end()); + return (observed_variables.find (abs (lit)) != + observed_variables.end ()); } - bool compare_trails () { - return true; - } + bool compare_trails () { return true; } /*-----------------functions for mobical ends ------------------------*/ /*-------------------------- Observer functions ----------------------*/ void notify_fixed_assignment (int lit) { MLOG ("notify_fixed_assignment: " << lit << " (current level: " - << observed_trail.size()-1 << ")" << std::endl); + << observed_trail.size () - 1 << ")" + << std::endl); - assert (std::find(observed_fixed.begin(),observed_fixed.end(), lit) == - observed_fixed.end()); + assert (std::find (observed_fixed.begin (), observed_fixed.end (), + lit) == observed_fixed.end ()); observed_fixed.push_back (lit); }; void add_prev_fixed (const std::vector &fixed_assignments) { - for (auto const& lit: fixed_assignments) notify_fixed_assignment (lit); + for (auto const &lit : fixed_assignments) + notify_fixed_assignment (lit); } /* ------------------------ Observer functions end -------------------*/ @@ -398,11 +413,11 @@ class MockPropagator : public ExternalPropagator { MLOG ("cb_check_found_model (" << model.size () << ") returns: "); // Model reconstruction can change the assignments of certain variables, - // but the internal trail of the solver and the propagator should be still - // in synchron. + // but the internal trail of the solver and the propagator should be + // still in synchron. assert (compare_trails ()); - - for (const auto lemma: external_lemmas) { + + for (const auto lemma : external_lemmas) { bool satisfied = false; for (const auto lit : *lemma) { @@ -416,7 +431,8 @@ class MockPropagator : public ExternalPropagator { } else { // if not satisfied, it must be falsified. search = std::find (model.begin (), model.end (), -lit); - assert (search != model.end ()); } + assert (search != model.end ()); + } } if (!satisfied) { @@ -425,23 +441,22 @@ class MockPropagator : public ExternalPropagator { must_add_clause = true; must_add_idx = lemma->id; - - MLOGC ("false (external clause " << lemma->id << "/" - << external_lemmas.size () - << " is not satisfied: (forgettable: " - << lemma->forgettable << ", size: " << lemma->size << "): " ); + MLOGC ("false (external clause " + << lemma->id << "/" << external_lemmas.size () + << " is not satisfied: (forgettable: " << lemma->forgettable + << ", size: " << lemma->size << "): "); for (auto const &l : *lemma) { MLOGC (l << " "); (void) l; } MLOGC (std::endl); - + return false; } } - - MLOGC( "true" << std::endl ); - + + MLOGC ("true" << std::endl); + return true; } @@ -451,15 +466,15 @@ class MockPropagator : public ExternalPropagator { return cb_has_external_clause (red); } - bool cb_has_external_clause (unsigned& clause_redundancy) { + bool cb_has_external_clause (unsigned &clause_redundancy) { MLOG ("cb_has_external_clause returns: "); assert (compare_trails ()); clause_redundancy = 0; - if (external_lemmas.empty()) { - MLOGC( "false (there are no external lemmas)." << std::endl ); + if (external_lemmas.empty ()) { + MLOGC ("false (there are no external lemmas)." << std::endl); return false; } @@ -472,17 +487,17 @@ class MockPropagator : public ExternalPropagator { if (external_lemmas[must_add_idx]->forgettable) clause_redundancy = 1; - MLOGC( "true (forced clause addition, " - << "forgettable: " << clause_redundancy - << " id: " << add_lemma_idx << ")." << std::endl ); - + MLOGC ("true (forced clause addition, " + << "forgettable: " << clause_redundancy + << " id: " << add_lemma_idx << ")." << std::endl); + added_lemma_count++; return true; } if (added_lemma_count > lemma_per_cb) { added_lemma_count = 0; - MLOGC( "false (lemma per CB treshold reached)." << std::endl ); + MLOGC ("false (lemma per CB treshold reached)." << std::endl); return false; } @@ -490,21 +505,21 @@ class MockPropagator : public ExternalPropagator { // 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()) { - + + while (add_lemma_idx < external_lemmas.size ()) { + if (!external_lemmas[add_lemma_idx]->add_count && - !external_lemmas[add_lemma_idx]->propagation_reason) { + !external_lemmas[add_lemma_idx]->propagation_reason) { - if (external_lemmas[add_lemma_idx]->forgettable) - clause_redundancy = 1; + if (external_lemmas[add_lemma_idx]->forgettable) + clause_redundancy = 1; - MLOGC ("true (new lemma was found, " - << "forgettable: " << clause_redundancy - << " id: " << add_lemma_idx << ")." << std::endl ); - - added_lemma_count++; - return true; + MLOGC ("true (new lemma was found, " + << "forgettable: " << clause_redundancy + << " id: " << add_lemma_idx << ")." << std::endl); + + added_lemma_count++; + return true; } // Forgettable lemmas are added repeatedly to the solver only when @@ -512,27 +527,28 @@ class MockPropagator : public ExternalPropagator { add_lemma_idx++; } - - MLOGC( "false." << std::endl ); + + MLOGC ("false." << std::endl); return false; } 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 << " (lemma " << add_lemma_idx << "/" + << external_lemmas.size () << ")" << std::endl); + + if (!lit) + external_lemmas[add_lemma_idx++]->add_count++; return lit; } int cb_decide () { - MLOG ( "cb_decide starts." << std::endl); - + MLOG ("cb_decide starts." << std::endl); + assert (compare_trails ()); if (observed_variables.empty () || observed_variables.size () <= 4) { @@ -566,27 +582,27 @@ class MockPropagator : public ExternalPropagator { } int cb_propagate () { - MLOGC ( "cb_propagate starts" << std::endl ); + MLOGC ("cb_propagate starts" << std::endl); assert (compare_trails ()); if (observed_trail.size () < 2) { - MLOG( "cb_propagate returns 0" - << " (less than two observed variables are assigned)." - << std::endl); + MLOG ("cb_propagate returns 0" + << " (less than two observed variables are assigned)." + << std::endl); return 0; } - + size_t lit_sum = 0; // sum of variables of satisfied observed literals - int lowest_lit = 0; // the lowest satisfied observed literal - int highest_lit = 0; // the highest satisfied observed literal + int lowest_lit = 0; // the lowest satisfied observed literal + int highest_lit = 0; // the highest satisfied observed literal std::set satisfied_literals = - current_observed_satisfied_set(lit_sum, lowest_lit, highest_lit); - - if (satisfied_literals.empty()) { - MLOGC( "cb_propagate returns 0" - << " (there are no observed satisfied literals)." - << std::endl); + current_observed_satisfied_set (lit_sum, lowest_lit, highest_lit); + + if (satisfied_literals.empty ()) { + MLOGC ("cb_propagate returns 0" + << " (there are no observed satisfied literals)." + << std::endl); return 0; } @@ -607,42 +623,43 @@ class MockPropagator : public ExternalPropagator { } if (!unassigned_var) { - MLOG( "cb_propagate returns 0" - << " (there are no unassigned observed variables)." - << std::endl); + MLOG ("cb_propagate returns 0" + << " (there are no unassigned observed variables)." + << std::endl); return 0; } - assert (clause.empty()); + assert (clause.empty ()); int propagated_lit = 0; if (lit_sum % 5 == 0 && satisfied_literals.size () > 1) { - clause = { unassigned_var, -1 * lowest_lit, -1 * highest_lit}; + clause = {unassigned_var, -1 * lowest_lit, -1 * highest_lit}; } else if (lit_sum % 7 == 0 && satisfied_literals.size () > 0) { - clause = { unassigned_var, -1 * highest_lit}; + clause = {unassigned_var, -1 * highest_lit}; } else if (lit_sum % 11 == 0) { - clause = { unassigned_var }; + clause = {unassigned_var}; } else if (lit_sum > 15 && lowest_lit) { // Propagate a falsified literal, ok if lowest == highest - clause = {-1 * lowest_lit, -1 * highest_lit }; + clause = {-1 * lowest_lit, -1 * highest_lit}; } - if (!clause.empty()) { + if (!clause.empty ()) { propagated_lit = clause[0]; size_t id = add_new_lemma (true); external_lemmas[id]->propagation_reason = true; reason_map[propagated_lit] = id; - clause.clear(); + clause.clear (); } - MLOG( "cb_propagate returns " << propagated_lit << std::endl ); + MLOG ("cb_propagate returns " << propagated_lit << std::endl); return propagated_lit; } int cb_add_reason_clause_lit (int plit) { - // At that point there is no need to assume that the trails are in synchron. + // At that point there is no need to assume that the trails are in + // synchron. assert (reason_map.find (plit) != reason_map.end ()); size_t reason_id = reason_map[plit]; @@ -651,16 +668,17 @@ class MockPropagator : public ExternalPropagator { if (!lit) { external_lemmas[reason_id]->add_count++; - MLOG ( "reason clause (id: " << reason_id << ") is added." << std::endl ); + MLOG ("reason clause (id: " << reason_id << ") is added." + << std::endl); } return lit; } void notify_assignment (int lit, bool is_fixed) { - MLOG ( "notify assignment: " << lit << " (current level: " - << observed_trail.size()-1 << ", is_fixed: " - << is_fixed << ")" << std::endl ); + MLOG ("notify assignment: " + << lit << " (current level: " << observed_trail.size () - 1 + << ", is_fixed: " << is_fixed << ")" << std::endl); if (is_fixed) { observed_trail.front ().push_back (lit); } else { @@ -669,43 +687,44 @@ class MockPropagator : public ExternalPropagator { } void notify_new_decision_level () { - MLOG ( "notify new decision level " - << observed_trail.size() << " -> " - << observed_trail.size() + 1 << std::endl ); + MLOG ("notify new decision level " << observed_trail.size () << " -> " + << observed_trail.size () + 1 + << std::endl); observed_trail.push_back (std::vector ()); } void notify_backtrack (size_t new_level) { - MLOG ( "notify backtrack: " << observed_trail.size () - 1 - << " -> " << new_level << std::endl ); + MLOG ("notify backtrack: " << observed_trail.size () - 1 << " -> " + << new_level << std::endl); assert (observed_trail.size () == 1 || observed_trail.size () >= new_level + 1); while (observed_trail.size () > new_level + 1) { - // Remove reason clause of backtracked assignments (keep it as lemma) - for (auto lit : observed_trail.back()) { - if (reason_map.find (lit) != reason_map.end ()) { - size_t reason_id = reason_map[lit]; - assert (reason_id < external_lemmas.size()); - external_lemmas[reason_id]->propagation_reason = false; - external_lemmas[reason_id]->forgettable = true; - reason_map.erase (lit); - } + // Remove reason clause of backtracked assignments (keep it as lemma) + for (auto lit : observed_trail.back ()) { + if (reason_map.find (lit) != reason_map.end ()) { + size_t reason_id = reason_map[lit]; + assert (reason_id < external_lemmas.size ()); + external_lemmas[reason_id]->propagation_reason = false; + external_lemmas[reason_id]->forgettable = true; + reason_map.erase (lit); } - observed_trail.pop_back (); + } + observed_trail.pop_back (); } } -/* ----------------- ExternalPropagator functions end ------------------*/ - + /* ----------------- ExternalPropagator functions end ------------------*/ /* -------------------------- Helper functions ---------------------- */ - std::set current_observed_satisfied_set (size_t& lit_sum, int& lowest_lit, int& highest_lit) { - + std::set current_observed_satisfied_set (size_t &lit_sum, + int &lowest_lit, + int &highest_lit) { + lit_sum = 0; lowest_lit = 0; highest_lit = 0; std::set satisfied_literals; - + for (auto level_lits : observed_trail) { for (auto lit : level_lits) { if (!s->observed (lit)) @@ -714,7 +733,8 @@ class MockPropagator : public ExternalPropagator { satisfied_literals.insert (lit); lit_sum += abs (lit); - if (!lowest_lit) lowest_lit = lit; + if (!lowest_lit) + lowest_lit = lit; highest_lit = lit; } } @@ -2040,7 +2060,7 @@ void Trace::generate_propagator (Random &random, int minvars, int maxvars) { // Give a chance to add no observed variables at all if (random.generate_double () < 0.05) - return; + return; for (int idx = minvars; idx <= maxvars; idx++) { if (random.generate_double () < 0.6) diff --git a/src/propagate.cpp b/src/propagate.cpp index 72082fb8..e0a2c63c 100644 --- a/src/propagate.cpp +++ b/src/propagate.cpp @@ -314,7 +314,7 @@ bool Internal::propagate () { continue; // blocking literal satisfied if (w.binary ()) { - + // assert (w.clause->redundant || !w.clause->garbage); // In principle we can ignore garbage binary clauses too, but that @@ -854,7 +854,8 @@ inline int Internal::next_propagation_level (int last) { // returns a conflict of conflicting_level at most l // -inline Clause *Internal::propagation_conflict (int *lp, Clause *c, bool exact) { +inline Clause *Internal::propagation_conflict (int *lp, Clause *c, + bool exact) { int l = *lp; if (c) conflicts.push_back (c); diff --git a/src/restart.cpp b/src/restart.cpp index a1c9131b..f08deb24 100644 --- a/src/restart.cpp +++ b/src/restart.cpp @@ -93,14 +93,16 @@ int Internal::reuse_trail () { assert (1 <= decision); int res = trivial_decisions; if (use_scores ()) { - while (res < level && control[res + 1].decision && - score_smaller (this) (decision, abs (control[res + 1].decision))) { + while ( + res < level && control[res + 1].decision && + score_smaller (this) (decision, abs (control[res + 1].decision))) { assert (control[res + 1].decision || opts.reimply); res++; } } else { int64_t limit = bumped (decision); - while (res < level && control[res + 1].decision && bumped (control[res + 1].decision) > limit) { + while (res < level && control[res + 1].decision && + bumped (control[res + 1].decision) > limit) { assert (control[res + 1].decision || opts.reimply); res++; } diff --git a/src/subsume.cpp b/src/subsume.cpp index 268d676e..ca8e0a56 100644 --- a/src/subsume.cpp +++ b/src/subsume.cpp @@ -259,7 +259,7 @@ inline int Internal::try_to_subsume_clause (Clause *c, dummy.literals[1] = other; flipped = (sign < 0) ? -lit : INT_MIN; } - dummy.moved = false; + dummy.moved = false; dummy.redundant = false; dummy.size = 2; dummy.id = bin.id; diff --git a/src/tracer.hpp b/src/tracer.hpp index 9c3d184e..68ac58f1 100644 --- a/src/tracer.hpp +++ b/src/tracer.hpp @@ -30,7 +30,8 @@ class Tracer { // Includes ID and wether the clause is redundant or irredundant // Arguments: ID, redundant, clause, restored // - virtual void add_original_clause (uint64_t, bool, const std::vector &, + virtual void add_original_clause (uint64_t, bool, + const std::vector &, bool = false) {} // Notify the observer that a new clause has been derived. @@ -121,7 +122,8 @@ class Tracer { // assumption clause or the ids of the failing constrain clauses // Arguments: conclusion_type, clause_ids // - virtual void conclude_unsat (ConclusionType, const std::vector &) {} + virtual void conclude_unsat (ConclusionType, + const std::vector &) {} // Notify the observer that conclude sat was requested. // will give the complete model as a vector. diff --git a/src/vivify.cpp b/src/vivify.cpp index 25a27449..03b5c024 100644 --- a/src/vivify.cpp +++ b/src/vivify.cpp @@ -1191,7 +1191,8 @@ void Internal::vivify_round (bool redundant_mode, connect_watches (!redundant_mode); // watch all relevant clauses - // the clauses might still contain set literals, so propagation since the beginning + // the clauses might still contain set literals, so propagation since the + // beginning propagated2 = propagated = 0; if (!unsat && !propagate ()) { From 37e13fc1679eb27e0b61d34e2d5f36e09daeae26 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sun, 17 Dec 2023 11:52:21 +0100 Subject: [PATCH 03/11] worked on NEWS for 1.9.2 --- NEWS.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/NEWS.md b/NEWS.md index 11f58efb..4d92e898 100644 --- a/NEWS.md +++ b/NEWS.md @@ -1,3 +1,18 @@ +Version 1.9.2 +------------- + +- 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 ------------- From 76f62045e82f1b11b6df09af162b7ff6f0a593ab Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sun, 17 Dec 2023 12:06:23 +0100 Subject: [PATCH 04/11] fixed bogus assertion for #80 --- src/external.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/external.cpp b/src/external.cpp index fc5feee3..4716fd17 100644 --- a/src/external.cpp +++ b/src/external.cpp @@ -392,7 +392,7 @@ 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 ()); + assert (!max_var || (size_t) max_var + 1 == is_observed.size ()); for (auto elit : vars) { int eidx = abs (elit); From 36a02d276f69df776366c9dbba2732d0667d1426 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sun, 17 Dec 2023 12:40:03 +0100 Subject: [PATCH 05/11] fixed issue #70 --- src/backtrack.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/backtrack.cpp b/src/backtrack.cpp index cceb289e..b7506b78 100644 --- a/src/backtrack.cpp +++ b/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); From 709a322518c33d5a0d45e15917b391c95968ab84 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sun, 17 Dec 2023 12:44:03 +0100 Subject: [PATCH 06/11] bumped version --- NEWS.md | 6 ++++-- src/version.cpp | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/NEWS.md b/NEWS.md index 4d92e898..2ab027b5 100644 --- a/NEWS.md +++ b/NEWS.md @@ -1,9 +1,11 @@ Version 1.9.2 ------------- -- Fixes for ILB, trail-reuse and external propagation with assumptions. +- Important fixes for ILB, trail-reuse and external propagation with + assumptions. -- Restored effectiveness of Mobical and improved external mock propagator. +- Restored effectiveness of Mobical and improved external mock + propagator. - Forced garbage collection of binary clauses before restore. diff --git a/src/version.cpp b/src/version.cpp index 6c4af6b7..48337b65 100644 --- a/src/version.cpp +++ b/src/version.cpp @@ -24,7 +24,7 @@ #ifdef NBUILD #ifndef VERSION -#define VERSION "1.9.1" +#define VERSION "1.9.2-rc.1" #endif // VERSION #endif // NBUILD From 2505c5f19d5c5776f3754a941471fd66e8c15ee9 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sun, 17 Dec 2023 13:05:26 +0100 Subject: [PATCH 07/11] fixed issue with C99 only flexible array member --- src/mobical.cpp | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/mobical.cpp b/src/mobical.cpp index 4f2cff9d..90c16db3 100644 --- a/src/mobical.cpp +++ b/src/mobical.cpp @@ -220,7 +220,10 @@ class MockPropagator : public ExternalPropagator { bool tainting; bool propagation_reason; - int literals[]; // variadic size + // Flexible array members are a C99 feature and not in C++11! + // Thus pedantic compilation fails for 'int literals[]'. + // + int *literals; int *begin () { return literals; } int *end () { return literals + size; } @@ -267,9 +270,8 @@ class MockPropagator : public ExternalPropagator { assert (external_lemmas.size () <= (size_t) INT_MAX); size_t size = clause.size (); - size_t bytes = sizeof (struct ExternalLemma) + size * sizeof (int); - - ExternalLemma *lemma = (ExternalLemma *) new char[bytes]; + ExternalLemma *lemma = new ExternalLemma; + lemma->literals = new int[size]; lemma->id = external_lemmas.size (); lemma->add_count = 0; @@ -320,7 +322,10 @@ class MockPropagator : public ExternalPropagator { logging = logging || with_logging; } - ~MockPropagator () {} + ~MockPropagator () { + for (auto l : external_lemmas) + delete l->literals, delete l; + } /*-----------------functions for mobical -----------------------------*/ void push_lemma_lit (int lit) { From 6cc0ce709e896c709c2354bb2432fee2cc81e51a Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sun, 17 Dec 2023 13:13:56 +0100 Subject: [PATCH 08/11] fixed wront format --- src/assume.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/assume.cpp b/src/assume.cpp index 89bfa0fa..8b63078c 100644 --- a/src/assume.cpp +++ b/src/assume.cpp @@ -542,7 +542,7 @@ void Internal::sort_and_reuse_assumptions () { if (!val (litA) && !val (litB)) return litA < litB; assert (val (litA) && val (litB)); - LOG ("%d -> %zd", litA, + LOG ("%d -> %" PRIu64, litA, ((uint64_t) var (litA).level << 32) + (uint64_t) var (litA).trail); return ((uint64_t) var (litA).level << 32) + From ac48dd6447f90ef6cca2d953387089941d1b13f4 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sun, 17 Dec 2023 14:52:26 +0100 Subject: [PATCH 09/11] bumped version to new release --- VERSION | 2 +- src/version.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/VERSION b/VERSION index cbb07ba9..8fdcf386 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -1.9.2-rc.1 +1.9.2 diff --git a/src/version.cpp b/src/version.cpp index 48337b65..7d89dd64 100644 --- a/src/version.cpp +++ b/src/version.cpp @@ -24,7 +24,7 @@ #ifdef NBUILD #ifndef VERSION -#define VERSION "1.9.2-rc.1" +#define VERSION "1.9.2" #endif // VERSION #endif // NBUILD From 2e73459c6c2e3eaff699863308872609d0f0cc5a Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sun, 17 Dec 2023 17:17:47 +0100 Subject: [PATCH 10/11] updated version for development --- VERSION | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/VERSION b/VERSION index 8fdcf386..cf2f79a6 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -1.9.2 +1.9.2-dev.1 From d1146672fd7b5d0921a5c2aa41398550eb551a34 Mon Sep 17 00:00:00 2001 From: Katalin Fazekas Date: Mon, 18 Dec 2023 06:43:01 +0100 Subject: [PATCH 11/11] fix propagator notification when ILB keeps unsat state that was found by preprocessing --- src/external.cpp | 10 ++++++++-- src/internal.cpp | 2 ++ src/mobical.cpp | 4 ++-- 3 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/external.cpp b/src/external.cpp index 4716fd17..fa97708a 100644 --- a/src/external.cpp +++ b/src/external.cpp @@ -392,6 +392,12 @@ void External::reset_observed_vars () { // Shouldn't be called if there is no connected propagator assert (propagator); reset_extended (); + + 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) { @@ -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) { diff --git a/src/internal.cpp b/src/internal.cpp index 2b26dfcd..54fc4c36 100644 --- a/src/internal.cpp +++ b/src/internal.cpp @@ -602,11 +602,13 @@ void Internal::produce_failed_assumptions () { assert (!assumptions.empty ()); while (!unsat) { assert (!satisfied ()); + notify_assignments (); if (decide ()) break; while (!unsat && !propagate ()) analyze (); } + notify_assignments (); if (unsat) LOG ("formula is actually unsatisfiable unconditionally"); else diff --git a/src/mobical.cpp b/src/mobical.cpp index 90c16db3..0822a87b 100644 --- a/src/mobical.cpp +++ b/src/mobical.cpp @@ -692,8 +692,8 @@ class MockPropagator : public ExternalPropagator { } void notify_new_decision_level () { - MLOG ("notify new decision level " << observed_trail.size () << " -> " - << observed_trail.size () + 1 + MLOG ("notify new decision level " << observed_trail.size () -1 << " -> " + << observed_trail.size () << std::endl); observed_trail.push_back (std::vector ()); }