Formalize solver state machine in propt and decision_proceduret

src/solvers/decision_procedure.cpp

@@ -19,21 +19,27 @@ decision_proceduret::~decision_proceduret()
 
 decision_proceduret::resultt decision_proceduret::operator()()
 {
-  return dec_solve(nil_exprt());
+  auto result = dec_solve(nil_exprt());
+  latest_result = result;
+  return result;
 }
 
 decision_proceduret::resultt
 decision_proceduret::operator()(const exprt &assumption)
 {
-  return dec_solve(assumption);
+  auto result = dec_solve(assumption);
+  latest_result = result;
+  return result;
 }
 
 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

@@ -18,6 +18,21 @@ Author: Daniel Kroening, kroening@kroening.com
 class exprt;
 
 /// An interface for a decision procedure for satisfiability problems.
+///
+/// A decision procedure follows a state machine:
+///
+///   D_ERROR ──operator()──► D_SATISFIABLE ──set_to()──► D_ERROR
+///     ▲                        │
+///     │                        └──get() valid
+///     │
+///   D_ERROR ──operator()──► D_UNSATISFIABLE ──set_to()──► D_ERROR
+///
+/// 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)
+/// resets the status to D_ERROR.
 class decision_proceduret
 {
 public:
@@ -59,7 +74,8 @@ class decision_proceduret
 
   /// Return \p expr with variables replaced by values from satisfying
   /// assignment if available.
-  /// Return `nil` if not available
+  /// Return `nil` if not available.
+  /// \pre The last call to \ref operator()() returned D_SATISFIABLE.
   virtual exprt get(const exprt &) const = 0;
 
   /// Print satisfying assignment to \p out
@@ -73,9 +89,18 @@ class decision_proceduret
 
   virtual ~decision_proceduret();
 
+  /// Return the result of the last call to \ref operator()().
+  /// \return The most recent result, or D_ERROR if not yet called.
+  resultt get_status() const
+  {
+    return latest_result;
+  }
+
 protected:
   /// Implementation of the decision procedure.
   virtual resultt dec_solve(const exprt &assumption) = 0;
+
+  resultt latest_result = resultt::D_ERROR;
 };
 
 /// Add Boolean constraint \p src to decision procedure \p dest

src/solvers/prop/prop.cpp

@@ -36,17 +36,54 @@ 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;
-  return do_prop_solve(empty_assumptions);
+  // Some do_prop_solve() implementations may throw (e.g., on solver
+  // interruption). Ensure solver_state is set to ERROR in that case so that
+  // l_get()/is_in_conflict() preconditions will fail.
+  try
+  {
+    auto result = do_prop_solve(empty_assumptions);
+    solver_state = status_from_result(result);
+    return result;
+  }
+  catch(...)
+  {
+    solver_state = statust::ERROR;
+    throw;
+  }
 }
 
 propt::resultt propt::prop_solve(const bvt &assumptions)
 {
   ++number_of_solver_calls;
-  return do_prop_solve(assumptions);
+  try
+  {
+    auto result = do_prop_solve(assumptions);
+    solver_state = status_from_result(result);
+    return result;
+  }
+  catch(...)
+  {
+    solver_state = statust::ERROR;
+    throw;
+  }
 }
 
 std::size_t propt::get_number_of_solver_calls() const

src/solvers/prop/prop.h

@@ -19,8 +19,39 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cstdint>
 
-/*! \brief TO_BE_DOCUMENTED
-*/
+/// \brief Abstract interface for propositional logic solvers.
+///
+/// Provides the common API for constructing propositional formulas and solving
+/// them. Formulas are built from \ref literalt variables obtained via
+/// \ref new_variable, combined using Boolean operators (\ref land, \ref lor,
+/// etc.), and constrained via clauses (\ref lcnf) or unit constraints
+/// (\ref l_set_to). Calling \ref prop_solve checks satisfiability; the
+/// satisfying assignment can then be read via \ref l_get, or, in the
+/// unsatisfiable case, the conflict queried via \ref is_in_conflict.
+///
+/// Concrete implementations include SAT solvers (MiniSat, CaDiCaL, etc.)
+/// and structural representations (DIMACS file output, AIG).
+///
+/// The solver supports incremental use: after solving, new constraints or
+/// variables may be added and the solver invoked again. The state machine
+/// below describes which operations are valid in each state.
+///
+/// A propositional solver follows a state machine:
+///
+///   UNKNOWN ──prop_solve()──► SAT ──lcnf()/new_variable()──► UNKNOWN
+///      ▲                      │
+///      │                      └──l_get() valid
+///      │
+///   UNKNOWN ──prop_solve()──► UNSAT ──lcnf()/new_variable()──► UNKNOWN
+///                              │
+///                              └──is_in_conflict() valid
+///
+/// After construction, the solver is in the UNKNOWN state. Calling
+/// \ref prop_solve transitions to SAT, UNSAT, or ERROR. Reading the
+/// satisfying assignment via \ref l_get is only valid in the SAT state.
+/// Querying \ref is_in_conflict is only valid in the UNSAT state.
+/// Adding new constraints (\ref lcnf, \ref l_set_to) or variables
+/// (\ref new_variable) transitions back to UNKNOWN.
 class propt
 {
 public:
@@ -46,6 +77,7 @@ class propt
 
   virtual void l_set_to(literalt a, bool value)
   {
+    clear_status();
     set_equal(a, const_literal(value));
   }
 
@@ -56,10 +88,17 @@ class propt
 
   // constraints
   void lcnf(literalt l0, literalt l1)
-  { lcnf_bv.resize(2); lcnf_bv[0]=l0; lcnf_bv[1]=l1; lcnf(lcnf_bv); }
+  {
+    clear_status();
+    lcnf_bv.resize(2);
+    lcnf_bv[0] = l0;
+    lcnf_bv[1] = l1;
+    lcnf(lcnf_bv);
+  }
 
   void lcnf(literalt l0, literalt l1, literalt l2)
   {
+    clear_status();
     lcnf_bv.resize(3);
     lcnf_bv[0]=l0;
     lcnf_bv[1]=l1;
@@ -69,6 +108,7 @@ class propt
 
   void lcnf(literalt l0, literalt l1, literalt l2, literalt l3)
   {
+    clear_status();
     lcnf_bv.resize(4);
     lcnf_bv[0]=l0;
     lcnf_bv[1]=l1;
@@ -102,6 +142,21 @@ class propt
   resultt prop_solve();
   resultt prop_solve(const bvt &assumptions);
 
+  /// Solver state: tracks whether the model or conflict can be queried.
+  enum class statust
+  {
+    UNKNOWN,
+    SAT,
+    UNSAT,
+    ERROR
+  };
+
+  /// Return the current solver state.
+  statust get_status() const
+  {
+    return solver_state;
+  }
+
   // satisfying assignment
   virtual tvt l_get(literalt a) const=0;
   virtual void set_assignment(literalt a, bool value) = 0;
@@ -128,11 +183,21 @@ class propt
   // solve under the given assumption
   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)
+      solver_state = statust::UNKNOWN;
+  }
+
   // to avoid a temporary for lcnf(...)
   bvt lcnf_bv;
 
   messaget log;
   std::size_t number_of_solver_calls = 0;
+  statust solver_state = statust::UNKNOWN;
 };
 
 #endif // CPROVER_SOLVERS_PROP_PROP_H

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/cnf.h

