transition_system.h

Go to the documentation of this file.

#pragma once
 
#include <irep2/irep2.h>
#include <util/irep/location.h>
#include <util/symtab/namespace.h>
#include <iosfwd>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <utility>
#include <vector>

class transition_systemt
{
public:
  struct propertyt
  {
    expr2tc violated;
    std::string comment;
    locationt location;
  };
 
  // Prefix are the commands before the loop starts
  // defs -> assignments, assumes -> assumptions, bad -> assertions
  std::vector<expr2tc> prefix_defs, prefix_assumes;
  std::vector<propertyt> prefix_bad;
 
  // Inductive state at the beginning (init), before (pre) and after (post)
  // each loop. Only variables the properties depend on are kept.
  struct statet
  {
    std::string name;
    expr2tc init, pre, post;
  };
  std::vector<statet> states;

  std::vector<std::pair<expr2tc, std::string>> inputs;
 
  // Same as the prefix but for loop body
  std::vector<expr2tc> body_defs, body_assumes;

  std::vector<propertyt> bad;

  expr2tc back_guard;

  std::vector<expr2tc> invariants;
 
  using step_localt = std::unordered_set<expr2tc, irep2_hash>;

  void set_step_local(step_localt syms);
  const step_localt &get_step_local() const
  {
    return step_local;
  }

  expr2tc at_step(const expr2tc &e, unsigned step) const;
 
  void dump(std::ostream &out, const namespacet &ns) const;

  bool has_local(const expr2tc &e) const;
 
private:
  step_localt step_local;

  mutable std::unordered_map<const expr2t *, bool> has_local_memo;
};

class ts_step_renamert
{
public:
  ts_step_renamert(const transition_systemt &ts, unsigned step);
  expr2tc operator()(const expr2tc &e);
 
private:
  const transition_systemt &ts;
  const std::string suffix;
  std::unordered_map<const expr2t *, expr2tc> memo;
};

void collect_symbols(
  const expr2tc &e,
  std::unordered_set<expr2tc, irep2_hash> &out,
  std::unordered_set<const expr2t *> &seen);