cprover
counterexample_beautificationt Class Reference

#include <counterexample_beautification.h>

+ Collaboration diagram for counterexample_beautificationt:

Public Member Functions

virtual ~counterexample_beautificationt ()
 
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
 

Detailed Description

Definition at line 21 of file counterexample_beautification.h.

Constructor & Destructor Documentation

◆ ~counterexample_beautificationt()

virtual counterexample_beautificationt::~counterexample_beautificationt ( )
inlinevirtual

Definition at line 24 of file counterexample_beautification.h.

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 63 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 22 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 82 of file counterexample_beautification.cpp.

Member Data Documentation

◆ failed

symex_target_equationt::SSA_stepst::const_iterator counterexample_beautificationt::failed
protected

Definition at line 46 of file counterexample_beautification.h.


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