Go to the documentation of this file.
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)
Copy the given argument to the end of exprt's operands.
long long signed int weightt
#define PRECONDITION(CONDITION)
virtual void set_assumptions(const bvt &_assumptions)
void operator()()
Try to cover all objectives.
void objective(const literalt condition, const weightt weight=1)
Add an objective.
objectivest::reverse_iterator current
std::vector< literalt > bvt
mstreamt & status() const
#define forall_literals(it, bv)
virtual void set_to(const exprt &expr, bool value)=0
virtual literalt convert(const exprt &expr)=0
std::size_t _number_objectives
virtual resultt dec_solve()=0
literalt const_literal(bool value)
#define POSTCONDITION(CONDITION)
std::size_t _number_satisfied
virtual tvt l_get(literalt a) const =0
void fix_objectives()
Fix objectives that are satisfied.
virtual bool has_set_assumptions() const
literalt constraint()
Build constraints that require us to improve on at least one goal, greedily.