counterexample_beautificationt Class Reference

#include <counterexample_beautification.h>

Collaboration diagram for counterexample_beautificationt:

Public Member Functions
	counterexample_beautificationt (message_handlert &message_handler)
virtual	~counterexample_beautificationt ()=default
void	operator() (boolbvt &boolbv, const symex_target_equationt &equation)

Protected Member Functions
void	get_minimization_list (prop_convt &prop_conv, const symex_target_equationt &equation, minimization_listt &minimization_list)
void	minimize (const exprt &expr, class prop_minimizet &prop_minimize)
symex_target_equationt::SSA_stepst::const_iterator	get_failed_property (const prop_convt &prop_conv, const symex_target_equationt &equation)

Protected Attributes
symex_target_equationt::SSA_stepst::const_iterator	failed
messaget	log

Detailed Description

Definition at line 19 of file counterexample_beautification.h.

Constructor & Destructor Documentation

counterexample_beautificationt()

counterexample_beautificationt::counterexample_beautificationt ( message_handlert &  message_handler )

explicit

Definition at line 18 of file counterexample_beautification.cpp.

~counterexample_beautificationt()

virtual counterexample_beautificationt::~counterexample_beautificationt ( )

virtualdefault

Member Function Documentation

get_failed_property()

symex_target_equationt::SSA_stepst::const_iterator counterexample_beautificationt::get_failed_property ( const prop_convt &  prop_conv, const symex_target_equationt &  equation  )

protected

Definition at line 67 of file counterexample_beautification.cpp.

get_minimization_list()

void counterexample_beautificationt::get_minimization_list ( prop_convt &  prop_conv, const symex_target_equationt &  equation, minimization_listt &  minimization_list  )

protected

Definition at line 24 of file counterexample_beautification.cpp.

minimize()

void counterexample_beautificationt::minimize ( const exprt &  expr, class prop_minimizet &  prop_minimize  )

protected

operator()()

void counterexample_beautificationt::operator()	(	boolbvt &	boolbv,
		const symex_target_equationt &	equation
	)

Definition at line 90 of file counterexample_beautification.cpp.

Member Data Documentation

failed

symex_target_equationt::SSA_stepst::const_iterator counterexample_beautificationt::failed

protected

Definition at line 40 of file counterexample_beautification.h.

log

messaget counterexample_beautificationt::log

protected

Definition at line 42 of file counterexample_beautification.h.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-checker/counterexample_beautification.h
• /home/runner/work/cbmc/cbmc/src/goto-checker/counterexample_beautification.cpp