Go to the documentation of this file.
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
Class that provides messages with a built-in verbosity 'level'.
std::list< goalt > goalst
std::size_t _number_covered
virtual void goal_covered(const goalt &)
Try to cover some given set of goals incrementally.
std::size_t number_covered() const
cover_goalst(prop_convt &_prop_conv)
decision_proceduret::resultt operator()()
Try to cover all goals.
unsigned iterations() const
void mark()
Mark goals that are covered.
void constraint()
Build clause.
void register_observer(observert &o)
enum cover_goalst::goalt::statust status
virtual void satisfying_assignment()
goalst::size_type size() const
void add(const literalt condition)
std::vector< observert * > observerst
void freeze_goal_variables()
Build clause.
unsignedbv_typet size_type()