tiny.smt.SolveStats

1/// Counts of the work one solve did. A caller reads them from `Solver.lastSolveStats` to report how2/// much work a solve took. The solver sets every count to zero when a solve starts. The counts3/// cover the main search: the extra solves of core minimization change only `proof_steps`, which4/// takes the certified trace's length.5pub const SolveStats = struct {6    /// Decisions the search made, each giving an unassigned variable a value.7    decisions: usize = 0,8    /// Decisions that gave the variable the value it last held, in this solve or an earlier one,9    /// counted within `decisions`.10    phase_saved_decisions: usize = 0,11    /// Literals the search assigned because every other literal of a clause was false. Unit clauses12    /// of the formula and assumptions sit outside the count.13    propagations: usize = 0,14    /// Times the main search found a clause with every literal false. `Solver.conflict_budget`15    /// limits this count.16    conflicts: usize = 0,17    /// Clauses the search learned from conflicts in this solve.18    learned_clauses: usize = 0,19    /// Learned clauses the solver removed to stay within `Solver.max_learned_clauses`, removals at20    /// the start of the solve included.21    evicted_clauses: usize = 0,22    /// Steps in the proof trace at the end of the solve: one per learned clause, plus the final23    /// empty clause after an unsatisfiable answer. After core minimization certified a smaller24    /// core, the count is the certifying solve's step count.25    proof_steps: usize = 0,26    /// Times the search went back to the first decision, on the restart schedule or to remove27    /// learned clauses.28    restarts: usize = 0,29    /// The largest number of decisions in force at once during the solve.30    max_decision_level: u32 = 0,31    /// Conflicts found at decision level zero, counted within `conflicts`. Assumptions sit below32    /// every decision, so a conflict among the assumptions counts here.33    root_conflicts: usize = 0,34};

1pub const SolveStats = sat.SolveStats;