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
bv_refinementt::convert_div
bvt convert_div(const div_exprt &expr) override
Definition: refine_arithmetic.cpp:101
bv_refinementt::configt::max_node_refinement
unsigned max_node_refinement
Max number of times we refine a formula node.
Definition: bv_refinement.h:26
bv_refinementt::configt::output_xml
bool output_xml
Definition: bv_refinement.h:24
bv_refinementt::conflicts_with
bool conflicts_with(approximationt &approximation)
check if an under-approximation is part of the conflict
Definition: refine_arithmetic.cpp:459
propt::solver_text
virtual const std::string solver_text()=0
bv_refinementt::approximationt::expr
exprt expr
Definition: bv_refinement.h:74
bvt
std::vector< literalt > bvt
Definition: literal.h:200
bv_refinementt::arrays_overapproximated
void arrays_overapproximated()
check whether counterexample is spurious
Definition: refine_arrays.cpp:37
bv_refinementt::add_approximation
approximationt & add_approximation(const exprt &expr, bvt &bv)
Definition: refine_arithmetic.cpp:484
bv_refinementt::infot
Definition: bv_refinement.h:33
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
bv_refinementt::check_SAT
void check_SAT()
Definition: bv_refinement_loop.cpp:113
bv_refinementt::configt::refine_arithmetic
bool refine_arithmetic
Enable arithmetic refinement.
Definition: bv_refinement.h:30
exprt
Base class for all expressions.
Definition: expr.h:54
bv_refinementt::decision_procedure_text
std::string decision_procedure_text() const override
Definition: bv_refinement.h:43
bv_refinementt::parent_assumptions
bvt parent_assumptions
Definition: bv_refinement.h:110
bv_refinementt::bv_refinementt
bv_refinementt(const infot &info)
Definition: bv_refinement_loop.cpp:13
bv_refinementt::approximationt::op1_bv
bvt op1_bv
Definition: bv_refinement.h:77
div_exprt
Division.
Definition: std_expr.h:1211
bv_refinementt::approximationt::under_assumptions
bvt under_assumptions
Definition: bv_refinement.h:80
bv_refinementt::approximationt::id_nr
std::size_t id_nr
Definition: bv_refinement.h:91
bv_refinementt::approximationt::approximationt
approximationt(std::size_t _id_nr)
Definition: bv_refinement.h:66
bv_pointers.h
bv_refinementt::convert_mult
bvt convert_mult(const mult_exprt &expr) override
Definition: refine_arithmetic.cpp:53
bv_refinementt::approximations
std::list< approximationt > approximations
Definition: bv_refinement.h:109
bv_refinementt::set_assumptions
void set_assumptions(const bvt &_assumptions) override
Definition: bv_refinement_loop.cpp:131
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
bv_refinementt::initialize
void initialize(approximationt &approximation)
Definition: refine_arithmetic.cpp:468
bv_refinementt::dec_solve
decision_proceduret::resultt dec_solve() override
Definition: bv_refinement_loop.cpp:24
bv_refinementt::approximationt::add_under_assumption
void add_under_assumption(literalt l)
Definition: refine_arithmetic.cpp:32
bv_refinementt::approximationt::add_over_assumption
void add_over_assumption(literalt l)
Definition: refine_arithmetic.cpp:25
bv_refinementt::approximationt
Definition: bv_refinement.h:63
bv_refinementt::approximationt::op2_value
mp_integer op2_value
Definition: bv_refinement.h:78
bv_refinementt::infot::prop
propt * prop
Definition: bv_refinement.h:36
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
bv_refinementt::approximationt::over_assumptions
bvt over_assumptions
Definition: bv_refinement.h:81
bv_pointerst
Definition: bv_pointers.h:17
bv_refinementt::check_UNSAT
void check_UNSAT()
Definition: bv_refinement_loop.cpp:123
bv_refinementt::approximationt::op0_value
mp_integer op0_value
Definition: bv_refinement.h:78
bv_refinementt::post_process_arrays
void post_process_arrays() override
generate array constraints
Definition: refine_arrays.cpp:22
bv_refinementt::convert_floatbv_op
bvt convert_floatbv_op(const exprt &expr) override
Definition: refine_arithmetic.cpp:39
bv_refinementt::approximationt::result_bv
bvt result_bv
Definition: bv_refinement.h:77
bv_refinementt::progress
bool progress
Definition: bv_refinement.h:108
bv_refinementt
Definition: bv_refinement.h:19
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
bv_refinementt::approximationt::over_state
unsigned over_state
Definition: bv_refinement.h:84
bv_refinementt::prop_solve
resultt prop_solve()
Definition: bv_refinement_loop.cpp:84
bv_refinementt::configt
Definition: bv_refinement.h:22
bv_refinementt::convert_mod
bvt convert_mod(const mod_exprt &expr) override
Definition: refine_arithmetic.cpp:119
bv_refinementt::config_
configt config_
Definition: bv_refinement.h:113
propt
TO_BE_DOCUMENTED.
Definition: prop.h:24
bv_refinementt::get_values
void get_values(approximationt &approximation)
Definition: refine_arithmetic.cpp:137
bv_refinementt::approximationt::op2_bv
bvt op2_bv
Definition: bv_refinement.h:77
bv_refinementt::freeze_lazy_constraints
void freeze_lazy_constraints()
freeze symbols for incremental solving
Definition: refine_arrays.cpp:115
literalt
Definition: literal.h:24
bv_refinementt::approximationt::under_state
unsigned under_state
Definition: bv_refinement.h:84
bv_refinementt::infot::ns
const namespacet * ns
Definition: bv_refinement.h:35
bv_refinementt::approximationt::op1_value
mp_integer op1_value
Definition: bv_refinement.h:78
bv_refinementt::approximationt::no_operands
std::size_t no_operands
Definition: bv_refinement.h:75
bv_refinementt::configt::refine_arrays
bool refine_arrays
Enable array refinement.
Definition: bv_refinement.h:28
bv_refinementt::approximationt::op0_bv
bvt op0_bv
Definition: bv_refinement.h:77
bv_refinementt::approximationt::result_value
mp_integer result_value
Definition: bv_refinement.h:78
mod_exprt
Modulo.
Definition: std_expr.h:1287
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152
bv_refinementt::approximationt::as_string
std::string as_string() const
Definition: refine_arithmetic.cpp:529