incremental_goto_checker.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Incremental Goto Checker Interface
 
Author: Daniel Kroening, Peter Schrammel
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_CHECKER_INCREMENTAL_GOTO_CHECKER_H
#define CPROVER_GOTO_CHECKER_INCREMENTAL_GOTO_CHECKER_H
 
#include <unordered_set>
 
#include "properties.h"
 
#include <util/message.h>
 
class optionst;
class ui_message_handlert;

class incremental_goto_checkert
{
public:
  incremental_goto_checkert() = delete;
  incremental_goto_checkert(const incremental_goto_checkert &) = delete;
  virtual ~incremental_goto_checkert() = default;
 
  struct resultt
  {
    enum class progresst
    {
      FOUND_FAIL,
      DONE
    };
 
    progresst progress;
 
    resultt() = delete;
    explicit resultt(progresst);

    std::unordered_set<irep_idt> updated_properties;
  };

  virtual resultt operator()(propertiest &properties) = 0;

  virtual void report()
  {
  }
 
protected:
  incremental_goto_checkert(const optionst &, ui_message_handlert &);
 
  const optionst &options;
  ui_message_handlert &ui_message_handler;
  messaget log;
};
 
#endif // CPROVER_GOTO_CHECKER_INCREMENTAL_GOTO_CHECKER_H