44 std::vector<objectivet> &entry =
current->second;
47 for(std::vector<objectivet>::iterator o_it = entry.begin();
51 if(!o_it->fixed &&
prop_conv.l_get(o_it->condition).is_false())
67 std::vector<objectivet> &entry =
current->second;
71 for(std::vector<objectivet>::iterator o_it = entry.begin();
76 or_clause.push_back(!o_it->condition);
83 else if(or_clause.size() == 1)
84 return or_clause.front();
88 disjuncts.reserve(or_clause.size());
89 for(
const auto &literal : or_clause)
102 bool last_was_SAT =
false;
127 last_was_SAT =
false;
137 last_was_SAT =
false;
resultt
Result of running the decision procedure.
std::vector< exprt > operandst
prop_minimizet(prop_convt &_prop_conv, message_handlert &message_handler)
void fix_objectives()
Fix objectives that are satisfied.
std::size_t _number_objectives
std::size_t _number_satisfied
long long signed int weightt
literalt constraint()
Build constraints that require us to improve on at least one goal, greedily.
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
literalt const_literal(bool value)
#define POSTCONDITION(CONDITION)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...