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;
37 int cnfVisitedDown : 2;
41 typedef struct NodeFlags NodeFlags;
52 #define DEFAULT_CNF_ARRAY_SIZE 256
53 #define LOAD_FACTOR 0.25
63 IncrementalSolver *solver;
64 VectorEdge constraints;
70 typedef struct CNF CNF;
73 typedef struct CNFExpr CNFExpr;
75 static inline bool getExpanded(Node *n, int isNegated) {
76 return n->flags.wasExpanded & (1 << isNegated);
79 static inline void setExpanded(Node *n, int isNegated) {
80 n->flags.wasExpanded |= (1 << isNegated);
83 static inline Edge constraintNegate(Edge e) {
84 Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
88 static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
89 return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~(uintptr_t) NEGATE_EDGE));
92 static inline bool sameSignEdge(Edge e1, Edge e2) {
93 return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
96 static inline bool sameNodeOppSign(Edge e1, Edge e2) {
97 return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
100 static inline bool isNegEdge(Edge e) {
101 return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
104 static inline bool isPosEdge(Edge e) {
105 return !(((uintptr_t)e.node_ptr) & NEGATE_EDGE);
108 static inline bool isNodeEdge(Edge e) {
109 return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
112 static inline bool isNegNodeEdge(Edge e) {
113 return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
116 static inline Node *getNodePtrFromEdge(Edge e) {
117 return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
120 static inline NodeType getNodeType(Edge e) {
121 Node *n = getNodePtrFromEdge(e);
122 return n->flags.type;
125 static inline bool equalsEdge(Edge e1, Edge e2) {
126 return e1.node_ptr == e2.node_ptr;
129 static inline bool ltEdge(Edge e1, Edge e2) {
130 return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr;
133 static inline uint getNodeSize(Edge e) {
134 Node *n = getNodePtrFromEdge(e);
138 static inline Edge *getEdgeArray(Edge e) {
139 Node *n = getNodePtrFromEdge(e);
143 static inline Edge getNonNeg(Edge e) {
144 Edge enew = {(Node *)(((uintptr_t)e.node_ptr) & (~((uintptr_t)NEGATE_EDGE)))};
148 static inline bool edgeIsConst(Edge e) {
149 return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
152 static inline bool edgeIsNull(Edge e) {
153 return e.node_ptr == NULL;
156 static inline bool edgeIsVarConst(Edge e) {
157 return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
160 static inline Edge constraintNegateIf(Edge e, bool negate) {
161 Edge eret = {(Node *)(((uintptr_t)e.node_ptr) ^ negate)};
165 static inline Literal getEdgeVar(Edge e) {
166 int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT);
167 return isNegEdge(e) ? -val : val;
170 static inline bool isProxy(CNFExpr *expr) {
171 return (bool) (((intptr_t) expr) & 1);
174 static inline Literal getProxy(CNFExpr *expr) {
175 return (Literal) (((intptr_t) expr) >> 1);
179 void deleteCNF(CNF *cnf);
181 uint hashNode(NodeType type, uint numEdges, Edge *edges);
182 Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashCode);
183 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges);
184 Edge create(CNF *cnf, NodeType type, uint numEdges, Edge *edges);
185 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges);
186 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges);
187 Edge constraintOR2(CNF *cnf, Edge left, Edge right);
188 Edge constraintAND2(CNF *cnf, Edge left, Edge right);
189 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right);
190 Edge constraintIFF(CNF *cnf, Edge left, Edge right);
191 static inline Edge constraintXOR(CNF *cnf, Edge left, Edge right) {return constraintNegate(constraintIFF(cnf, left,right));}
192 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge);
193 Edge constraintNewVar(CNF *cnf);
194 void countPass(CNF *cnf);
195 void countConstraint(CNF *cnf, VectorEdge *stack, Edge e);
196 void addConstraintCNF(CNF *cnf, Edge constraint);
197 int solveCNF(CNF *cnf);
198 bool getValueCNF(CNF *cnf, Edge var);
199 void printCNF(Edge e);
201 void convertPass(CNF *cnf, bool backtrackLit);
202 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
203 void constrainCNF(CNF *cnf, Literal l, CNFExpr *exp);
204 void produceCNF(CNF *cnf, Edge e);
205 CNFExpr *produceConjunction(CNF *cnf, Edge e);
206 CNFExpr *produceDisjunction(CNF *cnf, Edge e);
207 bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate);
208 void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign);
209 CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge);
210 Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg);
211 void outputCNF(CNF *cnf, CNFExpr *expr);
213 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
214 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
215 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
216 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
217 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);