rustsat-cadical 0.7.5

Interface to the SAT solver CaDiCaL for the RustSAT library.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36

#ifndef _occs_h_INCLUDED
#define _occs_h_INCLUDED

#include <vector>

namespace CaDiCaL {

// Full occurrence lists used in a one-watch scheme for all clauses in
// subsumption checking and for irredundant clauses in variable elimination.

struct Clause;
using namespace std;

typedef vector<Clause *> Occs;

inline void shrink_occs (Occs &os) { shrink_vector (os); }
inline void erase_occs (Occs &os) { erase_vector (os); }

inline void remove_occs (Occs &os, Clause *c) {
  const auto end = os.end ();
  auto i = os.begin ();
  for (auto j = i; j != end; j++) {
    const Clause *d = *i++ = *j;
    if (c == d)
      i--;
  }
  assert (i + 1 == end);
  os.resize (i - os.begin ());
}

typedef Occs::iterator occs_iterator;
typedef Occs::const_iterator const_occs_iterator;

} // namespace CaDiCaL

#endif