cprover
bv_refinement.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Abstraction Refinement Loop
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
13 #define CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
14 
15 #include <util/ui_message.h>
16 
18 
19 #define MAX_STATE 10000
20 
22 {
23 private:
24  struct configt
25  {
28  unsigned max_node_refinement=5;
30  bool refine_arrays=true;
32  bool refine_arithmetic=true;
33  };
34 public:
35  struct infot:public configt
36  {
37  const namespacet *ns=nullptr;
38  propt *prop=nullptr;
39  };
40 
41  explicit bv_refinementt(const infot &info);
42 
44 
45  std::string decision_procedure_text() const override
46  {
47  return "refinement loop with "+prop.solver_text();
48  }
49 
50 protected:
51 
52  // Refine array
53  void post_process_arrays() override;
54 
55  // Refine arithmetic
56  bvt convert_mult(const exprt &expr) override;
57  bvt convert_div(const div_exprt &expr) override;
58  bvt convert_mod(const mod_exprt &expr) override;
59  bvt convert_floatbv_op(const exprt &expr) override;
60 
61  void set_assumptions(const bvt &_assumptions) override;
62 
63 private:
64  // the list of operator approximations
65  struct approximationt final
66  {
67  public:
68  explicit approximationt(std::size_t _id_nr):
69  no_operands(0),
70  under_state(0),
71  over_state(0),
72  id_nr(_id_nr)
73  {
74  }
75 
77  std::size_t no_operands;
78 
81 
84 
85  // the kind of under- or over-approximation
87 
88  std::string as_string() const;
89 
92 
93  std::size_t id_nr;
94  };
95 
97  approximationt &add_approximation(const exprt &expr, bvt &bv);
98  bool conflicts_with(approximationt &approximation);
99  void check_SAT(approximationt &approximation);
100  void check_UNSAT(approximationt &approximation);
101  void initialize(approximationt &approximation);
102  void get_values(approximationt &approximation);
103  void check_SAT();
104  void check_UNSAT();
107 
108  // MEMBERS
109 
110  bool progress;
111  std::list<approximationt> approximations;
113 protected:
114  // use gui format
116 };
117 
118 #endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
const namespacet * ns
Definition: bv_refinement.h:37
approximationt & add_approximation(const exprt &expr, bvt &bv)
BigInt mp_integer
Definition: mp_arith.h:22
void freeze_lazy_constraints()
freeze symbols for incremental solving
void set_assumptions(const bvt &_assumptions) override
virtual const std::string solver_text()=0
std::list< approximationt > approximations
void initialize(approximationt &approximation)
void post_process_arrays() override
generate array constraints
bool conflicts_with(approximationt &approximation)
check if an under-approximation is part of the conflict
division (integer and real)
Definition: std_expr.h:1075
bool refine_arrays
Enable array refinement.
Definition: bv_refinement.h:30
unsigned max_node_refinement
Max number of times we refine a formula node.
Definition: bv_refinement.h:28
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::string decision_procedure_text() const override
Definition: bv_refinement.h:45
bvt convert_mod(const mod_exprt &expr) override
ui_message_handlert::uit ui
Definition: bv_refinement.h:26
approximationt(std::size_t _id_nr)
Definition: bv_refinement.h:68
decision_proceduret::resultt dec_solve() override
TO_BE_DOCUMENTED.
Definition: prop.h:24
void arrays_overapproximated()
check whether counterexample is spurious
bv_refinementt(const infot &info)
bvt convert_floatbv_op(const exprt &expr) override
bvt convert_mult(const exprt &expr) override
void get_values(approximationt &approximation)
Base class for all expressions.
Definition: expr.h:42
bool refine_arithmetic
Enable arithmetic refinement.
Definition: bv_refinement.h:32
bvt convert_div(const div_exprt &expr) override
std::vector< literalt > bvt
Definition: literal.h:200
binary modulo
Definition: std_expr.h:1133