17 std::stack<typename clausest::size_type> s;
18 std::vector<bool> seen;
20 assert(!clauses.empty());
22 seen.resize(clauses.size(),
false);
24 s.push(clauses.size()-1);
35 const T &c=clauses[c_id];
39 for(std::size_t i=0; i<c.root_clause.size(); i++)
41 unsigned v=c.root_clause[i].var_no();
42 assert(v<in_core.size());
48 assert(c.first_clause_id<c_id);
49 s.push(c.first_clause_id);
54 assert(c.steps[i].clause_id<c_id);
55 s.push(c.steps[i].clause_id);
unsignedbv_typet size_type()
void build_core(std::vector< bool > &in_core)