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;
68 typedef struct CNF CNF;
71 typedef struct CNFExpr CNFExpr;
73 static inline bool getExpanded(Node *n, int isNegated) {
74 return n->flags.wasExpanded & (1 << isNegated);
77 static inline void setExpanded(Node *n, int isNegated) {
78 n->flags.wasExpanded |= (1 << isNegated);
81 static inline Edge constraintNegate(Edge e) {
82 Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
86 static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
87 return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~(uintptr_t) NEGATE_EDGE));
90 static inline bool sameSignEdge(Edge e1, Edge e2) {
91 return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
94 static inline bool sameNodeOppSign(Edge e1, Edge e2) {
95 return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
98 static inline bool isNegEdge(Edge e) {
99 return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
102 static inline bool isPosEdge(Edge e) {
103 return !(((uintptr_t)e.node_ptr) & NEGATE_EDGE);
106 static inline bool isNodeEdge(Edge e) {
107 return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
110 static inline bool isNegNodeEdge(Edge e) {
111 return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
114 static inline Node *getNodePtrFromEdge(Edge e) {
115 return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
118 static inline NodeType getNodeType(Edge e) {
119 Node *n = getNodePtrFromEdge(e);
120 return n->flags.type;
123 static inline bool equalsEdge(Edge e1, Edge e2) {
124 return e1.node_ptr == e2.node_ptr;
127 static inline bool ltEdge(Edge e1, Edge e2) {
128 return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr;
131 static inline uint getNodeSize(Edge e) {
132 Node *n = getNodePtrFromEdge(e);
136 static inline Edge *getEdgeArray(Edge e) {
137 Node *n = getNodePtrFromEdge(e);
141 static inline Edge getNonNeg(Edge e) {
142 Edge enew = {(Node *)(((uintptr_t)e.node_ptr) & (~((uintptr_t)NEGATE_EDGE)))};
146 static inline bool edgeIsConst(Edge e) {
147 return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
150 static inline bool edgeIsNull(Edge e) {
151 return e.node_ptr == NULL;
154 static inline bool edgeIsVarConst(Edge e) {
155 return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
158 static inline Edge constraintNegateIf(Edge e, bool negate) {
159 Edge eret = {(Node *)(((uintptr_t)e.node_ptr) ^ negate)};
163 static inline Literal getEdgeVar(Edge e) {
164 int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT);
165 return isNegEdge(e) ? -val : val;
168 static inline bool isProxy(CNFExpr *expr) {
169 return (bool) (((intptr_t) expr) & 1);
172 static inline Literal getProxy(CNFExpr *expr) {
173 return (Literal) (((intptr_t) expr) >> 1);
177 void deleteCNF(CNF *cnf);
179 uint hashNode(NodeType type, uint numEdges, Edge *edges);
180 Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashCode);
181 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges);
182 Edge create(CNF *cnf, NodeType type, uint numEdges, Edge *edges);
183 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges);
184 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges);
185 Edge constraintOR2(CNF *cnf, Edge left, Edge right);
186 Edge constraintAND2(CNF *cnf, Edge left, Edge right);
187 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right);
188 Edge constraintIFF(CNF *cnf, Edge left, Edge right);
189 static inline Edge constraintXOR(CNF *cnf, Edge left, Edge right) {return constraintNegate(constraintIFF(cnf, left,right));}
190 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge);
191 Edge constraintNewVar(CNF *cnf);
192 void countPass(CNF *cnf);
193 void countConstraint(CNF *cnf, VectorEdge *stack, Edge e);
194 void addConstraintCNF(CNF *cnf, Edge constraint);
195 int solveCNF(CNF *cnf);
196 bool getValueCNF(CNF *cnf, Edge var);
197 void printCNF(Edge e);
199 void convertPass(CNF *cnf, bool backtrackLit);
200 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
201 void constrainCNF(CNF *cnf, Literal l, CNFExpr *exp);
202 void produceCNF(CNF *cnf, Edge e);
203 CNFExpr *produceConjunction(CNF *cnf, Edge e);
204 CNFExpr *produceDisjunction(CNF *cnf, Edge e);
205 bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate);
206 void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign);
207 CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge);
208 Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg);
209 void outputCNF(CNF *cnf, CNFExpr *expr);
211 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
212 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
213 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
214 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
215 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);