Merge pull request #4449 from peterschrammel/solver-resource-limits

Factor out solver resource limits capability

Author: peterschrammel

src/goto-checker/solver_factory.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/flattening/bv_dimacs.h>
 #include <solvers/prop/prop.h>
 #include <solvers/prop/prop_conv.h>
+#include <solvers/prop/solver_resource_limits.h>
 #include <solvers/refinement/bv_refinement.h>
 #include <solvers/sat/dimacs_cnf.h>
 #include <solvers/sat/satcheck.h>
@@ -79,8 +80,21 @@ void solver_factoryt::set_prop_conv_time_limit(prop_convt &prop_conv)
 {
   const int timeout_seconds =
     options.get_signed_int_option("solver-time-limit");
+
   if(timeout_seconds > 0)
-    prop_conv.set_time_limit_seconds(timeout_seconds);
+  {
+    solver_resource_limitst *solver =
+      dynamic_cast<solver_resource_limitst *>(&prop_conv);
+    if(solver == nullptr)
+    {
+      messaget log(message_handler);
+      log.warning() << "cannot set solver time limit on "
+                    << prop_conv.decision_procedure_text() << messaget::eom;
+      return;
+    }
+
+    solver->set_time_limit_seconds(timeout_seconds);
+  }
 }
 
 void solver_factoryt::solvert::set_prop_conv(std::unique_ptr<prop_convt> p)

src/solvers/prop/prop_conv.h

@@ -42,9 +42,6 @@ class prop_convt:public decision_proceduret
   // returns true if an assumption is in the final conflict
   virtual bool is_in_conflict(literalt l) const;
   virtual bool has_is_in_conflict() const { return false; }
-
-  // Resource limits:
-  virtual void set_time_limit_seconds(uint32_t) {}
 };
 
 //

src/solvers/prop/prop_conv_solver.h

@@ -21,8 +21,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "literal_expr.h"
 #include "prop.h"
 #include "prop_conv.h"
+#include "solver_resource_limits.h"
 
-class prop_conv_solvert : public prop_convt
+class prop_conv_solvert : public prop_convt, public solver_resource_limitst
 {
 public:
   prop_conv_solvert(propt &_prop, message_handlert &message_handler)

src/solvers/prop/solver_resource_limits.h

@@ -0,0 +1,24 @@
+/*******************************************************************\
+
+Module: Solver capability to set resource limits
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Solver capability to set resource limits
+
+#ifndef CPROVER_SOLVERS_PROP_SOLVER_RESOURCE_LIMITS_H
+#define CPROVER_SOLVERS_PROP_SOLVER_RESOURCE_LIMITS_H
+
+class solver_resource_limitst
+{
+public:
+  /// Set the limit for the solver to time out in seconds
+  virtual void set_time_limit_seconds(uint32_t) = 0;
+
+  virtual ~solver_resource_limitst() = default;
+};
+
+#endif // CPROVER_SOLVERS_PROP_SOLVER_RESOURCE_LIMITS_H