27 o->satisfying_assignment();
37 for(
const auto &o : observers)
49 for(std::list<goalt>::const_iterator
54 !g_it->condition.is_false())
64 for(std::list<goalt>::const_iterator
68 if(!g_it->condition.is_constant())
102 error() <<
"decision procedure has failed" <<
eom;
void mark()
Mark goals that are covered.
static mstreamt & eom(mstreamt &m)
decision_proceduret::resultt operator()()
Try to cover all goals.
void constraint()
Build clause.
virtual resultt dec_solve()=0
void freeze_goal_variables()
Build clause.
std::size_t _number_covered
std::size_t number_covered() const
exprt disjunction(const exprt::operandst &op)
std::vector< exprt > operandst
virtual tvt l_get(literalt a) const =0
void set_to_true(const exprt &expr)
Cover a set of goals incrementally.
virtual void set_frozen(literalt a)
goalst::size_type size() const