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 
19 #include <solvers/sat/satcheck.h>
20 
23 {
25  // at this point all indices should in the index set
26 
27  // just build the data structure
28  update_index_map(true);
29 
30  // we don't actually add any constraints
34 }
35 
38 {
40  return;
41 
42  unsigned nb_active=0;
43 
44  std::list<lazy_constraintt>::iterator it=lazy_array_constraints.begin();
45  while(it!=lazy_array_constraints.end())
46  {
47  satcheck_no_simplifiert sat_check;
48  bv_pointerst solver(ns, sat_check);
50 
51  exprt current=(*it).lazy;
52 
53  // some minor simplifications
54  // check if they are worth having
55  if(current.id()==ID_implies)
56  {
57  implies_exprt imp=to_implies_expr(current);
59  imp.operands().size()==2,
60  string_refinement_invariantt("implies must have two operands"));
61  exprt implies_simplified=get(imp.op0());
62  if(implies_simplified==false_exprt())
63  {
64  ++it;
65  continue;
66  }
67  }
68 
69  if(current.id()==ID_or)
70  {
71  or_exprt orexp=to_or_expr(current);
72  INVARIANT(
73  orexp.operands().size()==2,
74  string_refinement_invariantt("only treats the case of a binary or"));
75  exprt o1=get(orexp.op0());
76  exprt o2=get(orexp.op1());
77  if(o1==true_exprt() || o2 == true_exprt())
78  {
79  ++it;
80  continue;
81  }
82  }
83 
84  exprt simplified=get(current);
85  solver << simplified;
86 
87  switch(static_cast<decision_proceduret::resultt>(sat_check.prop_solve()))
88  {
90  ++it;
91  break;
93  prop.l_set_to_true(convert(current));
94  nb_active++;
95  lazy_array_constraints.erase(it++);
96  break;
97  default:
98  INVARIANT(
99  false,
100  string_refinement_invariantt("error in array over approximation "
101  "check"));
102  }
103  }
104 
105  debug() << "BV-Refinement: " << nb_active
106  << " array expressions become active" << eom;
107  debug() << "BV-Refinement: " << lazy_array_constraints.size()
108  << " inactive array expressions" << eom;
109  if(nb_active > 0)
110  progress=true;
111 }
112 
113 
116 {
117  if(!lazy_arrays)
118  return;
119 
120  for(const auto &constraint : lazy_array_constraints)
121  {
122  std::set<symbol_exprt> symbols;
123  find_symbols(constraint.lazy, symbols);
124  for(const auto &symbol : symbols)
125  {
126  const bvt bv=convert_bv(symbol);
127  forall_literals(b_it, bv)
128  if(!b_it->is_constant())
129  prop.set_frozen(*b_it);
130  }
131  }
132 }
bool lazy_arrays
Definition: arrays.h:95
void freeze_lazy_constraints()
freeze symbols for incremental solving
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
Boolean OR.
Definition: std_expr.h:2531
exprt & op0()
Definition: expr.h:84
void add_array_constraints()
Definition: arrays.cpp:260
mstreamt & progress() const
Definition: message.h:411
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2577
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
#define forall_literals(it, bv)
Definition: literal.h:202
Boolean implication.
Definition: std_expr.h:2485
void post_process_arrays() override
generate array constraints
void l_set_to_true(literalt a)
Definition: prop.h:49
symbolst symbols
Definition: prop_conv.h:142
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2505
const irep_idt & id() const
Definition: irep.h:259
The Boolean constant true.
Definition: std_expr.h:4443
bool refine_arrays
Enable array refinement.
Definition: bv_refinement.h:28
int solver(std::istream &in)
void update_index_map(bool update_all)
Definition: arrays.cpp:376
API to expression classes.
exprt & op1()
Definition: expr.h:87
void collect_indices()
Definition: arrays.cpp:74
virtual void set_frozen(literalt)
Definition: prop.h:111
const namespacet & ns
The Boolean constant false.
Definition: std_expr.h:4452
void arrays_overapproximated()
check whether counterexample is spurious
static eomt eom
Definition: message.h:284
Base class for all expressions.
Definition: expr.h:54
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:97
#define string_refinement_invariantt(reason)
Abstraction Refinement Loop.
mstreamt & debug() const
Definition: message.h:416
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
void find_symbols(const exprt &src, find_symbols_sett &dest)
std::vector< literalt > bvt
Definition: literal.h:200