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 }
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
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_refinement.h
decision_proceduret::resultt::D_UNSATISFIABLE
@ D_UNSATISFIABLE
prop_conv_solvert::symbols
symbolst symbols
Definition: prop_conv.h:142
string_refinement_invariant.h
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:84
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:49
arrayst::collect_indices
void collect_indices()
Definition: arrays.cpp:74
messaget::eom
static eomt eom
Definition: message.h:284
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:202
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
find_symbols
void find_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:16
find_symbols.h
or_exprt
Boolean OR.
Definition: std_expr.h:2531
arrayst::add_array_constraints
void add_array_constraints()
Definition: arrays.cpp:260
arrayst::lazy_array_constraints
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:97
exprt::op1
exprt & op1()
Definition: expr.h:87
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
bv_pointerst
Definition: bv_pointers.h:17
irept::id
const irep_idt & id() const
Definition: irep.h:259
propt::set_frozen
virtual void set_frozen(literalt)
Definition: prop.h:111
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
bv_refinementt::post_process_arrays
void post_process_arrays() override
generate array constraints
Definition: refine_arrays.cpp:22
bv_refinementt::progress
bool progress
Definition: bv_refinement.h:108
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
to_or_expr
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2577
bv_refinementt::config_
configt config_
Definition: bv_refinement.h:113
satcheck.h
to_implies_expr
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2505
string_refinement_invariantt
#define string_refinement_invariantt(reason)
Definition: string_refinement_invariant.h:12
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:360
boolbvt::unbounded_arrayt::U_ALL
@ U_ALL
bv_refinementt::freeze_lazy_constraints
void freeze_lazy_constraints()
freeze symbols for incremental solving
Definition: refine_arrays.cpp:115
arrayst::update_index_map
void update_index_map(bool update_all)
Definition: arrays.cpp:376
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
exprt::operands
operandst & operands()
Definition: expr.h:78
messaget::debug
mstreamt & debug() const
Definition: message.h:416
arrayst::lazy_arrays
bool lazy_arrays
Definition: arrays.h:95
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
std_expr.h
bv_refinementt::configt::refine_arrays
bool refine_arrays
Enable array refinement.
Definition: bv_refinement.h:28
boolbvt::get
exprt get(const exprt &expr) const override
Definition: boolbv_get.cpp:21
validation_modet::INVARIANT
@ INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152