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()))
105 debug() <<
"BV-Refinement: " << nb_active
106 <<
" array expressions become active" <<
eom;
108 <<
" inactive array expressions" <<
eom;
122 std::set<symbol_exprt>
symbols;
124 for(
const auto &symbol :
symbols)
128 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 an exprt to a or_exprt.
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
#define forall_literals(it, bv)
void post_process_arrays() override
generate array constraints
void l_set_to_true(literalt a)
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
const irep_idt & id() const
The Boolean constant true.
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)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
void find_symbols(const exprt &src, find_symbols_sett &dest)
std::vector< literalt > bvt