38 std::vector<objectivet> &entry=
current->second;
41 for(std::vector<objectivet>::iterator
63 std::vector<objectivet> &entry=
current->second;
67 for(std::vector<objectivet>::iterator
73 or_clause.push_back(!o_it->condition);
80 else if(or_clause.size()==1)
81 return or_clause.front();
101 bool last_was_SAT=
false;
123 assumptions.push_back(c);
139 error() <<
"decision procedure failed" <<
eom;
void copy_to_operands(const exprt &expr)
void objective(const literalt condition, const weightt weight=1)
Add an objective.
static mstreamt & eom(mstreamt &m)
#define forall_literals(it, bv)
virtual resultt dec_solve()=0
virtual literalt convert(const exprt &expr)=0
virtual void set_to(const exprt &expr, bool value)=0
literalt const_literal(bool value)
virtual bool has_set_assumptions() const
virtual tvt l_get(literalt a) const =0
objectivest::reverse_iterator current
long long signed int weightt
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::vector< literalt > bvt
virtual void set_assumptions(const bvt &_assumptions)
void operator()()
Try to cover all objectives.