cprover
counterexample_beautification.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Counterexample Beautification
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_CHECKER_COUNTEREXAMPLE_BEAUTIFICATION_H
13 #define CPROVER_GOTO_CHECKER_COUNTEREXAMPLE_BEAUTIFICATION_H
14 
15 #include <util/namespace.h>
16 
18 
20 
22 {
23 public:
24  explicit counterexample_beautificationt(message_handlert &message_handler);
25  virtual ~counterexample_beautificationt() = default;
26 
27  void operator()(boolbvt &boolbv, const symex_target_equationt &equation);
28 
29 protected:
31  prop_convt &prop_conv,
32  const symex_target_equationt &equation,
33  minimization_listt &minimization_list);
34 
35  void minimize(const exprt &expr, class prop_minimizet &prop_minimize);
36 
37  symex_target_equationt::SSA_stepst::const_iterator get_failed_property(
38  const prop_convt &prop_conv,
39  const symex_target_equationt &equation);
40 
41  // the failed property
42  symex_target_equationt::SSA_stepst::const_iterator failed;
43 
45 };
46 
47 #endif // CPROVER_GOTO_CHECKER_COUNTEREXAMPLE_BEAUTIFICATION_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
counterexample_beautificationt::get_failed_property
symex_target_equationt::SSA_stepst::const_iterator get_failed_property(const prop_convt &prop_conv, const symex_target_equationt &equation)
Definition: counterexample_beautification.cpp:70
symex_target_equation.h
Generate Equation using Symbolic Execution.
minimization_listt
std::set< exprt > minimization_listt
Definition: bv_minimize.h:23
prop_minimizet
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT.
Definition: prop_minimize.h:25
prop_convt
Definition: prop_conv.h:22
counterexample_beautificationt
Definition: counterexample_beautification.h:22
counterexample_beautificationt::~counterexample_beautificationt
virtual ~counterexample_beautificationt()=default
exprt
Base class for all expressions.
Definition: expr.h:53
counterexample_beautificationt::counterexample_beautificationt
counterexample_beautificationt(message_handlert &message_handler)
Definition: counterexample_beautification.cpp:21
namespace.h
counterexample_beautificationt::minimize
void minimize(const exprt &expr, class prop_minimizet &prop_minimize)
counterexample_beautificationt::failed
symex_target_equationt::SSA_stepst::const_iterator failed
Definition: counterexample_beautification.h:42
counterexample_beautificationt::log
messaget log
Definition: counterexample_beautification.h:44
message_handlert
Definition: message.h:28
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
counterexample_beautificationt::get_minimization_list
void get_minimization_list(prop_convt &prop_conv, const symex_target_equationt &equation, minimization_listt &minimization_list)
Definition: counterexample_beautification.cpp:27
bv_minimize.h
SAT-optimizer for minimizing expressions.
counterexample_beautificationt::operator()
void operator()(boolbvt &boolbv, const symex_target_equationt &equation)
Definition: counterexample_beautification.cpp:94
boolbvt
Definition: boolbv.h:35