cprover
resolution_proof.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "resolution_proof.h"
10 
11 #include <cassert>
12 #include <stack>
13 
14 template<class T>
15 void resolution_prooft<T>::build_core(std::vector<bool> &in_core)
16 {
17  std::stack<typename clausest::size_type> s;
18  std::vector<bool> seen;
19 
20  assert(!clauses.empty());
21 
22  seen.resize(clauses.size(), false);
23 
24  s.push(clauses.size()-1);
25 
26  while(!s.empty())
27  {
28  typename clausest::size_type c_id=s.top();
29  s.pop();
30 
31  if(seen[c_id])
32  continue;
33  seen[c_id]=true;
34 
35  const T &c=clauses[c_id];
36 
37  if(c.is_root)
38  {
39  for(std::size_t i=0; i<c.root_clause.size(); i++)
40  {
41  unsigned v=c.root_clause[i].var_no();
42  assert(v<in_core.size());
43  in_core[v]=true;
44  }
45  }
46  else
47  {
48  assert(c.first_clause_id<c_id);
49  s.push(c.first_clause_id);
50 
51  for(clauset::stepst::size_type i=0; i<c.steps.size(); i++)
52  {
53  // must decrease
54  assert(c.steps[i].clause_id<c_id);
55  s.push(c.steps[i].clause_id);
56  }
57  }
58  }
59 }
60 
61 template class resolution_prooft<clauset>;
unsignedbv_typet size_type()
Definition: c_types.cpp:58
void build_core(std::vector< bool > &in_core)