enumerative_loop_contracts_synthesizer.cpp File Reference
Enumerative Loop Contracts Synthesizer. More...
#include "enumerative_loop_contracts_synthesizer.h"#include <util/arith_tools.h>#include <util/c_types.h>#include <util/find_symbols.h>#include <util/format_expr.h>#include <util/pointer_predicates.h>#include <util/replace_symbol.h>#include <util/simplify_expr.h>#include <analyses/local_may_alias.h>#include <analyses/natural_loops.h>#include <goto-instrument/contracts/cfg_info.h>#include <goto-instrument/contracts/utils.h>#include <goto-instrument/havoc_utils.h>#include <goto-instrument/loop_utils.h>#include "cegis_evaluator.h"#include "expr_enumerator.h"
Include dependency graph for enumerative_loop_contracts_synthesizer.cpp:Go to the source code of this file.
Functions | |
| void | replace_tmp_post (exprt &dest, const std::unordered_map< exprt, exprt, irep_hash > &tmp_post_map) |
| std::vector< exprt > | construct_terminals (const std::set< symbol_exprt > &symbols) |
Detailed Description
Enumerative Loop Contracts Synthesizer.
Definition in file enumerative_loop_contracts_synthesizer.cpp.
Function Documentation
◆ construct_terminals()
| std::vector<exprt> construct_terminals | ( | const std::set< symbol_exprt > & | symbols | ) |
Definition at line 50 of file enumerative_loop_contracts_synthesizer.cpp.
