cprover
refine_arrays.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "bv_refinement.h"
10 
11 #ifdef DEBUG
12 #include <iostream>
13 #endif
14 
15 #include <util/std_expr.h>
16 #include <util/find_symbols.h>
17 
18 #include <solvers/sat/satcheck.h>
19 
22 {
24  // at this point all indices should in the index set
25 
26  // just build the data structure
27  update_index_map(true);
28 
29  // we don't actually add any constraints
33 }
34 
37 {
39  return;
40 
41  unsigned nb_active=0;
42 
43  std::list<lazy_constraintt>::iterator it=lazy_array_constraints.begin();
44  while(it!=lazy_array_constraints.end())
45  {
46  satcheck_no_simplifiert sat_check{log.get_message_handler()};
49 
50  exprt current=(*it).lazy;
51 
52  // some minor simplifications
53  // check if they are worth having
54  if(current.id()==ID_implies)
55  {
56  implies_exprt imp=to_implies_expr(current);
57  exprt implies_simplified=get(imp.op0());
58  if(implies_simplified==false_exprt())
59  {
60  ++it;
61  continue;
62  }
63  }
64 
65  if(current.id()==ID_or)
66  {
67  or_exprt orexp=to_or_expr(current);
68  INVARIANT(
69  orexp.operands().size() == 2, "only treats the case of a binary or");
70  exprt o1=get(orexp.op0());
71  exprt o2=get(orexp.op1());
72  if(o1==true_exprt() || o2 == true_exprt())
73  {
74  ++it;
75  continue;
76  }
77  }
78 
79  exprt simplified=get(current);
80  solver << simplified;
81 
82  switch(static_cast<decision_proceduret::resultt>(sat_check.prop_solve()))
83  {
85  ++it;
86  break;
88  prop.l_set_to_true(convert(current));
89  nb_active++;
90  lazy_array_constraints.erase(it++);
91  break;
93  INVARIANT(false, "error in array over approximation check");
94  }
95  }
96 
97  log.debug() << "BV-Refinement: " << nb_active
98  << " array expressions become active" << messaget::eom;
99  log.debug() << "BV-Refinement: " << lazy_array_constraints.size()
100  << " inactive array expressions" << messaget::eom;
101  if(nb_active > 0)
102  progress=true;
103 }
104 
105 
108 {
109  if(!lazy_arrays)
110  return;
111 
112  for(const auto &constraint : lazy_array_constraints)
113  {
114  for(const auto &symbol : find_symbols(constraint.lazy))
115  {
116  const bvt bv=convert_bv(symbol);
117  for(const auto &literal : bv)
118  if(!literal.is_constant())
119  prop.set_frozen(literal);
120  }
121  }
122 }
Abstraction Refinement Loop.
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:112
const namespacet & ns
Definition: arrays.h:54
bool lazy_arrays
Definition: arrays.h:109
void collect_indices()
Definition: arrays.cpp:80
void add_array_constraints()
Definition: arrays.cpp:273
void update_index_map(bool update_all)
Definition: arrays.cpp:399
messaget log
Definition: arrays.h:55
exprt & op0()
Definition: expr.h:99
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:40
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: boolbv_get.cpp:19
void post_process_arrays() override
generate array constraints
void freeze_lazy_constraints()
freeze symbols for incremental solving
void arrays_overapproximated()
check whether counterexample is spurious
resultt
Result of running the decision procedure.
Base class for all expressions.
Definition: expr.h:54
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2811
Boolean implication.
Definition: std_expr.h:1983
const irep_idt & id() const
Definition: irep.h:407
mstreamt & debug() const
Definition: message.h:429
message_handlert & get_message_handler()
Definition: message.h:184
static eomt eom
Definition: message.h:297
exprt & op1()
Definition: std_expr.h:850
exprt & op0()
Definition: std_expr.h:844
Boolean OR.
Definition: std_expr.h:2028
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
void l_set_to_true(literalt a)
Definition: prop.h:50
virtual void set_frozen(literalt)
Definition: prop.h:112
The Boolean constant true.
Definition: std_expr.h:2802
void find_symbols(const exprt &src, find_symbols_sett &dest, bool current, bool next)
Add to the set dest the sub-expressions of src with id ID_symbol if current is true,...
std::vector< literalt > bvt
Definition: literal.h:201
int solver(std::istream &in)
API to expression classes.
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2075
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2008
bool refine_arrays
Enable array refinement.
Definition: bv_refinement.h:28