Cleanup symex_target_equationt API

Remove methods that were never used (and one that wasn't even
implemented), mark `protected` what doesn't need to be part of the
public API, and remove an unnecessary case of a default parameter.

Author: tautschnig

src/goto-symex/symex_target_equation.cpp

@@ -349,7 +349,7 @@ void symex_target_equationt::convert(decision_proceduret &decision_procedure)
   const auto convert_SSA_start = std::chrono::steady_clock::now();
 
   convert_without_assertions(decision_procedure);
-  convert_assertions(decision_procedure);
+  convert_assertions(decision_procedure, true);
 
   const auto convert_SSA_stop = std::chrono::steady_clock::now();
   std::chrono::duration<double> convert_SSA_runtime =

src/goto-symex/symex_target_equation.h

@@ -12,18 +12,17 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
 #define CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
 
-#include <algorithm>
-#include <iosfwd>
-#include <list>
-
-#include <util/invariant.h>
 #include <util/merge_irep.h>
 #include <util/message.h>
 #include <util/narrow.h>
 
 #include "ssa_step.h"
 #include "symex_target.h"
 
+#include <algorithm>
+#include <iosfwd>
+#include <list>
+
 class decision_proceduret;
 class namespacet;
 
@@ -183,53 +182,16 @@ class symex_target_equationt:public symex_targett
   ///   interface
   void convert_without_assertions(decision_proceduret &decision_procedure);
 
-  /// Converts assignments: set the equality _lhs==rhs_ to _True_.
-  /// \param decision_procedure: A handle to a decision procedure
-  ///  interface
-  void convert_assignments(decision_proceduret &decision_procedure);
-
-  /// Converts declarations: these are effectively ignored by the decision
-  /// procedure.
-  /// \param decision_procedure: A handle to a decision procedure
-  ///  interface
-  void convert_decls(decision_proceduret &decision_procedure);
-
-  /// Converts assumptions: convert the expression the assumption represents.
-  /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_assumptions(decision_proceduret &decision_procedure);
-
   /// Converts assertions: build a disjunction of negated assertions.
   /// \param decision_procedure: A handle to a decision procedure interface
   /// \param optimized_for_single_assertions: Use an optimized encoding for
   ///   single assertions (unsound for incremental conversions)
   void convert_assertions(
     decision_proceduret &decision_procedure,
-    bool optimized_for_single_assertions = true);
-
-  /// Converts constraints: set the represented condition to _True_.
-  /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_constraints(decision_proceduret &decision_procedure);
-
-  /// Converts goto instructions: convert the expression representing the
-  /// condition of this goto.
-  /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_goto_instructions(decision_proceduret &decision_procedure);
-
-  /// Converts guards: convert the expression the guard represents.
-  /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_guards(decision_proceduret &decision_procedure);
+    bool optimized_for_single_assertions);
 
-  /// Converts function calls: for each argument build an equality between its
-  /// symbol and the argument itself.
-  /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_function_calls(decision_proceduret &decision_procedure);
-
-  /// Converts I/O: for each argument build an equality between its
-  /// symbol and the argument itself.
-  /// \param decision_procedure: A handle to a decision procedure interface
-  void convert_io(decision_proceduret &decision_procedure);
-
-  exprt make_expression() const;
+  typedef std::list<SSA_stept> SSA_stepst;
+  SSA_stepst SSA_steps;
 
   std::size_t count_assertions() const
   {
@@ -247,27 +209,8 @@ class symex_target_equationt:public symex_targett
       }));
   }
 
-  typedef std::list<SSA_stept> SSA_stepst;
-  SSA_stepst SSA_steps;
-
-  SSA_stepst::iterator get_SSA_step(std::size_t s)
-  {
-    SSA_stepst::iterator it=SSA_steps.begin();
-    for(; s!=0; s--)
-    {
-      PRECONDITION(it != SSA_steps.end());
-      it++;
-    }
-    return it;
-  }
-
   void output(std::ostream &out) const;
 
-  void clear()
-  {
-    SSA_steps.clear();
-  }
-
   bool has_threads() const
   {
     return std::any_of(
@@ -283,6 +226,44 @@ class symex_target_equationt:public symex_targett
   }
 
 protected:
+  /// Converts assignments: set the equality _lhs==rhs_ to _True_.
+  /// \param decision_procedure: A handle to a decision procedure
+  ///  interface
+  void convert_assignments(decision_proceduret &decision_procedure);
+
+  /// Converts declarations: these are effectively ignored by the decision
+  /// procedure.
+  /// \param decision_procedure: A handle to a decision procedure
+  ///  interface
+  void convert_decls(decision_proceduret &decision_procedure);
+
+  /// Converts assumptions: convert the expression the assumption represents.
+  /// \param decision_procedure: A handle to a decision procedure interface
+  void convert_assumptions(decision_proceduret &decision_procedure);
+
+  /// Converts constraints: set the represented condition to _True_.
+  /// \param decision_procedure: A handle to a decision procedure interface
+  void convert_constraints(decision_proceduret &decision_procedure);
+
+  /// Converts goto instructions: convert the expression representing the
+  /// condition of this goto.
+  /// \param decision_procedure: A handle to a decision procedure interface
+  void convert_goto_instructions(decision_proceduret &decision_procedure);
+
+  /// Converts guards: convert the expression the guard represents.
+  /// \param decision_procedure: A handle to a decision procedure interface
+  void convert_guards(decision_proceduret &decision_procedure);
+
+  /// Converts function calls: for each argument build an equality between its
+  /// symbol and the argument itself.
+  /// \param decision_procedure: A handle to a decision procedure interface
+  void convert_function_calls(decision_proceduret &decision_procedure);
+
+  /// Converts I/O: for each argument build an equality between its
+  /// symbol and the argument itself.
+  /// \param decision_procedure: A handle to a decision procedure interface
+  void convert_io(decision_proceduret &decision_procedure);
+
   messaget log;
 
   // for enforcing sharing in the expressions stored