synthesizer_utils.h File Reference

#include <goto-instrument/contracts/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.

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.