Go to the documentation of this file.
50 exprt current=(*it).lazy;
54 if(current.
id()==ID_implies)
65 if(current.
id()==ID_or)
69 orexp.
operands().size() == 2,
"only treats the case of a binary or");
93 INVARIANT(
false,
"error in array over approximation check");
97 log.
debug() <<
"BV-Refinement: " << nb_active
118 if(!b_it->is_constant())
std::vector< literalt > bvt
void arrays_overapproximated()
check whether counterexample is spurious
Abstraction Refinement Loop.
Base class for all expressions.
void l_set_to_true(literalt a)
#define forall_literals(it, bv)
void add_array_constraints()
std::list< lazy_constraintt > lazy_array_constraints
const irep_idt & id() const
virtual void set_frozen(literalt)
The Boolean constant false.
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...
void post_process_arrays() override
generate array constraints
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,...
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
resultt
Result of running the decision procedure.
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
message_handlert & get_message_handler()
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
int solver(std::istream &in)
void freeze_lazy_constraints()
freeze symbols for incremental solving
void update_index_map(bool update_all)
The Boolean constant true.
API to expression classes.
bool refine_arrays
Enable array refinement.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.