7 #define EDGE_IS_VAR_CONSTANT 2
9 #define EDGE_MASK (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)
14 typedef struct Edge Edge;
17 typedef struct Node Node;
31 typedef enum NodeType NodeType;
43 typedef struct Node Node;
45 #define DEFAULT_CNF_ARRAY_SIZE 2048
51 IncrementalSolver *solver;
58 typedef struct CNF CNF;
60 static inline Edge constraintNegate(Edge e) {
61 Edge eneg = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
65 static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
66 return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~(uintptr_t) NEGATE_EDGE));
69 static inline bool sameSignEdge(Edge e1, Edge e2) {
70 return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
73 static inline bool sameNodeOppSign(Edge e1, Edge e2) {
74 return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
77 static inline bool isNegEdge(Edge e) {
78 return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
81 static inline bool isPosEdge(Edge e) {
82 return !(((uintptr_t)e.node_ptr) & NEGATE_EDGE);
85 static inline bool isNodeEdge(Edge e) {
86 return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
89 static inline bool isNegNodeEdge(Edge e) {
90 return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
93 static inline bool isPosNodeEdge(Edge e) {
94 return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == 0;
97 static inline Node *getNodePtrFromEdge(Edge e) {
98 return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
101 static inline NodeType getNodeType(Edge e) {
102 Node *n = getNodePtrFromEdge(e);
106 static inline bool equalsEdge(Edge e1, Edge e2) {
107 return e1.node_ptr == e2.node_ptr;
110 static inline bool ltEdge(Edge e1, Edge e2) {
111 return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr;
114 static inline uint getNodeSize(Edge e) {
115 Node *n = getNodePtrFromEdge(e);
119 static inline Edge *getEdgeArray(Edge e) {
120 Node *n = getNodePtrFromEdge(e);
124 static inline Edge getNonNeg(Edge e) {
125 Edge enew = {(Node *)(((uintptr_t)e.node_ptr) & (~((uintptr_t)NEGATE_EDGE)))};
129 static inline bool edgeIsConst(Edge e) {
130 return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
133 static inline bool edgeIsNull(Edge e) {
134 return e.node_ptr == NULL;
137 static inline bool edgeIsVarConst(Edge e) {
138 return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
141 static inline Edge constraintNegateIf(Edge e, bool negate) {
142 Edge eret = {(Node *)(((uintptr_t)e.node_ptr) ^ negate)};
146 static inline Literal getEdgeVar(Edge e) {
147 int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT);
148 return isNegEdge(e) ? -val : val;
152 void deleteCNF(CNF *cnf);
153 void resetCNF(CNF *cnf);
155 uint hashNode(NodeType type, uint numEdges, Edge *edges);
156 Node *allocNode(NodeType type, uint numEdges, Edge *edges);
157 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges);
158 Edge createNode(NodeType type, uint numEdges, Edge *edges);
159 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges);
160 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges);
161 Edge constraintOR2(CNF *cnf, Edge left, Edge right);
162 Edge constraintAND2(CNF *cnf, Edge left, Edge right);
163 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right);
164 Edge constraintIFF(CNF *cnf, Edge left, Edge right);
165 static inline Edge constraintXOR(CNF *cnf, Edge left, Edge right) {return constraintNegate(constraintIFF(cnf, left,right));}
166 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge);
167 Edge constraintNewVar(CNF *cnf);
168 void countPass(CNF *cnf);
169 void countConstraint(CNF *cnf, VectorEdge *stack, Edge e);
170 void addConstraintCNF(CNF *cnf, Edge constraint);
171 int solveCNF(CNF *cnf);
172 bool getValueCNF(CNF *cnf, Edge var);
173 void printCNF(Edge e);
174 Node *allocBaseNode(NodeType type, uint numEdges);
175 Node *allocResizeNode(uint capacity);
176 Edge cloneEdge(Edge e);
177 void addEdgeToResizeNode(Node **node, Edge e);
178 void mergeFreeNodeToResizeNode(Node **node, Node *innode);
179 void mergeNodeToResizeNode(Node **node, Node *innode);
180 void freeEdgeRec(Edge e);
181 void outputCNF(CNF *cnf, Edge cnfform);
182 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar);
183 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p);
184 void addClause(CNF *cnf, uint numliterals, int *literals);
185 void freezeVariable(CNF *cnf, Edge e);
186 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
187 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
188 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
189 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
190 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);