fix tabbing
[satune.git] / src / Backend / constraint.cc
1 #include "constraint.h"
2 #include <string.h>
3 #include <stdlib.h>
4 #include "inc_solver.h"
5 #include "common.h"
6 #include "qsort.h"
7 /*
8    CNF SAT Conversion Copyright Brian Demsky 2017.
9  */
10
11
12 VectorImpl(Edge, Edge, 16)
13 Edge E_True = {(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
14 Edge E_False = {(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
15 Edge E_BOGUS = {(Node *)0xffff5673};
16 Edge E_NULL = {(Node *)NULL};
17
18 CNF *createCNF() {
19         CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
20         cnf->varcount = 1;
21         cnf->clausecount = 0;
22         cnf->solver = allocIncrementalSolver();
23         cnf->solveTime = 0;
24         cnf->encodeTime = 0;
25         cnf->asize = DEFAULT_CNF_ARRAY_SIZE;
26         cnf->array = (int *) ourmalloc(sizeof(int) * DEFAULT_CNF_ARRAY_SIZE);
27         cnf->unsat = false;
28         return cnf;
29 }
30
31 void deleteCNF(CNF *cnf) {
32         deleteIncrementalSolver(cnf->solver);
33         ourfree(cnf->array);
34         ourfree(cnf);
35 }
36
37 void resetCNF(CNF *cnf) {
38         resetSolver(cnf->solver);
39         cnf->varcount = 1;
40         cnf->clausecount = 0;
41         cnf->solveTime = 0;
42         cnf->encodeTime = 0;
43         cnf->unsat = false;
44 }
45
46 Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
47         Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
48         n->numVars = 0;
49         n->type = type;
50         n->numEdges = numEdges;
51         memcpy(n->edges, edges, sizeof(Edge) * numEdges);
52         return n;
53 }
54
55 Node *allocBaseNode(NodeType type, uint numEdges) {
56         Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
57         n->numVars = 0;
58         n->type = type;
59         n->numEdges = numEdges;
60         return n;
61 }
62
63 Node *allocResizeNode(uint capacity) {
64         Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * capacity);
65         n->numVars = 0;
66         n->numEdges = 0;
67         n->capacity = capacity;
68         return n;
69 }
70
71 Edge cloneEdge(Edge e) {
72         if (edgeIsVarConst(e))
73                 return e;
74         Node *node = getNodePtrFromEdge(e);
75         bool isneg = isNegEdge(e);
76         uint numEdges = node->numEdges;
77         Node *clone = allocBaseNode(node->type, numEdges);
78         for (uint i = 0; i < numEdges; i++) {
79                 clone->edges[i] = cloneEdge(node->edges[i]);
80         }
81         return isneg ? constraintNegate((Edge) {clone}) : (Edge) {clone};
82 }
83
84 void freeEdgeRec(Edge e) {
85         if (edgeIsVarConst(e))
86                 return;
87         Node *node = getNodePtrFromEdge(e);
88         uint numEdges = node->numEdges;
89         for (uint i = 0; i < numEdges; i++) {
90                 freeEdgeRec(node->edges[i]);
91         }
92         ourfree(node);
93 }
94
95 void freeEdge(Edge e) {
96         if (edgeIsVarConst(e))
97                 return;
98         Node *node = getNodePtrFromEdge(e);
99         ourfree(node);
100 }
101
102 void freeEdgesRec(uint numEdges, Edge *earray) {
103         for (uint i = 0; i < numEdges; i++) {
104                 Edge e = earray[i];
105                 freeEdgeRec(e);
106         }
107 }
108
109 void freeEdgeCNF(Edge e) {
110         Node *node = getNodePtrFromEdge(e);
111         uint numEdges = node->numEdges;
112         for (uint i = 0; i < numEdges; i++) {
113                 Edge ec = node->edges[i];
114                 if (!edgeIsVarConst(ec)) {
115                         ourfree(ec.node_ptr);
116                 }
117         }
118         ourfree(node);
119 }
120
121 void addEdgeToResizeNode(Node **node, Edge e) {
122         Node *currnode = *node;
123         if (currnode->capacity == currnode->numEdges) {
124                 Node *newnode = allocResizeNode( currnode->capacity << 1);
125                 newnode->numVars = currnode->numVars;
126                 newnode->numEdges = currnode->numEdges;
127                 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
128                 ourfree(currnode);
129                 *node = newnode;
130                 currnode = newnode;
131         }
132         currnode->edges[currnode->numEdges++] = e;
133 }
134
135 void mergeFreeNodeToResizeNode(Node **node, Node *innode) {
136         Node *currnode = *node;
137         uint currEdges = currnode->numEdges;
138         uint inEdges = innode->numEdges;
139
140         uint newsize = currEdges + inEdges;
141         if (newsize >= currnode->capacity) {
142                 if (newsize < innode->capacity) {
143                         //just swap
144                         innode->numVars = currnode->numVars;
145                         Node *tmp = innode;
146                         innode = currnode;
147                         *node = currnode = tmp;
148                 } else {
149                         Node *newnode = allocResizeNode( newsize << 1);
150                         newnode->numVars = currnode->numVars;
151                         newnode->numEdges = currnode->numEdges;
152                         memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
153                         ourfree(currnode);
154                         *node = newnode;
155                         currnode = newnode;
156                 }
157         } else {
158                 if (inEdges > currEdges && newsize < innode->capacity) {
159                         //just swap
160                         innode->numVars = currnode->numVars;
161                         Node *tmp = innode;
162                         innode = currnode;
163                         *node = currnode = tmp;
164                 }
165         }
166         memcpy(&currnode->edges[currnode->numEdges], innode->edges, innode->numEdges * sizeof(Edge));
167         currnode->numEdges += innode->numEdges;
168         ourfree(innode);
169 }
170
171 void mergeNodeToResizeNode(Node **node, Node *innode) {
172         Node *currnode = *node;
173         uint currEdges = currnode->numEdges;
174         uint inEdges = innode->numEdges;
175         uint newsize = currEdges + inEdges;
176         if (newsize >= currnode->capacity) {
177                 Node *newnode = allocResizeNode( newsize << 1);
178                 newnode->numVars = currnode->numVars;
179                 newnode->numEdges = currnode->numEdges;
180                 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
181                 ourfree(currnode);
182                 *node = newnode;
183                 currnode = newnode;
184         }
185         memcpy(&currnode->edges[currnode->numEdges], innode->edges, inEdges * sizeof(Edge));
186         currnode->numEdges += inEdges;
187 }
188
189 Edge createNode(NodeType type, uint numEdges, Edge *edges) {
190         Edge e = {allocNode(type, numEdges, edges)};
191         return e;
192 }
193
194 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
195         if (numEdges < 200000) {
196                 Edge edgearray[numEdges];
197
198                 for (uint i = 0; i < numEdges; i++) {
199                         edgearray[i] = constraintNegate(edges[i]);
200                 }
201                 Edge eand = constraintAND(cnf, numEdges, edgearray);
202                 return constraintNegate(eand);
203         } else {
204                 Edge *edgearray = (Edge *)ourmalloc(numEdges * sizeof(Edge));
205
206                 for (uint i = 0; i < numEdges; i++) {
207                         edgearray[i] = constraintNegate(edges[i]);
208                 }
209                 Edge eand = constraintAND(cnf, numEdges, edgearray);
210                 ourfree(edgearray);
211                 return constraintNegate(eand);
212         }
213 }
214
215 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
216         Edge lneg = constraintNegate(left);
217         Edge rneg = constraintNegate(right);
218         Edge eand = constraintAND2(cnf, lneg, rneg);
219         return constraintNegate(eand);
220 }
221
222 int comparefunction(const Edge *e1, const Edge *e2) {
223         if (e1->node_ptr == e2->node_ptr)
224                 return 0;
225         if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
226                 return -1;
227         else
228                 return 1;
229 }
230
231 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
232         ASSERT(numEdges != 0);
233
234         bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
235         uint initindex = 0;
236         while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
237                 initindex++;
238
239         uint remainSize = numEdges - initindex;
240
241         if (remainSize == 0)
242                 return E_True;
243         else if (remainSize == 1)
244                 return edges[initindex];
245         else if (equalsEdge(edges[initindex], E_False)) {
246                 freeEdgesRec(numEdges, edges);
247                 return E_False;
248         }
249
250         /** De-duplicate array */
251         uint lowindex = 0;
252         edges[lowindex] = edges[initindex++];
253
254         for (; initindex < numEdges; initindex++) {
255                 Edge e1 = edges[lowindex];
256                 Edge e2 = edges[initindex];
257                 if (sameNodeVarEdge(e1, e2)) {
258                         ASSERT(!isNodeEdge(e1));
259                         if (!sameSignEdge(e1, e2)) {
260                                 freeEdgesRec(lowindex + 1, edges);
261                                 freeEdgesRec(numEdges - initindex, &edges[initindex]);
262                                 return E_False;
263                         }
264                 } else
265                         edges[++lowindex] = edges[initindex];
266         }
267         lowindex++;     //Make lowindex look like size
268
269         if (lowindex == 1)
270                 return edges[0];
271
272         if (lowindex == 2 &&
273                         isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
274                         getNodeType(edges[0]) == NodeType_AND &&
275                         getNodeType(edges[1]) == NodeType_AND &&
276                         getNodeSize(edges[0]) == 2 &&
277                         getNodeSize(edges[1]) == 2) {
278                 Edge *e0edges = getEdgeArray(edges[0]);
279                 Edge *e1edges = getEdgeArray(edges[1]);
280                 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
281                         Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
282                         freeEdge(edges[0]);
283                         freeEdge(edges[1]);
284                         return result;
285                 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
286                         Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
287                         freeEdge(edges[0]);
288                         freeEdge(edges[1]);
289                         return result;
290                 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
291                         Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
292                         freeEdge(edges[0]);
293                         freeEdge(edges[1]);
294                         return result;
295                 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
296                         Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
297                         freeEdge(edges[0]);
298                         freeEdge(edges[1]);
299                         return result;
300                 }
301         }
302
303         return createNode(NodeType_AND, lowindex, edges);
304 }
305
306 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
307         Edge edges[2] = {left, right};
308         return constraintAND(cnf, 2, edges);
309 }
310
311 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
312         Edge array[2];
313         array[0] = left;
314         array[1] = constraintNegate(right);
315         Edge eand = constraintAND(cnf, 2, array);
316         return constraintNegate(eand);
317 }
318
319 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
320         bool negate = !sameSignEdge(left, right);
321         Edge lpos = getNonNeg(left);
322         Edge rpos = getNonNeg(right);
323
324         Edge e;
325         if (equalsEdge(lpos, rpos)) {
326                 freeEdgeRec(left);
327                 freeEdgeRec(right);
328                 e = E_True;
329         } else if (ltEdge(lpos, rpos)) {
330                 Edge edges[] = {lpos, rpos};
331                 e = (edgeIsConst(lpos)) ? rpos : createNode(NodeType_IFF, 2, edges);
332         } else {
333                 Edge edges[] = {rpos, lpos};
334                 e = (edgeIsConst(rpos)) ? lpos : createNode(NodeType_IFF, 2, edges);
335         }
336         if (negate)
337                 e = constraintNegate(e);
338         return e;
339 }
340
341 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
342         if (isNegEdge(cond)) {
343                 cond = constraintNegate(cond);
344                 Edge tmp = thenedge;
345                 thenedge = elseedge;
346                 elseedge = tmp;
347         }
348
349         bool negate = isNegEdge(thenedge);
350         if (negate) {
351                 thenedge = constraintNegate(thenedge);
352                 elseedge = constraintNegate(elseedge);
353         }
354
355         Edge result;
356         if (equalsEdge(cond, E_True)) {
357                 freeEdgeRec(elseedge);
358                 result = thenedge;
359         } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
360                 Edge array[] = {cond, elseedge};
361                 result = constraintOR(cnf,  2, array);
362         } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
363                 result = constraintIMPLIES(cnf, cond, thenedge);
364         } else if (equalsEdge(elseedge, E_False) || equalsEdge(cond, elseedge)) {
365                 Edge array[] = {cond, thenedge};
366                 result = constraintAND(cnf, 2, array);
367         } else if (equalsEdge(thenedge, elseedge)) {
368                 freeEdgeRec(cond);
369                 result = thenedge;
370         } else if (sameNodeOppSign(thenedge, elseedge)) {
371                 if (ltEdge(cond, thenedge)) {
372                         Edge array[] = {cond, thenedge};
373                         result = createNode(NodeType_IFF, 2, array);
374                 } else {
375                         Edge array[] = {thenedge, cond};
376                         result = createNode(NodeType_IFF, 2, array);
377                 }
378         } else {
379                 Edge edges[] = {cond, thenedge, elseedge};
380                 result = createNode(NodeType_ITE, 3, edges);
381         }
382         if (negate)
383                 result = constraintNegate(result);
384         return result;
385 }
386
387 Edge disjoinLit(Edge vec, Edge lit) {
388         Node *nvec = vec.node_ptr;
389         uint nvecedges = nvec->numEdges;
390
391         for (uint i = 0; i < nvecedges; i++) {
392                 Edge ce = nvec->edges[i];
393                 if (!edgeIsVarConst(ce)) {
394                         Node *cne = ce.node_ptr;
395                         addEdgeToResizeNode(&cne, lit);
396                         nvec->edges[i] = (Edge) {cne};
397                 } else {
398                         Node *clause = allocResizeNode(2);
399                         addEdgeToResizeNode(&clause, lit);
400                         addEdgeToResizeNode(&clause, ce);
401                         nvec->edges[i] = (Edge) {clause};
402                 }
403         }
404         nvec->numVars += nvecedges;
405         return vec;
406 }
407
408 Edge disjoinAndFree(CNF *cnf, Edge newvec, Edge cnfform) {
409         Node *nnewvec = newvec.node_ptr;
410         Node *ncnfform = cnfform.node_ptr;
411         uint newvecedges = nnewvec->numEdges;
412         uint cnfedges = ncnfform->numEdges;
413         uint newvecvars = nnewvec->numVars;
414         uint cnfvars = ncnfform->numVars;
415
416         if (cnfedges > 3 ||
417                         ((cnfedges * newvecvars + newvecedges * cnfvars) > (cnfedges + newvecedges + newvecvars + cnfvars))) {
418                 Edge proxyVar = constraintNewVar(cnf);
419                 if (newvecedges > cnfedges) {
420                         outputCNFOR(cnf, newvec, constraintNegate(proxyVar));
421                         freeEdgeCNF(newvec);
422                         return disjoinLit(cnfform, proxyVar);
423                 } else {
424                         outputCNFOR(cnf, cnfform, constraintNegate(proxyVar));
425                         freeEdgeCNF(cnfform);
426                         return disjoinLit(newvec, proxyVar);
427                 }
428         }
429
430
431
432         if (newvecedges == 1 || cnfedges == 1) {
433                 if (cnfedges != 1) {
434                         Node *tmp = nnewvec;
435                         nnewvec = ncnfform;
436                         ncnfform = tmp;
437                         newvecedges = cnfedges;
438                         cnfedges = 1;
439                 }
440                 Edge e = ncnfform->edges[0];
441                 if (!edgeIsVarConst(e)) {
442                         Node *n = e.node_ptr;
443                         for (uint i = 0; i < newvecedges; i++) {
444                                 Edge ce = nnewvec->edges[i];
445                                 if (isNodeEdge(ce)) {
446                                         Node *cne = ce.node_ptr;
447                                         mergeNodeToResizeNode(&cne, n);
448                                         nnewvec->edges[i] = (Edge) {cne};
449                                 } else {
450                                         Node *clause = allocResizeNode(n->numEdges + 1);
451                                         mergeNodeToResizeNode(&clause, n);
452                                         addEdgeToResizeNode(&clause, ce);
453                                         nnewvec->edges[i] = (Edge) {clause};
454                                 }
455                         }
456                         nnewvec->numVars += newvecedges * n->numVars;
457                 } else {
458                         for (uint i = 0; i < newvecedges; i++) {
459                                 Edge ce = nnewvec->edges[i];
460                                 if (!edgeIsVarConst(ce)) {
461                                         Node *cne = ce.node_ptr;
462                                         addEdgeToResizeNode(&cne, e);
463                                         nnewvec->edges[i] = (Edge) {cne};
464                                 } else {
465                                         Node *clause = allocResizeNode(2);
466                                         addEdgeToResizeNode(&clause, e);
467                                         addEdgeToResizeNode(&clause, ce);
468                                         nnewvec->edges[i] = (Edge) {clause};
469                                 }
470                         }
471                         nnewvec->numVars += newvecedges;
472                 }
473                 freeEdgeCNF((Edge) {ncnfform});
474                 return (Edge) {nnewvec};
475         }
476
477         Node *result = allocResizeNode(1);
478
479         for (uint i = 0; i < newvecedges; i++) {
480                 Edge nedge = nnewvec->edges[i];
481                 uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1;
482                 for (uint j = 0; j < cnfedges; j++) {
483                         Edge cedge = ncnfform->edges[j];
484                         uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
485                         if (equalsEdge(cedge, nedge)) {
486                                 addEdgeToResizeNode(&result, cedge);
487                                 result->numVars += cSize;
488                         } else if (!sameNodeOppSign(nedge, cedge)) {
489                                 Node *clause = allocResizeNode(cSize + nSize);
490                                 if (isNodeEdge(nedge)) {
491                                         mergeNodeToResizeNode(&clause, nedge.node_ptr);
492                                 } else {
493                                         addEdgeToResizeNode(&clause, nedge);
494                                 }
495                                 if (isNodeEdge(cedge)) {
496                                         mergeNodeToResizeNode(&clause, cedge.node_ptr);
497                                 } else {
498                                         addEdgeToResizeNode(&clause, cedge);
499                                 }
500                                 addEdgeToResizeNode(&result, (Edge) {clause});
501                                 result->numVars += clause->numEdges;
502                         }
503                         //otherwise skip
504                 }
505         }
506         freeEdgeCNF(newvec);
507         freeEdgeCNF(cnfform);
508         return (Edge) {result};
509 }
510
511 Edge simplifyCNF(CNF *cnf, Edge input) {
512         if (edgeIsVarConst(input)) {
513                 Node *newvec = allocResizeNode(1);
514                 addEdgeToResizeNode(&newvec, input);
515                 newvec->numVars = 1;
516                 return (Edge) {newvec};
517         }
518         bool negated = isNegEdge(input);
519         Node *node = getNodePtrFromEdge(input);
520         NodeType type = node->type;
521         if (!negated) {
522                 if (type == NodeType_AND) {
523                         //AND case
524                         Node *newvec = allocResizeNode(node->numEdges);
525                         uint numEdges = node->numEdges;
526                         for (uint i = 0; i < numEdges; i++) {
527                                 Edge e = simplifyCNF(cnf, node->edges[i]);
528                                 uint enumvars = e.node_ptr->numVars;
529                                 mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
530                                 newvec->numVars += enumvars;
531                         }
532                         return (Edge) {newvec};
533                 } else {
534                         Edge cond = node->edges[0];
535                         Edge thenedge = node->edges[1];
536                         Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
537                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
538                         Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
539                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
540                         Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
541                         Edge thencnf = simplifyCNF(cnf, thencons);
542                         Edge elsecnf = simplifyCNF(cnf, elsecons);
543                         //free temporary nodes
544                         ourfree(getNodePtrFromEdge(thencons));
545                         ourfree(getNodePtrFromEdge(elsecons));
546                         Node *result = thencnf.node_ptr;
547                         uint elsenumvars = elsecnf.node_ptr->numVars;
548                         mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
549                         result->numVars += elsenumvars;
550                         return (Edge) {result};
551                 }
552         } else {
553                 if (type == NodeType_AND) {
554                         //OR Case
555                         uint numEdges = node->numEdges;
556
557                         Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
558                         for (uint i = 1; i < numEdges; i++) {
559                                 Edge e = node->edges[i];
560                                 Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
561                                 newvec = disjoinAndFree(cnf, newvec, cnfform);
562                         }
563                         return newvec;
564                 } else {
565                         Edge cond = node->edges[0];
566                         Edge thenedge = node->edges[1];
567                         Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
568
569
570                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
571                         Edge thencons = createNode(NodeType_AND, 2, thenedges);
572                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
573                         Edge elsecons = createNode(NodeType_AND, 2, elseedges);
574
575                         Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
576                         Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
577                         Edge result = simplifyCNF(cnf, combined);
578                         //free temporary nodes
579                         ourfree(getNodePtrFromEdge(thencons));
580                         ourfree(getNodePtrFromEdge(elsecons));
581                         ourfree(getNodePtrFromEdge(combined));
582                         return result;
583                 }
584         }
585 }
586
587 void addClause(CNF *cnf, uint numliterals, int *literals) {
588         cnf->clausecount++;
589         addArrayClauseLiteral(cnf->solver, numliterals, literals);
590 }
591
592 void freezeVariable(CNF *cnf, Edge e) {
593         int literal = getEdgeVar(e);
594         freeze(cnf->solver, literal);
595 }
596
597 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
598         Node *andNode = cnfform.node_ptr;
599         int orvar = getEdgeVar(eorvar);
600         ASSERT(orvar != 0);
601         uint numEdges = andNode->numEdges;
602         for (uint i = 0; i < numEdges; i++) {
603                 Edge e = andNode->edges[i];
604                 if (edgeIsVarConst(e)) {
605                         int array[2] = {getEdgeVar(e), orvar};
606                         ASSERT(array[0] != 0);
607                         addClause(cnf, 2, array);
608                 } else {
609                         Node *clause = e.node_ptr;
610                         uint cnumEdges = clause->numEdges + 1;
611                         if (cnumEdges > cnf->asize) {
612                                 cnf->asize = cnumEdges << 1;
613                                 ourfree(cnf->array);
614                                 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
615                         }
616                         int *array = cnf->array;
617                         for (uint j = 0; j < (cnumEdges - 1); j++) {
618                                 array[j] = getEdgeVar(clause->edges[j]);
619                                 ASSERT(array[j] != 0);
620                         }
621                         array[cnumEdges - 1] = orvar;
622                         addClause(cnf, cnumEdges, array);
623                 }
624         }
625 }
626
627 void outputCNF(CNF *cnf, Edge cnfform) {
628         Node *andNode = cnfform.node_ptr;
629         uint numEdges = andNode->numEdges;
630         for (uint i = 0; i < numEdges; i++) {
631                 Edge e = andNode->edges[i];
632                 if (edgeIsVarConst(e)) {
633                         int array[1] = {getEdgeVar(e)};
634                         ASSERT(array[0] != 0);
635                         addClause(cnf, 1, array);
636                 } else {
637                         Node *clause = e.node_ptr;
638                         uint cnumEdges = clause->numEdges;
639                         if (cnumEdges > cnf->asize) {
640                                 cnf->asize = cnumEdges << 1;
641                                 ourfree(cnf->array);
642                                 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
643                         }
644                         int *array = cnf->array;
645                         for (uint j = 0; j < cnumEdges; j++) {
646                                 array[j] = getEdgeVar(clause->edges[j]);
647                                 ASSERT(array[j] != 0);
648                         }
649                         addClause(cnf, cnumEdges, array);
650                 }
651         }
652 }
653
654 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
655         ASSERT(p != P_UNDEFINED);
656         if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
657                 // proxy => expression
658                 Edge cnfexpr = simplifyCNF(cnf, expression);
659                 if (p == P_TRUE)
660                         freeEdgeRec(expression);
661                 outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
662                 freeEdgeCNF(cnfexpr);
663         }
664         if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
665                 // expression => proxy
666                 Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
667                 freeEdgeRec(expression);
668                 outputCNFOR(cnf, cnfnegexpr, proxy);
669                 freeEdgeCNF(cnfnegexpr);
670         }
671 }
672
673 void addConstraintCNF(CNF *cnf, Edge constraint) {
674         if (equalsEdge(constraint, E_True)) {
675                 return;
676         } else if (equalsEdge(constraint, E_False)) {
677                 cnf->unsat = true;
678                 return;
679         }
680         if (cnf->unsat) {
681                 freeEdgeRec(constraint);
682                 return;
683         }
684
685 #if 0
686         model_print("****SATC_ADDING NEW Constraint*****\n");
687         printCNF(constraint);
688         model_print("\n******************************\n");
689 #endif
690
691         Edge cnfform = simplifyCNF(cnf, constraint);
692         freeEdgeRec(constraint);
693         outputCNF(cnf, cnfform);
694         freeEdgeCNF(cnfform);
695 }
696
697 Edge constraintNewVar(CNF *cnf) {
698         uint varnum = cnf->varcount++;
699         Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
700         return e;
701 }
702
703 int solveCNF(CNF *cnf) {
704         long long startSolve = getTimeNano();
705         model_print("#Clauses = %u\t#Vars = %u\n", cnf->clausecount, cnf->varcount);
706         int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
707         long long finishTime = getTimeNano();
708         model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
709         cnf->solveTime = finishTime - startSolve;
710         model_print("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0);
711         return result;
712 }
713
714 bool getValueCNF(CNF *cnf, Edge var) {
715         Literal l = getEdgeVar(var);
716         bool isneg = (l < 0);
717         l = abs(l);
718         return isneg ^ getValueSolver(cnf->solver, l);
719 }
720
721 void printCNF(Edge e) {
722         if (edgeIsVarConst(e)) {
723                 Literal l = getEdgeVar(e);
724                 model_print ("%d", l);
725                 return;
726         }
727         bool isNeg = isNegEdge(e);
728         if (edgeIsConst(e)) {
729                 if (isNeg)
730                         model_print("T");
731                 else
732                         model_print("F");
733                 return;
734         }
735         Node *n = getNodePtrFromEdge(e);
736         if (isNeg) {
737                 //Pretty print things that are equivalent to OR's
738                 if (getNodeType(e) == NodeType_AND) {
739                         model_print("or(");
740                         for (uint i = 0; i < n->numEdges; i++) {
741                                 Edge e = n->edges[i];
742                                 if (i != 0)
743                                         model_print(" ");
744                                 printCNF(constraintNegate(e));
745                         }
746                         model_print(")");
747                         return;
748                 }
749
750                 model_print("!");
751         }
752         switch (getNodeType(e)) {
753         case NodeType_AND:
754                 model_print("and");
755                 break;
756         case NodeType_ITE:
757                 model_print("ite");
758                 break;
759         case NodeType_IFF:
760                 model_print("iff");
761                 break;
762         }
763         model_print("(");
764         for (uint i = 0; i < n->numEdges; i++) {
765                 Edge e = n->edges[i];
766                 if (i != 0)
767                         model_print(" ");
768                 printCNF(e);
769         }
770         model_print(")");
771 }
772
773 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
774         Edge carray[numvars];
775         for (uint j = 0; j < numvars; j++) {
776                 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
777                 value = value >> 1;
778         }
779
780         return constraintAND(cnf, numvars, carray);
781 }
782
783 /** Generates a constraint to ensure that all encodings are less than value */
784 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
785         Edge orarray[numvars];
786         Edge andarray[numvars];
787         uint andi = 0;
788
789         while (true) {
790                 uint val = value;
791                 uint ori = 0;
792                 for (uint j = 0; j < numvars; j++) {
793                         if ((val & 1) == 1)
794                                 orarray[ori++] = constraintNegate(vars[j]);
795                         val = val >> 1;
796                 }
797                 //no ones to flip, so bail now...
798                 if (ori == 0) {
799                         return constraintAND(cnf, andi, andarray);
800                 }
801                 andarray[andi++] = constraintOR(cnf, ori, orarray);
802
803                 value = value + (1 << (__builtin_ctz(value)));
804                 //flip the last one
805         }
806 }
807
808 void generateAddConstraint(CNF *cnf, uint nSum, Edge *sum, uint nVar1, Edge *var1, uint nVar2, Edge *var2) {
809         //TO WRITE....
810 }
811
812 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
813         if (numvars == 0)
814                 return E_True;
815         Edge array[numvars];
816         for (uint i = 0; i < numvars; i++) {
817                 array[i] = constraintIFF(cnf, var1[i], var2[i]);
818         }
819         return constraintAND(cnf, numvars, array);
820 }
821
822 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
823         if (numvars == 0 )
824                 return E_False;
825         Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
826         for (uint i = 1; i < numvars; i++) {
827                 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
828                 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
829                 result = constraintOR2(cnf, lt, eq);
830         }
831         return result;
832 }
833
834 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
835         if (numvars == 0 )
836                 return E_True;
837         Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
838         for (uint i = 1; i < numvars; i++) {
839                 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
840                 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
841                 result = constraintOR2(cnf, lt, eq);
842         }
843         return result;
844 }