cprover
Loading...
Searching...
No Matches
refine_arrays.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
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);
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}
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
Abstraction Refinement Loop.
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:114
const namespacet & ns
Definition: arrays.h:56
bool lazy_arrays
Definition: arrays.h:111
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:400
messaget log
Definition: arrays.h:57
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:20
void freeze_lazy_constraints()
freeze symbols for incremental solving
void arrays_overapproximated()
check whether counterexample is spurious
void finish_eager_conversion_arrays() override
generate array constraints
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:2865
Boolean implication.
Definition: std_expr.h:2037
const irep_idt & id() const
Definition: irep.h:396
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:2082
void l_set_to_true(literalt a)
Definition: prop.h:51
virtual void set_frozen(literalt)
Definition: prop.h:113
The Boolean constant true.
Definition: std_expr.h:2856
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)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
API to expression classes.
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2129
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2062
bool refine_arrays
Enable array refinement.
Definition: bv_refinement.h:28