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 
16 
17 #define MAX_STATE 10000
18 
20 {
21 private:
22  struct configt
23  {
24  bool output_xml = false;
26  unsigned max_node_refinement=5;
28  bool refine_arrays=true;
30  bool refine_arithmetic=true;
31  };
32 public:
33  struct infot:public configt
34  {
35  const namespacet *ns=nullptr;
36  propt *prop=nullptr;
37  };
38 
39  explicit bv_refinementt(const infot &info);
40 
42 
43  std::string decision_procedure_text() const override
44  {
45  return "refinement loop with "+prop.solver_text();
46  }
47 
48 protected:
49 
50  // Refine array
51  void post_process_arrays() override;
52 
53  // Refine arithmetic
54  bvt convert_mult(const mult_exprt &expr) override;
55  bvt convert_div(const div_exprt &expr) override;
56  bvt convert_mod(const mod_exprt &expr) override;
57  bvt convert_floatbv_op(const exprt &expr) override;
58 
59  void set_assumptions(const bvt &_assumptions) override;
60 
61 private:
62  // the list of operator approximations
63  struct approximationt final
64  {
65  public:
66  explicit approximationt(std::size_t _id_nr):
67  no_operands(0),
68  under_state(0),
69  over_state(0),
70  id_nr(_id_nr)
71  {
72  }
73 
75  std::size_t no_operands;
76 
79 
82 
83  // the kind of under- or over-approximation
85 
86  std::string as_string() const;
87 
90 
91  std::size_t id_nr;
92  };
93 
95  approximationt &add_approximation(const exprt &expr, bvt &bv);
96  bool conflicts_with(approximationt &approximation);
97  void check_SAT(approximationt &approximation);
98  void check_UNSAT(approximationt &approximation);
99  void initialize(approximationt &approximation);
100  void get_values(approximationt &approximation);
101  void check_SAT();
102  void check_UNSAT();
105 
106  // MEMBERS
107 
108  bool progress;
109  std::list<approximationt> approximations;
111 protected:
112  // use gui format
114 };
115 
116 #endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
const namespacet * ns
Definition: bv_refinement.h:35
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.
Definition: std_expr.h:1211
bool refine_arrays
Enable array refinement.
Definition: bv_refinement.h:28
bvt convert_mult(const mult_exprt &expr) override
unsigned max_node_refinement
Max number of times we refine a formula node.
Definition: bv_refinement.h:26
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
std::string decision_procedure_text() const override
Definition: bv_refinement.h:43
bvt convert_mod(const mod_exprt &expr) override
approximationt(std::size_t _id_nr)
Definition: bv_refinement.h:66
decision_proceduret::resultt dec_solve() override
TO_BE_DOCUMENTED.
Definition: prop.h:24
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
void arrays_overapproximated()
check whether counterexample is spurious
bv_refinementt(const infot &info)
bvt convert_floatbv_op(const exprt &expr) override
void get_values(approximationt &approximation)
Base class for all expressions.
Definition: expr.h:54
bool refine_arithmetic
Enable arithmetic refinement.
Definition: bv_refinement.h:30
bvt convert_div(const div_exprt &expr) override
std::vector< literalt > bvt
Definition: literal.h:200
Modulo.
Definition: std_expr.h:1287