26 o->satisfying_assignment();
49 for(
const auto &g :
goals)
51 disjuncts.push_back(g.condition);
std::size_t _number_covered
std::size_t number_covered() const
goalst::size_type size() const
decision_proceduret::resultt operator()(message_handlert &)
Try to cover all goals.
void constraint()
Build clause.
void mark()
Mark goals that are covered.
decision_proceduret & decision_procedure
resultt
Result of running the decision procedure.
std::vector< exprt > operandst
Class that provides messages with a built-in verbosity 'level'.
Cover a set of goals incrementally.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
API to expression classes.