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 <langapi/language_ui.h>
16 
18 
19 #define MAX_STATE 10000
20 
22 {
23 public:
24  bv_refinementt(const namespacet &_ns, propt &_prop);
26 
28 
29  virtual std::string decision_procedure_text() const
30  {
31  return "refinement loop with "+prop.solver_text();
32  }
33 
34  // NOLINTNEXTLINE(readability/identifiers)
35  typedef bv_pointerst SUB;
36 
37  // maximal number of times we refine a formula node
39  // enable/disable refinements
42 
44 
45  void set_ui(language_uit::uit _ui) { ui=_ui; }
46 
47 protected:
49 
50  // the list of operator approximations
52  {
53  public:
54  explicit approximationt(std::size_t _id_nr):id_nr(_id_nr)
55  {
56  }
57 
59  std::size_t no_operands;
60 
63 
66 
67  // the kind of under- or over-approximation
69 
70  approximationt():under_state(0), over_state(0)
71  {
72  }
73 
74  std::string as_string() const;
75 
78 
79  std::size_t id_nr;
80  };
81 
82  typedef std::list<approximationt> approximationst;
83  approximationst approximations;
84 
86  void check_SAT(approximationt &approximation);
87  void check_UNSAT(approximationt &approximation);
88  void initialize(approximationt &approximation);
89  void get_values(approximationt &approximation);
90  bool is_in_conflict(approximationt &approximation);
91 
92  virtual void check_SAT();
93  virtual void check_UNSAT();
94  bool progress;
95 
96  // we refine the theory of arrays
97  virtual void post_process_arrays();
100 
101  // we refine expensive arithmetic
102  virtual bvt convert_mult(const exprt &expr);
103  virtual bvt convert_div(const div_exprt &expr);
104  virtual bvt convert_mod(const mod_exprt &expr);
105  virtual bvt convert_floatbv_op(const exprt &expr);
106 
107  // for collecting statistics
108  virtual void set_to(const exprt &expr, bool value);
109 
110  // overloading
111  virtual void set_assumptions(const bvt &_assumptions);
112 
114 
115  // use gui format
117 };
118 
119 #endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
virtual decision_proceduret::resultt dec_solve()
approximationt & add_approximation(const exprt &expr, bvt &bv)
BigInt mp_integer
Definition: mp_arith.h:19
void freeze_lazy_constraints()
freeze symbols for incremental solving
virtual std::string decision_procedure_text() const
Definition: bv_refinement.h:29
bool is_in_conflict(approximationt &approximation)
check if an under-approximation is part of the conflict
virtual const std::string solver_text()=0
virtual void set_assumptions(const bvt &_assumptions)
virtual void set_to(const exprt &expr, bool value)
approximationst approximations
Definition: bv_refinement.h:83
bv_pointerst SUB
Definition: bv_refinement.h:35
virtual void post_process_arrays()
generate array constraints
void initialize(approximationt &approximation)
void set_ui(language_uit::uit _ui)
Definition: bv_refinement.h:45
std::list< approximationt > approximationst
Definition: bv_refinement.h:82
virtual bvt convert_floatbv_op(const exprt &expr)
division (integer and real)
Definition: std_expr.h:854
bool do_arithmetic_refinement
Definition: bv_refinement.h:41
TO_BE_DOCUMENTED.
Definition: namespace.h:62
language_uit::uit ui
virtual bvt convert_mult(const exprt &expr)
approximationt(std::size_t _id_nr)
Definition: bv_refinement.h:54
bv_refinementt(const namespacet &_ns, propt &_prop)
TO_BE_DOCUMENTED.
Definition: prop.h:22
virtual bvt convert_mod(const mod_exprt &expr)
void arrays_overapproximated()
check whether counterexample is spurious
unsigned max_node_refinement
Definition: bv_refinement.h:38
void get_values(approximationt &approximation)
bool do_array_refinement
Definition: bv_refinement.h:40
virtual void check_SAT()
virtual bool is_in_conflict(literalt l) const override
determine whether a variable is in the final conflict
Definition: prop_conv.h:98
Base class for all expressions.
Definition: expr.h:46
virtual bvt convert_div(const div_exprt &expr)
virtual void check_UNSAT()
std::vector< literalt > bvt
Definition: literal.h:197
binary modulo
Definition: std_expr.h:902