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_CBMC_COUNTEREXAMPLE_BEAUTIFICATION_H
13 #define CPROVER_CBMC_COUNTEREXAMPLE_BEAUTIFICATION_H
14 
15 #include <util/namespace.h>
16 
18 
20 
21 #include "bv_cbmc.h"
22 
24 {
25 public:
27  {
28  }
29 
30  void operator()(
31  bv_cbmct &bv_cbmc,
32  const symex_target_equationt &equation,
33  const namespacet &ns);
34 
35 protected:
37  prop_convt &prop_conv,
38  const symex_target_equationt &equation,
39  minimization_listt &minimization_list);
40 
41  void minimize(
42  const exprt &expr,
43  class prop_minimizet &prop_minimize);
44 
45  symex_target_equationt::SSA_stepst::const_iterator get_failed_property(
46  const prop_convt &prop_conv,
47  const symex_target_equationt &equation);
48 
49  // the failed property
50  symex_target_equationt::SSA_stepst::const_iterator failed;
51 };
52 
53 #endif // CPROVER_CBMC_COUNTEREXAMPLE_BEAUTIFICATION_H
Generate Equation using Symbolic Execution.
void minimize(const exprt &expr, class prop_minimizet &prop_minimize)
symex_target_equationt::SSA_stepst::const_iterator failed
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT...
Definition: minimize.h:23
SAT-optimizer for minimizing expressions.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::set< exprt > minimization_listt
Definition: bv_minimize.h:23
symex_target_equationt::SSA_stepst::const_iterator get_failed_property(const prop_convt &prop_conv, const symex_target_equationt &equation)
Base class for all expressions.
Definition: expr.h:42
void operator()(bv_cbmct &bv_cbmc, const symex_target_equationt &equation, const namespacet &ns)
void get_minimization_list(prop_convt &prop_conv, const symex_target_equationt &equation, minimization_listt &minimization_list)