cprover
Loading...
Searching...
No Matches
propagate.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Propagate
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_CPROVER_PROPAGATE_H
13#define CPROVER_CPROVER_PROPAGATE_H
14
15#include "solver_types.h"
16
17#include <unordered_set>
18
19void propagate(
20 const std::vector<framet> &,
21 const workt &,
22 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
23 bool verbose,
24 const namespacet &,
25 const std::function<void(const symbol_exprt &, exprt, const workt::patht &)>
26 &propagator);
27
28exprt simplify_state_expr(
29 exprt,
30 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
31 const namespacet &);
32
33exprt simplify_state_expr_node(
34 exprt,
35 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
36 const namespacet &);
37
38#endif // CPROVER_CPROVER_PROPAGATE_H
address_taken
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
Definition address_taken.cpp:51
exprt
Base class for all expressions.
Definition expr.h:57
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
symbol_exprt
Expression to hold a symbol (variable).
Definition std_expr.h:132
simplify_state_expr_node
exprt simplify_state_expr_node(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
Definition simplify_state_expr.cpp:961
propagate
void propagate(const std::vector< framet > &, const workt &, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, bool verbose, const namespacet &, const std::function< void(const symbol_exprt &, exprt, const workt::patht &)> &propagator)
Definition propagate.cpp:24
simplify_state_expr
exprt simplify_state_expr(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
Definition simplify_state_expr.cpp:1087
solver_types.h
Solver.
workt::patht
std::vector< frame_reft > patht
Definition solver_types.h:167