Address review comments on solver state machine

- Wrap do_prop_solve() in try/catch to set ERROR state on exception
- Clarify decision_proceduret docs: D_ERROR represents unsolved or error
- Add PRECONDITION(!a.is_constant()) to CaDiCaL is_in_conflict()
- Add unit test for new_variable() invalidating SAT state
- Call clear_status() in cnft::new_variable() and cnft::new_variables()
- Document that ERROR state is intentionally sticky in clear_status()
- Invalidate latest_result in set_to_true/set_to_false

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

src/solvers/decision_procedure.cpp

@@ -34,10 +34,12 @@ decision_proceduret::operator()(const exprt &assumption)
 
 void decision_proceduret::set_to_true(const exprt &expr)
 {
+  latest_result = resultt::D_ERROR;
   set_to(expr, true);
 }
 
 void decision_proceduret::set_to_false(const exprt &expr)
 {
+  latest_result = resultt::D_ERROR;
   set_to(expr, false);
 }

src/solvers/decision_procedure.h

@@ -21,17 +21,18 @@ class exprt;
 ///
 /// A decision procedure follows a state machine:
 ///
-///   UNKNOWN ──operator()──► D_SATISFIABLE ──set_to()──► UNKNOWN
-///      ▲                        │
-///      │                        └──get() valid
-///      │
-///   UNKNOWN ──operator()──► D_UNSATISFIABLE ──set_to()──► UNKNOWN
+///   D_ERROR ──operator()──► D_SATISFIABLE ──set_to()──► D_ERROR
+///     ▲                        │
+///     │                        └──get() valid
+///     │
+///   D_ERROR ──operator()──► D_UNSATISFIABLE ──set_to()──► D_ERROR
 ///
-/// After construction, the procedure is in the UNKNOWN state. Calling
+/// After construction, the procedure's status (\ref latest_result) is
+/// initialised to D_ERROR, representing "not yet solved". Calling
 /// \ref operator() transitions to D_SATISFIABLE, D_UNSATISFIABLE, or D_ERROR.
 /// Reading the satisfying assignment via \ref get is only valid in the
 /// D_SATISFIABLE state. Adding new constraints (\ref set_to, \ref handle)
-/// transitions back to UNKNOWN.
+/// resets the status to D_ERROR.
 class decision_proceduret
 {
 public:

src/solvers/prop/prop.cpp

@@ -36,43 +36,51 @@ bvt propt::new_variables(std::size_t width)
   return result;
 }
 
+static propt::statust status_from_result(propt::resultt result)
+{
+  switch(result)
+  {
+  case propt::resultt::P_SATISFIABLE:
+    return propt::statust::SAT;
+  case propt::resultt::P_UNSATISFIABLE:
+    return propt::statust::UNSAT;
+  case propt::resultt::P_ERROR:
+    return propt::statust::ERROR;
+  }
+  UNREACHABLE;
+}
+
 propt::resultt propt::prop_solve()
 {
   static const bvt empty_assumptions;
   ++number_of_solver_calls;
-  auto result = do_prop_solve(empty_assumptions);
-  switch(result)
+  try
+  {
+    auto result = do_prop_solve(empty_assumptions);
+    solver_state = status_from_result(result);
+    return result;
+  }
+  catch(...)
   {
-  case resultt::P_SATISFIABLE:
-    solver_state = statust::SAT;
-    break;
-  case resultt::P_UNSATISFIABLE:
-    solver_state = statust::UNSAT;
-    break;
-  case resultt::P_ERROR:
     solver_state = statust::ERROR;
-    break;
+    throw;
   }
-  return result;
 }
 
 propt::resultt propt::prop_solve(const bvt &assumptions)
 {
   ++number_of_solver_calls;
-  auto result = do_prop_solve(assumptions);
-  switch(result)
+  try
+  {
+    auto result = do_prop_solve(assumptions);
+    solver_state = status_from_result(result);
+    return result;
+  }
+  catch(...)
   {
-  case resultt::P_SATISFIABLE:
-    solver_state = statust::SAT;
-    break;
-  case resultt::P_UNSATISFIABLE:
-    solver_state = statust::UNSAT;
-    break;
-  case resultt::P_ERROR:
     solver_state = statust::ERROR;
-    break;
+    throw;
   }
-  return result;
 }
 
 std::size_t propt::get_number_of_solver_calls() const

src/solvers/prop/prop.h

@@ -163,6 +163,8 @@ class propt
   virtual resultt do_prop_solve(const bvt &assumptions) = 0;
 
   /// Transition to UNKNOWN state when the solver is mutated.
+  /// The ERROR state is intentionally sticky: once the solver has encountered
+  /// an error, adding new constraints does not clear it.
   void clear_status()
   {
     if(solver_state == statust::SAT || solver_state == statust::UNSAT)

src/solvers/sat/cnf.cpp

@@ -384,6 +384,7 @@ literalt cnft::lselect(literalt a, literalt b, literalt c)
 /// \return New variable as literal
 literalt cnft::new_variable()
 {
+  clear_status();
   literalt l(_no_variables, false);
 
   set_no_variables(_no_variables+1);
@@ -395,6 +396,7 @@ literalt cnft::new_variable()
 /// \return Vector of new variables.
 bvt cnft::new_variables(std::size_t width)
 {
+  clear_status();
   bvt result;
   result.reserve(width);
 

src/solvers/sat/satcheck_cadical.cpp

@@ -197,6 +197,7 @@ satcheck_cadical_baset::~satcheck_cadical_baset()
 bool satcheck_cadical_baset::is_in_conflict(literalt a) const
 {
   PRECONDITION(solver_state == propt::statust::UNSAT);
+  PRECONDITION(!a.is_constant());
   return solver->failed(a.dimacs());
 }
 

unit/solvers/sat/satcheck_cadical.cpp

@@ -160,6 +160,16 @@ SCENARIO(
         REQUIRE(satcheck.get_status() == propt::statust::UNSAT);
       }
     }
+
+    WHEN("first solve is SAT, then add a new variable")
+    {
+      REQUIRE(satcheck.prop_solve() == propt::resultt::P_SATISFIABLE);
+      REQUIRE(satcheck.get_status() == propt::statust::SAT);
+
+      // Adding a new variable transitions state back to UNKNOWN
+      satcheck.new_variable();
+      REQUIRE(satcheck.get_status() == propt::statust::UNKNOWN);
+    }
   }
 }