6 #define EDGE_IS_VAR_CONSTANT 2
8 #define EDGE_MASK (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)
11 typedef struct Edge Edge;
14 typedef struct Node Node;
26 typedef enum NodeType NodeType;
32 typedef struct NodeFlags NodeFlags;
41 #define DEFAULT_CNF_ARRAY_SIZE 256
42 #define LOAD_FACTOR 0.25
43 #define enableMatching 1
54 typedef struct CNF CNF;
56 static inline Edge constraintNegate(Edge e) {
57 Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
61 static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
62 return ! (((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~ (uintptr_t) NEGATE_EDGE));
65 static inline bool sameSignEdge(Edge e1, Edge e2) {
66 return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
69 static inline bool sameNodeOppSign(Edge e1, Edge e2) {
70 return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
73 static inline bool isNegEdge(Edge e) {
74 return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
77 static inline bool isNodeEdge(Edge e) {
78 return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
81 static inline bool isNegNodeEdge(Edge e) {
82 return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
85 static inline Node * getNodePtrFromEdge(Edge e) {
86 return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
89 static inline NodeType getNodeType(Edge e) {
90 Node * n=getNodePtrFromEdge(e);
94 static inline bool equalsEdge(Edge e1, Edge e2) {
95 return e1.node_ptr == e2.node_ptr;
98 static inline bool ltEdge(Edge e1, Edge e2) {
99 return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr;
102 static inline uint getNodeSize(Edge e) {
103 Node * n=getNodePtrFromEdge(e);
107 static inline Edge * getEdgeArray(Edge e) {
108 Node * n=getNodePtrFromEdge(e);
112 static inline Edge getNonNeg(Edge e) {
113 Edge enew={(Node *)(((uintptr_t)e.node_ptr)&(~((uintptr_t)NEGATE_EDGE)))};
117 static inline bool edgeIsConst(Edge e) {
118 return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
121 uint hashNode(NodeType type, uint numEdges, Edge * edges);
122 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode);
123 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges);
124 Edge create(CNF *cnf, NodeType type, uint numEdges, Edge * edges);
125 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges);
126 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges);
127 Edge constraintOR2(CNF * cnf, Edge left, Edge right);
128 Edge constraintAND2(CNF * cnf, Edge left, Edge right);
129 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right);
130 Edge constraintIFF(CNF * cnf, Edge left, Edge right);
131 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge);
132 Edge constraintNewVar(CNF *cnf);
134 Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
135 Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};