counterexample_beautification.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Counterexample Beautification
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_CHECKER_COUNTEREXAMPLE_BEAUTIFICATION_H
#define CPROVER_GOTO_CHECKER_COUNTEREXAMPLE_BEAUTIFICATION_H
 
#include <goto-symex/symex_target_equation.h>
 
#include <solvers/flattening/bv_minimize.h>
 
class counterexample_beautificationt
{
public:
  explicit counterexample_beautificationt(message_handlert &message_handler);
  virtual ~counterexample_beautificationt() = default;
 
  void operator()(boolbvt &boolbv, const symex_target_equationt &equation);
 
protected:
  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);
 
  // the failed property
  symex_target_equationt::SSA_stepst::const_iterator failed;
 
  messaget log;
};
 
#endif // CPROVER_GOTO_CHECKER_COUNTEREXAMPLE_BEAUTIFICATION_H