Formalize solver state machine in propt and decision_proceduret

[tautschnig]

As suggested by @kroening in #8849, this formalizes the solver state machine in propt and decision_proceduret.

Commit 1: Document and track solver state machine

• Adds propt::statust enum (UNKNOWN, SAT, UNSAT, ERROR) and tracks state transitions:
  • prop_solve() sets state based on result
  • l_set_to() and lcnf() overloads call clear_status() to transition SAT/UNSAT → UNKNOWN
• Adds decision_proceduret::get_status() tracking latest_result
• Documents the state machine contract as class-level comments
• Adds unit tests verifying state transitions in CaDiCaL

Commit 2: Call clear_status() in all solver backends

• All SAT solver lcnf() implementations now call clear_status() at entry, ensuring the state machine is consistently enforced across all backends.

Commit 3: Enforce state preconditions

• l_get() requires SAT state, is_in_conflict() requires UNSAT state (via PRECONDITION)
• All existing regression and unit tests pass — the codebase already respects the state machine; this commit makes violations fail-fast.

Note: cnf_solvert::statust is retained for now (marked as legacy/superseded) since it is used by all do_prop_solve implementations. Unifying the two can be done as a follow-up.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

This PR formalizes and enforces a solver/decision-procedure “state machine” to make model/conflict queries fail-fast when called in invalid states, and to consistently invalidate solver results when the underlying solver is mutated.

Changes:

• Add propt::statust and track solver state transitions in prop_solve() plus invalidation via clear_status().
• Add decision_proceduret::get_status() tracking of the latest solve result, and document the intended state machine.
• Update SAT solver backends to call clear_status() at lcnf() entry; add CaDiCaL unit tests and CaDiCaL precondition checks for state-dependent APIs.

Reviewed changes

Copilot reviewed 16 out of 16 changed files in this pull request and generated 6 comments.

Show a summary per file

File	Description
unit/solvers/sat/satcheck_cadical.cpp	Adds unit tests for propt state transitions using CaDiCaL.
src/solvers/sat/satcheck_picosat.cpp	Invalidates propt solver state on clause addition (lcnf).
src/solvers/sat/satcheck_minisat2.cpp	Invalidates propt solver state on clause addition (lcnf).
src/solvers/sat/satcheck_minisat.cpp	Invalidates propt solver state on clause addition (lcnf).
src/solvers/sat/satcheck_lingeling.cpp	Invalidates propt solver state on clause addition (lcnf).
src/solvers/sat/satcheck_ipasir.cpp	Invalidates propt solver state on clause addition (lcnf).
src/solvers/sat/satcheck_glucose.cpp	Invalidates propt solver state on clause addition (lcnf).
src/solvers/sat/satcheck_cadical.cpp	Enforces SAT/UNSAT-only preconditions for model/conflict queries; invalidates state on lcnf.
src/solvers/sat/satcheck_booleforce.cpp	Invalidates propt solver state on clause addition (lcnf).
src/solvers/sat/dimacs_cnf.cpp	Invalidates propt solver state on clause “addition” for DIMACS dumping.
src/solvers/sat/cnf_clause_list.cpp	Invalidates propt solver state on clause addition to clause-list CNF.
src/solvers/sat/cnf.h	Documents legacy vs canonical status tracking (cnf_solvert::status vs propt::solver_state).
src/solvers/prop/prop.h	Documents propt state machine; adds statust, get_status(), and invalidation hooks in mutating APIs.
src/solvers/prop/prop.cpp	Updates prop_solve() to set solver_state based on solve result.
src/solvers/decision_procedure.h	Documents decision procedure state machine; adds get_status() / latest_result.
src/solvers/decision_procedure.cpp	Tracks latest solve result in operator().

Comments suppressed due to low confidence (1)

src/solvers/decision_procedure.cpp:43

• Per the documented state machine, adding constraints should transition back to UNKNOWN, but set_to_true/false don’t invalidate latest_result. After a SAT result, callers can add constraints and get_status() will still report D_SATISFIABLE even though the model is no longer valid. Consider resetting latest_result (or a dedicated UNKNOWN status) in these wrappers, and ensure other mutation entry points (e.g., handle() or direct set_to() implementations) also invalidate the status consistently.

void decision_proceduret::set_to_true(const exprt &expr)
{
  set_to(expr, true);
}

void decision_proceduret::set_to_false(const exprt &expr)
{
  set_to(expr, false);
}

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[codecov]

Codecov Report

❌ Patch coverage is 82.50000% with 7 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.01%. Comparing base (eaaf029) to head (30cc7c2).

Files with missing lines	Patch %	Lines
src/solvers/prop/prop.cpp	62.50%	6 Missing ⚠️
src/solvers/sat/dimacs_cnf.cpp	0.00%	1 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8852   +/-   ##
========================================
  Coverage    80.01%   80.01%           
========================================
  Files         1700     1700           
  Lines       188338   188373   +35     
  Branches        73       73           
========================================
+ Hits        150695   150723   +28     
- Misses       37643    37650    +7     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.