@@ -83,6 +83,8 @@ class cnf_solvert:public cnft
   }
 
 protected:
+  // Legacy status tracking in do_prop_solve implementations.
+  // The canonical state is now propt::solver_state, updated by prop_solve().
   enum class statust { INIT, SAT, UNSAT, ERROR };
   statust status;
   size_t clause_counter;

src/solvers/sat/cnf_clause_list.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 void cnf_clause_listt::lcnf(const bvt &bv)
 {
+  clear_status();
   bvt new_bv;
 
   if(process_clause(bv, new_bv))

src/solvers/sat/dimacs_cnf.cpp

@@ -97,5 +97,6 @@ void dimacs_cnft::write_clauses(std::ostream &out) const
 
 void dimacs_cnf_dumpt::lcnf(const bvt &bv)
 {
+  clear_status();
   dimacs_cnft::write_dimacs_clause(bv, out, true);
 }

src/solvers/sat/satcheck_booleforce.cpp

@@ -65,6 +65,7 @@ std::string satcheck_booleforce_baset::solver_text() const
 
 void satcheck_booleforce_baset::lcnf(const bvt &bv)
 {
+  clear_status();
   bvt tmp;
 
   if(process_clause(bv, tmp))

src/solvers/sat/satcheck_cadical.cpp

@@ -19,6 +19,7 @@ Author: Michael Tautschnig
 
 tvt satcheck_cadical_baset::l_get(literalt a) const
 {
+  PRECONDITION(solver_state == propt::statust::SAT);
   if(a.is_constant())
     return tvt(a.sign());
 
@@ -45,6 +46,8 @@ std::string satcheck_cadical_baset::solver_text() const
 
 void satcheck_cadical_baset::lcnf(const bvt &bv)
 {
+  clear_status();
+
   for(const auto &lit : bv)
   {
     if(lit.is_true())
@@ -193,6 +196,8 @@ 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());
 }
 

src/solvers/sat/satcheck_glucose.cpp

@@ -108,6 +108,7 @@ void satcheck_glucose_baset<T>::add_variables()
 template<typename T>
 void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
 {
+  clear_status();
   try
   {
     add_variables();

src/solvers/sat/satcheck_ipasir.cpp

@@ -66,6 +66,7 @@ std::string satcheck_ipasirt::solver_text() const
 
 void satcheck_ipasirt::lcnf(const bvt &bv)
 {
+  clear_status();
   for(const auto &literal : bv)
   {
     if(literal.is_true())

src/solvers/sat/satcheck_lingeling.cpp

@@ -50,6 +50,7 @@ std::string satcheck_lingelingt::solver_text() const
 
 void satcheck_lingelingt::lcnf(const bvt &bv)
 {
+  clear_status();
   bvt new_bv;
 
   if(process_clause(bv, new_bv))

src/solvers/sat/satcheck_minisat.cpp

@@ -121,6 +121,7 @@ void satcheck_minisat1_baset::add_variables()
 
 void satcheck_minisat1_baset::lcnf(const bvt &bv)
 {
+  clear_status();
   bvt new_bv;
 
   if(process_clause(bv, new_bv))

src/solvers/sat/satcheck_minisat2.cpp

@@ -137,6 +137,7 @@ void satcheck_minisat2_baset<T>::add_variables()
 template<typename T>
 void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
 {
+  clear_status();
   try
   {
     add_variables();

src/solvers/sat/satcheck_picosat.cpp

@@ -50,6 +50,7 @@ std::string satcheck_picosatt::solver_text() const
 
 void satcheck_picosatt::lcnf(const bvt &bv)
 {
+  clear_status();
   bvt new_bv;
 
   if(process_clause(bv, new_bv))