17 const exprt &objective)
23 if(type.
id()==ID_bool ||
24 type.
id()==ID_unsignedbv ||
25 type.
id()==ID_c_enum ||
26 type.
id()==ID_c_enum_tag ||
27 type.
id()==ID_signedbv ||
28 type.
id()==ID_fixedbv)
33 for(std::size_t i=0; i<bv.size(); i++)
42 if(type.
id()==ID_signedbv ||
43 type.
id()==ID_fixedbv ||
44 type.
id()==ID_floatbv)
64 for(minimization_listt::const_iterator
void operator()(const minimization_listt &objectives)
The type of an expression.
void objective(const literalt condition, const weightt weight=1)
Add an objective.
const irep_idt & id() const
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT...
virtual const bvt & convert_bv(const exprt &expr)
SAT-optimizer for minimizing expressions.
virtual void set_message_handler(message_handlert &_message_handler)
std::set< exprt > minimization_listt
message_handlert & get_message_handler()
Base class for all expressions.
long long signed int weightt
void add_objective(class prop_minimizet &prop_minimize, const exprt &objective)
std::vector< literalt > bvt