cache.h

Go to the documentation of this file.

#pragma once
 
#include <unordered_set>
 
#include <goto-symex/equation/ssa_step_algorithm.h>
#include <util/base/time_stopping.h>
#include <util/ssa/cache_defs.h>

class assertion_cache : public ssa_step_algorithm
{
public:
  assertion_cache(assert_db &db) : ssa_step_algorithm(true), db(db)
  {
  }
 
  bool run(symex_target_equationt::SSA_stepst &) override;
 
  void run_on_assert(symex_target_equationt::SSA_stept &) override;
  virtual BigInt ignored() const override
  {
    return hits;
  }
 
protected:
  assert_db &db;
 
private:
  BigInt hits = 0;
  BigInt total = 0;
};