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  error() << "error in array over approximation check" << eom;
99  INVARIANT(
100  false,
101  string_refinement_invariantt("error in array over approximation "
102  "check"));
103  // Placeholder to tell the compiler we bail
104  throw 0;
105  }
106  }
107 
108  debug() << "BV-Refinement: " << nb_active
109  << " array expressions become active" << eom;
110  debug() << "BV-Refinement: " << lazy_array_constraints.size()
111  << " inactive array expressions" << eom;
112  if(nb_active > 0)
113  progress=true;
114 }
115 
116 
119 {
120  if(!lazy_arrays)
121  return;
122 
123  for(const auto &constraint : lazy_array_constraints)
124  {
125  std::set<symbol_exprt> symbols;
126  find_symbols(constraint.lazy, symbols);
127  for(const auto &symbol : symbols)
128  {
129  const bvt bv=convert_bv(symbol);
130  forall_literals(b_it, bv)
131  if(!b_it->is_constant())
132  prop.set_frozen(*b_it);
133  }
134  }
135 }
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:162
virtual void set_frozen(literalt a)
Definition: prop.h:111
boolean OR
Definition: std_expr.h:2391
exprt & op0()
Definition: expr.h:72
void add_array_constraints()
Definition: arrays.cpp:260
mstreamt & progress() const
Definition: message.h:327
const or_exprt & to_or_expr(const exprt &expr)
Cast a generic exprt to a or_exprt.
Definition: std_expr.h:2442
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
#define forall_literals(it, bv)
Definition: literal.h:202
boolean implication
Definition: std_expr.h:2339
void post_process_arrays() override
generate array constraints
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
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 a generic exprt to a implies_exprt.
Definition: std_expr.h:2362
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:4488
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
bool refine_arrays
Enable array refinement.
Definition: bv_refinement.h:30
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:75
mstreamt & error() const
Definition: message.h:302
void collect_indices()
Definition: arrays.cpp:74
const namespacet & ns
The boolean constant false.
Definition: std_expr.h:4499
void arrays_overapproximated()
check whether counterexample is spurious
Base class for all expressions.
Definition: expr.h:42
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:332
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
operandst & operands()
Definition: expr.h:66
void find_symbols(const exprt &src, find_symbols_sett &dest)
std::vector< literalt > bvt
Definition: literal.h:200