12 #ifndef CPROVER_SOLVERS_PROP_COVER_GOALS_H 13 #define CPROVER_SOLVERS_PROP_COVER_GOALS_H 73 goals.back().condition=condition;
105 #endif // CPROVER_SOLVERS_PROP_COVER_GOALS_H std::list< goalt > goalst
unsignedbv_typet size_type()
void mark()
Mark goals that are covered.
decision_proceduret::resultt operator()()
Try to cover all goals.
virtual void satisfying_assignment()
void constraint()
Build clause.
void freeze_goal_variables()
Build clause.
cover_goalst(prop_convt &_prop_conv)
std::size_t _number_covered
std::size_t number_covered() const
void add(const literalt condition)
unsigned iterations() const
Try to cover some given set of goals incrementally.
std::vector< observert * > observerst
enum cover_goalst::goalt::statust status
void register_observer(observert &o)
goalst::size_type size() const
virtual void goal_covered(const goalt &)