CBMC
synthesizer_utils.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Utility functions for loop invariant synthesizer.
4 
5 Author: 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 
16 invariant_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
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:31