CBMC
synthesizer_utils.cpp File Reference
+ Include dependency graph for synthesizer_utils.cpp:

Go to the source code of this file.

Functions

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) More...
 

Function Documentation

◆ 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 at line 11 of file synthesizer_utils.cpp.