Go to the documentation of this file.
21 : prop_conv(_prop_conv), log(message_handler)
43 std::vector<objectivet> &entry =
current->second;
46 for(std::vector<objectivet>::iterator o_it = entry.begin();
66 std::vector<objectivet> &entry =
current->second;
70 for(std::vector<objectivet>::iterator o_it = entry.begin();
75 or_clause.push_back(!o_it->condition);
82 else if(or_clause.size() == 1)
83 return or_clause.front();
87 disjuncts.reserve(or_clause.size());
101 bool last_was_SAT =
false;
126 last_was_SAT =
false;
136 last_was_SAT =
false;
long long signed int weightt
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
virtual void push(const std::vector< exprt > &assumptions)=0
Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.
mstreamt & status() const
#define forall_literals(it, bv)
virtual void set_to(const exprt &expr, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
virtual literalt convert(const exprt &expr)=0
Convert a Boolean expression and return the corresponding literal.
std::size_t _number_objectives
prop_minimizet(prop_convt &_prop_conv, message_handlert &message_handler)
literalt const_literal(bool value)
std::vector< exprt > operandst
std::size_t _number_satisfied
resultt
Result of running the decision procedure.
void fix_objectives()
Fix objectives that are satisfied.
#define POSTCONDITION(CONDITION)
virtual void pop()=0
Pop whatever is on top of the stack.
literalt constraint()
Build constraints that require us to improve on at least one goal, greedily.
virtual tvt l_get(literalt l) const =0
Return value of literal l from satisfying assignment.