Make dec_solve protected

According to comment in the code.

Author: peterschrammel

jbmc/src/jbmc/bmc.cpp

@@ -54,7 +54,7 @@ decision_proceduret::resultt bmct::run_decision_procedure()
 
   status() << "Running " << prop_conv.decision_procedure_text() << eom;
 
-  decision_proceduret::resultt dec_result = prop_conv.dec_solve();
+  decision_proceduret::resultt dec_result = prop_conv();
 
   {
     auto solver_stop = std::chrono::steady_clock::now();

src/goto-checker/goto_symex_property_decider.cpp

@@ -103,7 +103,7 @@ void goto_symex_property_decidert::add_constraint_from_goals(
 
 decision_proceduret::resultt goto_symex_property_decidert::solve()
 {
-  return solver->prop_conv().dec_solve();
+  return solver->prop_conv()();
 }
 
 prop_convt &goto_symex_property_decidert::get_solver() const

src/goto-instrument/accelerate/scratch_program.cpp

@@ -70,7 +70,7 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
   std::cout << "Finished symex, invoking decision procedure.\n";
 #endif
 
-  return (checker->dec_solve()==decision_proceduret::resultt::D_SATISFIABLE);
+  return ((*checker)() == decision_proceduret::resultt::D_SATISFIABLE);
 }
 
 exprt scratch_programt::eval(const exprt &e)

src/solvers/prop/cover_goals.cpp

@@ -88,7 +88,7 @@ operator()(message_handlert &message_handler)
     _iterations++;
 
     constraint();
-    dec_result=prop_conv.dec_solve();
+    dec_result = prop_conv();
 
     switch(dec_result)
     {

src/solvers/prop/decision_procedure.h

@@ -56,9 +56,6 @@ class decision_proceduret
   // solve the problem
   enum class resultt { D_SATISFIABLE, D_UNSATISFIABLE, D_ERROR };
 
-  // will eventually be protected, use below call operator
-  virtual resultt dec_solve()=0;
-
   resultt operator()()
   {
     return dec_solve();
@@ -69,6 +66,9 @@ class decision_proceduret
 
   /// Returns the number of incremental solver calls
   virtual std::size_t get_number_of_solver_calls() const = 0;
+
+protected:
+  virtual resultt dec_solve() = 0;
 };
 
 inline decision_proceduret &operator<<(

src/solvers/prop/minimize.cpp

@@ -123,7 +123,7 @@ void prop_minimizet::operator()()
         bvt assumptions;
         assumptions.push_back(c);
         prop_conv.set_assumptions(assumptions);
-        dec_result=prop_conv.dec_solve();
+        dec_result = prop_conv();
 
         switch(dec_result)
         {
@@ -153,6 +153,6 @@ void prop_minimizet::operator()()
 
     bvt assumptions; // no assumptions
     prop_conv.set_assumptions(assumptions);
-    prop_conv.dec_solve();
+    (void)prop_conv();
   }
 }