17 #ifndef CPROVER_SOLVERS_FLATTENING_BV_MINIMIZE_H 18 #define CPROVER_SOLVERS_FLATTENING_BV_MINIMIZE_H 40 const exprt &objective);
48 return "Bit vector minimizing SAT";
60 bv_minimize(objectives);
66 #endif // CPROVER_SOLVERS_FLATTENING_BV_MINIMIZE_H void operator()(const minimization_listt &objectives)
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT...
virtual void set_message_handler(message_handlert &_message_handler)
virtual const std::string description()
std::set< exprt > minimization_listt
bv_minimizing_dect(const namespacet &_ns)
message_handlert & get_message_handler()
Base class for all expressions.
bv_minimizet(boolbvt &_boolbv)
void add_objective(class prop_minimizet &prop_minimize, const exprt &objective)
void minimize(const minimization_listt &objectives)