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;
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 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge);
190 Edge constraintNewVar(CNF *cnf);
191 void countPass(CNF *cnf);
192 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
193 void addConstraint(CNF *cnf, Edge constraint);
194 void solveCNF(CNF *cnf);
197 void convertPass(CNF *cnf, bool backtrackLit);
198 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
199 void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp);
200 void produceCNF(CNF * cnf, Edge e);
201 CNFExpr * produceConjunction(CNF * cnf, Edge e);
202 CNFExpr* produceDisjunction(CNF *cnf, Edge e);
203 bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate);
204 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign);
205 CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge);
206 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg);
207 void outputCNF(CNF *cnf, CNFExpr *expr);
209 Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
210 Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};