12 #ifndef CPROVER_SOLVERS_PROP_MINIMIZE_H 13 #define CPROVER_SOLVERS_PROP_MINIMIZE_H 75 typedef std::map<weightt, std::vector<objectivet> >
objectivest;
90 #endif // CPROVER_SOLVERS_PROP_MINIMIZE_H void objective(const literalt condition, const weightt weight=1)
Add an objective.
Computes a satisfying assignment of minimal cost according to a const function using incremental SAT...
unsigned iterations() const
objectivet(const literalt _condition)
objectivest::reverse_iterator current
long long signed int weightt
std::map< weightt, std::vector< objectivet > > objectivest
literalt constraint()
Build constraints that require us to improve on at least one goal, greedily.
std::size_t _number_satisfied
std::size_t _number_objectives
void fix_objectives()
Fix objectives that are satisfied.
std::size_t number_satisfied() const
prop_minimizet(prop_convt &_prop_conv)
void operator()()
Try to cover all objectives.