symmetry_breakingt Class Reference

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

#include <symex_symmetry.h>

Inheritance diagram for symmetry_breakingt:

Public Member Functions
	symmetry_breakingt ()
bool	run (symex_target_equationt::SSA_stepst &steps) override
	Executes the algorithm over a T object.
BigInt	ignored () const override
	How many steps were ignored after this algorithm.
Public Member Functions inherited from ssa_step_algorithm
	ssa_step_algorithm (bool sideffect)
void	run_on_step (symex_target_equationt::SSA_stept &)
virtual void	run_on_assignment (symex_target_equationt::SSA_stept &)
virtual void	run_on_assume (symex_target_equationt::SSA_stept &)
virtual void	run_on_assert (symex_target_equationt::SSA_stept &)
virtual void	run_on_output (symex_target_equationt::SSA_stept &)
virtual void	run_on_skip (symex_target_equationt::SSA_stept &)
virtual void	run_on_renumber (symex_target_equationt::SSA_stept &)
virtual void	run_on_branching (symex_target_equationt::SSA_stept &)
Public Member Functions inherited from algorithm< symex_target_equationt::SSA_stepst >
	algorithm (bool sideeffect)
virtual	~algorithm ()=default
bool	has_sideeffect ()
	Says wether the algorithm is a plain analysis or if it also changes the structure.

Additional Inherited Members
Protected Attributes inherited from algorithm< symex_target_equationt::SSA_stepst >
const bool	sideeffect

Detailed Description

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.

This hands the solver the fold bound directly instead of forcing it to case-split to re-derive it – the motivating case (discussion #5998 / Z3 #10125) is a running max/min folded over free values. For a chain of such ites, a direct leaf-to-final bound is also injected, so a property against the chain's final result doesn't force the solver to chain the per-step bounds transitively.

Each bound is a tautology implied by the ite's own definition, so it cannot change satisfiability, provided the comparison is over a total order – floatbv is excluded because NaN comparisons break it. Recognition is a bounded syntactic check with no solver queries. Running this as its own pass (alongside slicing) keeps the optimisation out of symex_target_equationt::convert, which stays pure formula creation.

Constructor & Destructor Documentation

symmetry_breakingt()

symmetry_breakingt::symmetry_breakingt ( )

inline

Member Function Documentation

ignored()

BigInt symmetry_breakingt::ignored ( ) const

inlineoverridevirtual

How many steps were ignored after this algorithm.

Implements ssa_step_algorithm.

run()

bool symmetry_breakingt::run ( symex_target_equationt::SSA_stepst & )

overridevirtual

Executes the algorithm over a T object.

Returns

success of the algorithm

Implements algorithm< symex_target_equationt::SSA_stepst >.

---

The documentation for this class was generated from the following files:

• src/goto-symex/equation/symex_symmetry.h
• src/goto-symex/equation/symex_symmetry.cpp