slice.h File Reference

#include <goto-symex/equation/symex_target_equation.h>
#include <util/base/time_stopping.h>
#include <goto-programs/property_verdict.h>
#include <goto-symex/equation/ssa_step_algorithm.h>
#include <util/config/options.h>
#include <boost/range/adaptor/reversed.hpp>
#include <langapi/language_util.h>

Include dependency graph for slice.h:

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

Go to the source code of this file.

Classes
class	slicer
class	simple_slice
	Naive slicer: slice every step after the last assertion. More...
class	claim_slicer
	Claim slicer: remove every other claim of the formula with the exception of the one to keep. More...
class	symex_slicet
	Class for the symex-slicer, this slicer is to be executed on SSA formula in order to remove every symbol that does not depends on it. More...