47 satcheck_no_simplifiert sat_check;
51 exprt current=(*it).lazy;
55 if(current.
id()==ID_implies)
61 exprt implies_simplified=
get(imp.
op0());
69 if(current.
id()==ID_or)
84 exprt simplified=
get(current);
87 switch(static_cast<decision_proceduret::resultt>(sat_check.prop_solve()))
98 error() <<
"error in array over approximation check" <<
eom;
108 debug() <<
"BV-Refinement: " << nb_active
109 <<
" array expressions become active" <<
eom;
111 <<
" inactive array expressions" <<
eom;
125 std::set<symbol_exprt>
symbols;
127 for(
const auto &symbol :
symbols)
131 if(!b_it->is_constant())
void freeze_lazy_constraints()
freeze symbols for incremental solving
literalt convert(const exprt &expr) override
void add_array_constraints()
mstreamt & progress() const
const or_exprt & to_or_expr(const exprt &expr)
Cast a generic exprt to a or_exprt.
static mstreamt & eom(mstreamt &m)
#define forall_literals(it, bv)
void post_process_arrays() override
generate array constraints
#define INVARIANT(CONDITION, REASON)
void l_set_to_true(literalt a)
const implies_exprt & to_implies_expr(const exprt &expr)
Cast a generic exprt to a implies_exprt.
const irep_idt & id() const
The boolean constant true.
virtual const bvt & convert_bv(const exprt &expr)
bool refine_arrays
Enable array refinement.
int solver(std::istream &in)
void update_index_map(bool update_all)
API to expression classes.
virtual void set_frozen(literalt)
The boolean constant false.
void arrays_overapproximated()
check whether counterexample is spurious
Base class for all expressions.
std::list< lazy_constraintt > lazy_array_constraints
#define string_refinement_invariantt(reason)
Abstraction Refinement Loop.
#define DATA_INVARIANT(CONDITION, REASON)
void find_symbols(const exprt &src, find_symbols_sett &dest)
std::vector< literalt > bvt