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 #include <langapi/language_util.h>
14 #endif
15 
16 #include <util/std_expr.h>
17 #include <util/find_symbols.h>
18 
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);
58  assert(imp.operands().size()==2);
59  exprt implies_simplified=get(imp.op0());
60  if(implies_simplified==false_exprt())
61  {
62  ++it;
63  continue;
64  }
65  }
66 
67  if(current.id()==ID_or)
68  {
69  or_exprt orexp=to_or_expr(current);
70  assert(orexp.operands().size()==2);
71  exprt o1=get(orexp.op0());
72  exprt o2=get(orexp.op1());
73  if(o1==true_exprt() || o2 == true_exprt())
74  {
75  ++it;
76  continue;
77  }
78  }
79 
80  exprt simplified=get(current);
81  solver << simplified;
82 
83  switch(static_cast<decision_proceduret::resultt>(sat_check.prop_solve()))
84  {
86  ++it;
87  break;
89  prop.l_set_to_true(convert(current));
90  nb_active++;
91  lazy_array_constraints.erase(it++);
92  break;
93  default:
94  assert(false);
95  }
96  }
97 
98  debug() << "BV-Refinement: " << nb_active
99  << " array expressions become active" << eom;
100  debug() << "BV-Refinement: " << lazy_array_constraints.size()
101  << " inactive array expressions" << eom;
102  if(nb_active > 0)
103  progress=true;
104 }
105 
106 
109 {
110  if(!lazy_arrays)
111  return;
112 
113  for(std::list<lazy_constraintt>::iterator
114  l_it=lazy_array_constraints.begin();
115  l_it!=lazy_array_constraints.end(); ++l_it)
116  {
117  std::set<symbol_exprt> symbols;
118  find_symbols(l_it->lazy, symbols);
119  for(std::set<symbol_exprt>::const_iterator it=symbols.begin();
120  it!=symbols.end(); ++it)
121  {
122  bvt bv=convert_bv(l_it->lazy);
123  forall_literals(b_it, bv)
124  if(!b_it->is_constant())
125  prop.set_frozen(*b_it);
126  }
127  }
128 }
bool lazy_arrays
Definition: arrays.h:95
void freeze_lazy_constraints()
freeze symbols for incremental solving
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
virtual void set_frozen(literalt a)
Definition: prop.h:109
boolean OR
Definition: std_expr.h:1968
exprt & op0()
Definition: expr.h:84
void add_array_constraints()
Definition: arrays.cpp:244
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void post_process_arrays()
generate array constraints
#define forall_literals(it, bv)
Definition: literal.h:199
boolean implication
Definition: std_expr.h:1926
void l_set_to_true(literalt a)
Definition: prop.h:47
symbolst symbols
Definition: prop_conv.h:132
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:3742
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
void update_index_map(bool update_all)
Definition: arrays.cpp:360
API to expression classes.
exprt & op1()
Definition: expr.h:87
void collect_indices()
Definition: arrays.cpp:70
const namespacet & ns
The boolean constant false.
Definition: std_expr.h:3753
void arrays_overapproximated()
check whether counterexample is spurious
mstreamt & debug()
Definition: message.h:253
bool do_array_refinement
Definition: bv_refinement.h:40
unbounded_arrayt unbounded_array
Definition: boolbv.h:76
Base class for all expressions.
Definition: expr.h:46
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:97
mstreamt & progress()
Definition: message.h:248
Abstraction Refinement Loop.
operandst & operands()
Definition: expr.h:70
void find_symbols(const exprt &src, find_symbols_sett &dest)
std::vector< literalt > bvt
Definition: literal.h:197
virtual resultt prop_solve() override
const implies_exprt & to_implies_expr(const exprt &expr)
Cast a generic exprt to a implies_exprt.
Definition: std_expr.h:1949
const or_exprt & to_or_expr(const exprt &expr)
Cast a generic exprt to a or_exprt.
Definition: std_expr.h:2019