CBMC
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
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: