#include <goto-programs/goto_model.h>#include <goto-programs/goto_program.h>#include <goto-programs/loop_ids.h>#include <analyses/loop_analysis.h>#include <goto-instrument/loop_utils.h>
Include dependency graph for synthesizer_utils.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Typedefs | |
| typedef std::map< loop_idt, exprt > | invariant_mapt |
Functions | |
| goto_programt::targett | get_loop_end_from_loop_head_and_content_mutable (const goto_programt::targett &loop_head, const loop_templatet< goto_programt::targett > &loop) |
Find the goto instruction of loop that jumps to loop_head More... | |
| goto_programt::const_targett | get_loop_end_from_loop_head_and_content (const goto_programt::const_targett &loop_head, const loop_templatet< goto_programt::const_targett > &loop) |
| goto_programt::targett | get_loop_head_or_end (const unsigned int loop_number, goto_functiont &function, bool finding_head) |
Return loop head if finding_head is true, Otherwise return loop end. More... | |
| goto_programt::targett | get_loop_end (const unsigned int loop_number, goto_functiont &function) |
Find and return the last instruction of the natural loop with loop_number in function. More... | |
| goto_programt::targett | get_loop_head (const unsigned int loop_number, goto_functiont &function) |
Find and return the first instruction of the natural loop with loop_number in function. More... | |
| void | annotate_invariants (const invariant_mapt &invariant_map, goto_modelt &goto_model, messaget &log) |
Annotate the invariants in invariant_map to their corresponding loops. More... | |
Typedef Documentation
◆ invariant_mapt
| typedef std::map<loop_idt, exprt> invariant_mapt |
Definition at line 19 of file synthesizer_utils.h.
Function Documentation
◆ annotate_invariants()
| void annotate_invariants | ( | const invariant_mapt & | invariant_map, |
| goto_modelt & | goto_model, | ||
| messaget & | log | ||
| ) |
Annotate the invariants in invariant_map to their corresponding loops.
Corresponding loops are specified by keys of invariant_map
Definition at line 93 of file synthesizer_utils.cpp.
◆ get_loop_end()
| goto_programt::targett get_loop_end | ( | const unsigned int | loop_number, |
| goto_functiont & | function | ||
| ) |
Find and return the last instruction of the natural loop with loop_number in function.
loop_end -> loop_head
Definition at line 82 of file synthesizer_utils.cpp.
◆ get_loop_end_from_loop_head_and_content()
| goto_programt::const_targett get_loop_end_from_loop_head_and_content | ( | const goto_programt::const_targett & | loop_head, |
| const loop_templatet< goto_programt::const_targett > & | loop | ||
| ) |
Definition at line 11 of file synthesizer_utils.cpp.
◆ get_loop_end_from_loop_head_and_content_mutable()
| goto_programt::targett get_loop_end_from_loop_head_and_content_mutable | ( | const goto_programt::targett & | loop_head, |
| const loop_templatet< goto_programt::targett > & | loop | ||
| ) |
Find the goto instruction of loop that jumps to loop_head
Definition at line 33 of file synthesizer_utils.cpp.
◆ get_loop_head()
| goto_programt::targett get_loop_head | ( | const unsigned int | loop_number, |
| goto_functiont & | function | ||
| ) |
Find and return the first instruction of the natural loop with loop_number in function.
loop_end -> loop_head
Definition at line 88 of file synthesizer_utils.cpp.
◆ get_loop_head_or_end()
| goto_programt::targett get_loop_head_or_end | ( | const unsigned int | loop_number, |
| goto_functiont & | function, | ||
| bool | finding_head | ||
| ) |
Return loop head if finding_head is true, Otherwise return loop end.
Definition at line 55 of file synthesizer_utils.cpp.
