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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110

#ifndef _stack_h_INCLUDED
#define _stack_h_INCLUDED

#include <stdlib.h>

#define STACK(TYPE) \
  struct { \
    TYPE *begin; \
    TYPE *end; \
    TYPE *allocated; \
  }

#define FULL_STACK(S) ((S).end == (S).allocated)
#define EMPTY_STACK(S) ((S).begin == (S).end)
#define SIZE_STACK(S) ((size_t) ((S).end - (S).begin))
#define CAPACITY_STACK(S) ((size_t) ((S).allocated - (S).begin))

#define INIT_STACK(S) \
  do { \
    (S).begin = (S).end = (S).allocated = 0; \
  } while (0)

#define TOP_STACK(S) (END_STACK (S)[assert (!EMPTY_STACK (S)), -1])

#define PEEK_STACK(S, N) \
  (BEGIN_STACK (S)[assert ((N) < SIZE_STACK (S)), (N)])

#define POKE_STACK(S, N, E) \
  do { \
    PEEK_STACK (S, N) = (E); \
  } while (0)

#define POP_STACK(S) (assert (!EMPTY_STACK (S)), *--(S).end)

#define PUSH_STACK(S, E) \
  do { \
    if (FULL_STACK (S)) \
      ENLARGE_STACK (S); \
    *(S).end++ = (E); \
  } while (0)

#define BEGIN_STACK(S) (S).begin

#define END_STACK(S) (S).end

#define CLEAR_STACK(S) \
  do { \
    (S).end = (S).begin; \
  } while (0)

#define RESIZE_STACK(S, NEW_SIZE) \
  do { \
    const size_t TMP_NEW_SIZE = (NEW_SIZE); \
    assert (TMP_NEW_SIZE <= SIZE_STACK (S)); \
    (S).end = (S).begin + TMP_NEW_SIZE; \
  } while (0)

#define SET_END_OF_STACK(S, P) \
  do { \
    assert (BEGIN_STACK (S) <= (P)); \
    assert ((P) <= END_STACK (S)); \
    if ((P) == END_STACK (S)) \
      break; \
    (S).end = (P); \
  } while (0)

#define RELEASE_STACK(S) \
  do { \
    DEALLOC ((S).begin, CAPACITY_STACK (S)); \
    INIT_STACK (S); \
  } while (0)

#define REMOVE_STACK(T, S, E) \
  do { \
    assert (!EMPTY_STACK (S)); \
    T *END_REMOVE_STACK = END_STACK (S); \
    T *P_REMOVE_STACK = BEGIN_STACK (S); \
    while (*P_REMOVE_STACK != (E)) { \
      P_REMOVE_STACK++; \
      assert (P_REMOVE_STACK != END_REMOVE_STACK); \
    } \
    P_REMOVE_STACK++; \
    while (P_REMOVE_STACK != END_REMOVE_STACK) { \
      P_REMOVE_STACK[-1] = *P_REMOVE_STACK; \
      P_REMOVE_STACK++; \
    } \
    (S).end--; \
  } while (0)

#define all_stack(T, E, S) \
  T E, *E##_PTR = BEGIN_STACK (S), *const E##_END = END_STACK (S); \
  E##_PTR != E##_END && (E = *E##_PTR, true); \
  ++E##_PTR

#define all_pointers(T, E, S) \
  T *E, *const *E##_PTR = BEGIN_STACK (S), \
               *const *const E##_END = END_STACK (S); \
  E##_PTR != E##_END && (E = *E##_PTR, true); \
  ++E##_PTR

// clang-format off

typedef STACK (char) chars;
typedef STACK (int) ints;
typedef STACK (size_t) sizes;
typedef STACK (unsigned) unsigneds;

// clang-format on

#endif