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 edgeIsVarConst(Edge e) {
151 return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
154 static inline Edge constraintNegateIf(Edge e, bool negate) {
155 Edge eret={(Node *)(((uintptr_t)e.node_ptr) ^ negate)};
159 static inline Literal getEdgeVar(Edge e) {
160 int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT);
161 return isNegEdge(e) ? -val : val;
164 static inline bool isProxy(CNFExpr *expr) {
165 return (bool) (((intptr_t) expr) & 1);
168 static inline Literal getProxy(CNFExpr *expr) {
169 return (Literal) (((intptr_t) expr) >> 1);
172 uint hashNode(NodeType type, uint numEdges, Edge * edges);
173 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode);
174 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges);
175 Edge create(CNF *cnf, NodeType type, uint numEdges, Edge * edges);
176 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges);
177 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges);
178 Edge constraintOR2(CNF * cnf, Edge left, Edge right);
179 Edge constraintAND2(CNF * cnf, Edge left, Edge right);
180 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right);
181 Edge constraintIFF(CNF * cnf, Edge left, Edge right);
182 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge);
183 Edge constraintNewVar(CNF *cnf);
184 void countPass(CNF *cnf);
185 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
186 void convertPass(CNF *cnf, bool backtrackLit);
187 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
188 void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp);
189 void produceCNF(CNF * cnf, Edge e);
190 CNFExpr * produceConjunction(CNF * cnf, Edge e);
191 CNFExpr* produceDisjunction(CNF *cnf, Edge e);
192 bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate);
193 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign);
194 CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge);
198 Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
199 Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};