20 std::stack<typename clausest::size_type> s;
21 std::vector<bool> seen;
23 seen.resize(clauses.size(),
false);
25 s.push(clauses.size()-1);
29 typename clausest::size_type
c_id=s.top();
36 const T &
c=clauses[
c_id];
40 for(std::size_t
i=0;
i<
c.root_clause.size();
i++)
42 unsigned v=
c.root_clause[
i].var_no();
44 v < in_core.size(),
"variable number should be within bounds");
51 c.first_clause_id <
c_id,
52 "id of the clause to be pushed onto the clause stack shall be smaller "
53 "than the id of the current clause");
54 s.push(
c.first_clause_id);
56 for(clauset::stepst::size_type
i=0;
i<
c.steps.size();
i++)
60 c.steps[
i].clause_id <
c_id,
61 "id of the clause to be pushed onto the clause stack shall be "
62 "smaller than the id of the current clause");
63 s.push(
c.steps[
i].clause_id);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
void build_core(std::vector< bool > &in_core)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.