symex_symmetry.h File Reference

#include <goto-symex/equation/symex_target_equation.h>
#include <goto-symex/equation/ssa_step_algorithm.h>

Include dependency graph for symex_symmetry.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	symmetry_breakingt
	SSA transformation pass that recognises lhs = ite(cond, t, e) max/min idioms in the equation and injects the redundant bounds they imply (t <= lhs && e <= lhs for a max, <= reversed for a min) as extra ASSUME steps. More...