Break down steps of multi-path symex goto checker

Enables better code reuse in derived classes.

src/goto-checker/multi_path_symex_checker.cpp

@@ -56,21 +56,37 @@ operator()(propertiest &properties)
     if(!has_properties_to_check(properties))
       return result;
 
-    solver_runtime += prepare_property_decider(
-      properties, equation, property_decider, ui_message_handler);
-
-    if(options.get_bool_option("localize-faults"))
-      freeze_guards(equation, property_decider.get_solver());
+    solver_runtime += prepare_property_decider(properties);
 
     equation_generated = true;
   }
 
-  run_property_decider(
-    result, properties, property_decider, ui_message_handler, solver_runtime);
+  run_property_decider(result, properties, solver_runtime);
 
   return result;
 }
 
+std::chrono::duration<double>
+multi_path_symex_checkert::prepare_property_decider(propertiest &properties)
+{
+  std::chrono::duration<double> solver_runtime = ::prepare_property_decider(
+    properties, equation, property_decider, ui_message_handler);
+
+  if(options.get_bool_option("localize-faults"))
+    freeze_guards(equation, property_decider.get_solver());
+
+  return solver_runtime;
+}
+
+void multi_path_symex_checkert::run_property_decider(
+  incremental_goto_checkert::resultt &result,
+  propertiest &properties,
+  std::chrono::duration<double> solver_runtime)
+{
+  ::run_property_decider(
+    result, properties, property_decider, ui_message_handler, solver_runtime);
+}
+
 goto_tracet multi_path_symex_checkert::build_full_trace() const
 {
   goto_tracet goto_trace;

src/goto-checker/multi_path_symex_checker.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H
 #define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H
 
+#include <chrono>
+
 #include "fault_localization_provider.h"
 #include "goto_symex_property_decider.h"
 #include "goto_trace_provider.h"
@@ -55,6 +57,23 @@ public:
 protected:
   bool equation_generated;
   goto_symex_property_decidert property_decider;
+
+  /// Prepare the property decider for solving. This sets up the data structures
+  /// for tracking goal literals, sets the status of \p properties to be checked
+  /// to UNKNOWN and pushes the equation into the solver.
+  /// \return the time taken (pushing into the solver is a costly operation)
+  virtual std::chrono::duration<double>
+  prepare_property_decider(propertiest &properties);
+
+  /// Run the property decider, which calls the SAT solver, and set the status
+  /// of checked \p properties accordingly. The property IDs of updated
+  /// properties are added to the `result.updated_properties` and the goto
+  /// checker's progress (DONE, FOUND_FAIL) is set in \p result.
+  /// The \p solver_runtime will be logged.
+  virtual void run_property_decider(
+    incremental_goto_checkert::resultt &result,
+    propertiest &properties,
+    std::chrono::duration<double> solver_runtime);
 };
 
 #endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H