Move trace returning into separate interface

Not all incremental goto checker implementations
may support traces.

Author: peterschrammel

src/goto-checker/goto_trace_provider.h

@@ -0,0 +1,30 @@
+/*******************************************************************\
+
+Module: Interface for returning Goto Traces from Goto Checkers
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Interface for returning Goto Traces from Goto Checkers
+
+#ifndef CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H
+#define CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H
+
+class goto_tracet;
+class namespacet;
+
+/// An implementation of `incremental_goto_checkert`
+/// may implement this interface to provide goto traces.
+class goto_trace_providert
+{
+public:
+  /// Builds and returns a trace
+  virtual goto_tracet build_trace() const = 0;
+
+  /// Returns the namespace associated with the traces
+  virtual const namespacet &get_namespace() const = 0;
+};
+
+#endif // CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H

src/goto-checker/incremental_goto_checker.h

@@ -64,11 +64,6 @@ class incremental_goto_checkert
   /// failing properties any more.
   virtual resultt operator()(propertiest &properties) = 0;
 
-  /// Builds and returns the counterexample
-  virtual goto_tracet build_error_trace() const = 0;
-
-  virtual const namespacet &get_namespace() const = 0;
-
 protected:
   incremental_goto_checkert(const optionst &, ui_message_handlert &);