+typedef enum NodeType NodeType;
+
+struct NodeFlags {
+ NodeType type : 2;
+ int varForced : 1;
+ int wasExpanded : 2;
+ int cnfVisitedDown : 2;
+ int cnfVisitedUp : 2;
+};
+
+typedef struct NodeFlags NodeFlags;
+
+struct Node {
+ NodeFlags flags;
+ uint numEdges;
+ uint hashCode;
+ uint intAnnot[2];
+ void *ptrAnnot[2];
+ Edge edges[];
+};
+
+#define DEFAULT_CNF_ARRAY_SIZE 256
+#define LOAD_FACTOR 0.25
+
+struct CNF {
+ uint varcount;
+ uint capacity;
+ uint size;
+ uint mask;
+ uint maxsize;
+ bool enableMatching;
+ Node **node_array;
+ IncrementalSolver *solver;
+ VectorEdge constraints;
+ VectorEdge args;
+ long long solveTime;
+ long long encodeTime;
+};
+
+typedef struct CNF CNF;
+
+struct CNFExpr;
+typedef struct CNFExpr CNFExpr;
+
+static inline bool getExpanded(Node *n, int isNegated) {
+ return n->flags.wasExpanded & (1 << isNegated);
+}
+
+static inline void setExpanded(Node *n, int isNegated) {
+ n->flags.wasExpanded |= (1 << isNegated);
+}
+
+static inline Edge constraintNegate(Edge e) {
+ Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
+ return enew;
+}
+
+static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
+ return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~(uintptr_t) NEGATE_EDGE));
+}
+
+static inline bool sameSignEdge(Edge e1, Edge e2) {
+ return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
+}
+
+static inline bool sameNodeOppSign(Edge e1, Edge e2) {
+ return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
+}
+
+static inline bool isNegEdge(Edge e) {
+ return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
+}
+
+static inline bool isPosEdge(Edge e) {
+ return !(((uintptr_t)e.node_ptr) & NEGATE_EDGE);
+}
+
+static inline bool isNodeEdge(Edge e) {
+ return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
+}
+
+static inline bool isNegNodeEdge(Edge e) {
+ return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
+}
+
+static inline Node *getNodePtrFromEdge(Edge e) {
+ return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
+}
+
+static inline NodeType getNodeType(Edge e) {
+ Node *n = getNodePtrFromEdge(e);
+ return n->flags.type;
+}
+
+static inline bool equalsEdge(Edge e1, Edge e2) {
+ return e1.node_ptr == e2.node_ptr;
+}
+
+static inline bool ltEdge(Edge e1, Edge e2) {
+ return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr;
+}
+
+static inline uint getNodeSize(Edge e) {
+ Node *n = getNodePtrFromEdge(e);
+ return n->numEdges;
+}
+
+static inline Edge *getEdgeArray(Edge e) {
+ Node *n = getNodePtrFromEdge(e);
+ return n->edges;
+}
+
+static inline Edge getNonNeg(Edge e) {
+ Edge enew = {(Node *)(((uintptr_t)e.node_ptr) & (~((uintptr_t)NEGATE_EDGE)))};
+ return enew;
+}
+
+static inline bool edgeIsConst(Edge e) {
+ return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
+}
+
+static inline bool edgeIsNull(Edge e) {
+ return e.node_ptr == NULL;
+}
+
+static inline bool edgeIsVarConst(Edge e) {
+ return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
+}
+
+static inline Edge constraintNegateIf(Edge e, bool negate) {
+ Edge eret = {(Node *)(((uintptr_t)e.node_ptr) ^ negate)};
+ return eret;
+}
+
+static inline Literal getEdgeVar(Edge e) {
+ int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT);
+ return isNegEdge(e) ? -val : val;
+}
+
+static inline bool isProxy(CNFExpr *expr) {
+ return (bool) (((intptr_t) expr) & 1);
+}