15 const exprt &objective)
31 for(std::size_t i=0; i<bv.size(); i++)
61 for(minimization_listt::const_iterator
SAT-optimizer for minimizing expressions.
std::set< exprt > minimization_listt
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
void operator()(const minimization_listt &objectives)
void add_objective(class prop_minimizet &prop_minimize, const exprt &objective)
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & id() const
message_handlert & get_message_handler()
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT.
The type of an expression, extends irept.
std::vector< literalt > bvt