CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
synthesizer_utils.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Utility functions for loop invariant synthesizer.
4
5Author: Qinheping Hu
6
7\*******************************************************************/
8
9#ifndef CPROVER_GOTO_SYNTHESIZER_SYNTHESIZER_UTILS_H
10#define CPROVER_GOTO_SYNTHESIZER_SYNTHESIZER_UTILS_H
11
12#include <goto-instrument/contracts/utils.h>
13
16invariant_mapt combine_in_and_post_invariant_clauses(
17 const invariant_mapt &in_clauses,
18 const invariant_mapt &post_clauses,
19 const invariant_mapt &neg_guards);
20
21#endif // CPROVER_GOTO_SYNTHESIZER_SYNTHESIZER_UTILS_H
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
combine_in_and_post_invariant_clauses
invariant_mapt combine_in_and_post_invariant_clauses(const invariant_mapt &in_clauses, const invariant_mapt &post_clauses, const invariant_mapt &neg_guards)
Combine invariant of form (in_inv || !guard) && (!guard -> pos_inv)
Definition synthesizer_utils.cpp:11
invariant_mapt
std::map< loop_idt, exprt > invariant_mapt
Definition utils.h:32