Skip to content

Commit 32e0beb

Browse files
msoosclaude
andcommitted
Expose conflict count via Solver::conflicts()
statistics() prints the cumulative conflict count but there was no programmatic accessor for it. Add int64_t Solver::conflicts() mirroring redundant()/irredundant(), reading internal->stats.conflicts. Valid in both VALID and SOLVING state so it can be queried between solve() calls. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 392e90f commit 32e0beb

2 files changed

Lines changed: 17 additions & 0 deletions

File tree

src/cadical.hpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -686,6 +686,15 @@ class Solver {
686686
int64_t redundant () const; // Number of active redundant clauses.
687687
int64_t irredundant () const; // Number of active irredundant clauses.
688688

689+
// Cumulative number of conflicts generated during search, as also
690+
// reported by 'statistics ()'. Valid both in 'VALID' and 'SOLVING'
691+
// state so it can be queried after (or between) 'solve' calls.
692+
//
693+
// require (VALID | SOLVING)
694+
// ensure (VALID | SOLVING)
695+
//
696+
int64_t conflicts () const;
697+
689698
//------------------------------------------------------------------------
690699
// This function executes the given number of preprocessing rounds. It is
691700
// similar to 'solve' with 'limits ("preprocessing", rounds)' except that

src/solver.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1068,6 +1068,14 @@ int64_t Solver::irredundant () const {
10681068
return res;
10691069
}
10701070

1071+
int64_t Solver::conflicts () const {
1072+
TRACE ("conflicts");
1073+
REQUIRE_VALID_OR_SOLVING_STATE ();
1074+
int64_t res = internal->stats.conflicts;
1075+
LOG_API_CALL_RETURNS ("conflicts", res);
1076+
return res;
1077+
}
1078+
10711079
/*------------------------------------------------------------------------*/
10721080

10731081
void Solver::freeze (int lit) {

0 commit comments

Comments
 (0)