Adding timeout for SATTune
[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         Edge edgearray[numEdges];
196
197         for (uint i = 0; i < numEdges; i++) {
198                 edgearray[i] = constraintNegate(edges[i]);
199         }
200         Edge eand = constraintAND(cnf, numEdges, edgearray);
201         return constraintNegate(eand);
202 }
203
204 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
205         Edge lneg = constraintNegate(left);
206         Edge rneg = constraintNegate(right);
207         Edge eand = constraintAND2(cnf, lneg, rneg);
208         return constraintNegate(eand);
209 }
210
211 int comparefunction(const Edge *e1, const Edge *e2) {
212         if (e1->node_ptr == e2->node_ptr)
213                 return 0;
214         if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
215                 return -1;
216         else
217                 return 1;
218 }
219
220 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
221         ASSERT(numEdges != 0);
222
223         bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
224         uint initindex = 0;
225         while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
226                 initindex++;
227
228         uint remainSize = numEdges - initindex;
229
230         if (remainSize == 0)
231                 return E_True;
232         else if (remainSize == 1)
233                 return edges[initindex];
234         else if (equalsEdge(edges[initindex], E_False)) {
235                 freeEdgesRec(numEdges, edges);
236                 return E_False;
237         }
238
239         /** De-duplicate array */
240         uint lowindex = 0;
241         edges[lowindex] = edges[initindex++];
242
243         for (; initindex < numEdges; initindex++) {
244                 Edge e1 = edges[lowindex];
245                 Edge e2 = edges[initindex];
246                 if (sameNodeVarEdge(e1, e2)) {
247                         ASSERT(!isNodeEdge(e1));
248                         if (!sameSignEdge(e1, e2)) {
249                                 freeEdgesRec(lowindex + 1, edges);
250                                 freeEdgesRec(numEdges - initindex, &edges[initindex]);
251                                 return E_False;
252                         }
253                 } else
254                         edges[++lowindex] = edges[initindex];
255         }
256         lowindex++;     //Make lowindex look like size
257
258         if (lowindex == 1)
259                 return edges[0];
260
261         if (lowindex == 2 &&
262                         isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
263                         getNodeType(edges[0]) == NodeType_AND &&
264                         getNodeType(edges[1]) == NodeType_AND &&
265                         getNodeSize(edges[0]) == 2 &&
266                         getNodeSize(edges[1]) == 2) {
267                 Edge *e0edges = getEdgeArray(edges[0]);
268                 Edge *e1edges = getEdgeArray(edges[1]);
269                 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
270                         Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
271                         freeEdge(edges[0]);
272                         freeEdge(edges[1]);
273                         return result;
274                 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
275                         Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
276                         freeEdge(edges[0]);
277                         freeEdge(edges[1]);
278                         return result;
279                 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
280                         Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
281                         freeEdge(edges[0]);
282                         freeEdge(edges[1]);
283                         return result;
284                 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
285                         Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
286                         freeEdge(edges[0]);
287                         freeEdge(edges[1]);
288                         return result;
289                 }
290         }
291
292         return createNode(NodeType_AND, lowindex, edges);
293 }
294
295 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
296         Edge edges[2] = {left, right};
297         return constraintAND(cnf, 2, edges);
298 }
299
300 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
301         Edge array[2];
302         array[0] = left;
303         array[1] = constraintNegate(right);
304         Edge eand = constraintAND(cnf, 2, array);
305         return constraintNegate(eand);
306 }
307
308 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
309         bool negate = !sameSignEdge(left, right);
310         Edge lpos = getNonNeg(left);
311         Edge rpos = getNonNeg(right);
312
313         Edge e;
314         if (equalsEdge(lpos, rpos)) {
315                 freeEdgeRec(left);
316                 freeEdgeRec(right);
317                 e = E_True;
318         } else if (ltEdge(lpos, rpos)) {
319                 Edge edges[] = {lpos, rpos};
320                 e = (edgeIsConst(lpos)) ? rpos : createNode(NodeType_IFF, 2, edges);
321         } else {
322                 Edge edges[] = {rpos, lpos};
323                 e = (edgeIsConst(rpos)) ? lpos : createNode(NodeType_IFF, 2, edges);
324         }
325         if (negate)
326                 e = constraintNegate(e);
327         return e;
328 }
329
330 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
331         if (isNegEdge(cond)) {
332                 cond = constraintNegate(cond);
333                 Edge tmp = thenedge;
334                 thenedge = elseedge;
335                 elseedge = tmp;
336         }
337
338         bool negate = isNegEdge(thenedge);
339         if (negate) {
340                 thenedge = constraintNegate(thenedge);
341                 elseedge = constraintNegate(elseedge);
342         }
343
344         Edge result;
345         if (equalsEdge(cond, E_True)) {
346                 freeEdgeRec(elseedge);
347                 result = thenedge;
348         } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
349                 Edge array[] = {cond, elseedge};
350                 result = constraintOR(cnf,  2, array);
351         } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
352                 result = constraintIMPLIES(cnf, cond, thenedge);
353         } else if (equalsEdge(elseedge, E_False) || equalsEdge(cond, elseedge)) {
354                 Edge array[] = {cond, thenedge};
355                 result = constraintAND(cnf, 2, array);
356         } else if (equalsEdge(thenedge, elseedge)) {
357                 freeEdgeRec(cond);
358                 result = thenedge;
359         } else if (sameNodeOppSign(thenedge, elseedge)) {
360                 if (ltEdge(cond, thenedge)) {
361                         Edge array[] = {cond, thenedge};
362                         result = createNode(NodeType_IFF, 2, array);
363                 } else {
364                         Edge array[] = {thenedge, cond};
365                         result = createNode(NodeType_IFF, 2, array);
366                 }
367         } else {
368                 Edge edges[] = {cond, thenedge, elseedge};
369                 result = createNode(NodeType_ITE, 3, edges);
370         }
371         if (negate)
372                 result = constraintNegate(result);
373         return result;
374 }
375
376 Edge disjoinLit(Edge vec, Edge lit) {
377         Node *nvec = vec.node_ptr;
378         uint nvecedges = nvec->numEdges;
379
380         for (uint i = 0; i < nvecedges; i++) {
381                 Edge ce = nvec->edges[i];
382                 if (!edgeIsVarConst(ce)) {
383                         Node *cne = ce.node_ptr;
384                         addEdgeToResizeNode(&cne, lit);
385                         nvec->edges[i] = (Edge) {cne};
386                 } else {
387                         Node *clause = allocResizeNode(2);
388                         addEdgeToResizeNode(&clause, lit);
389                         addEdgeToResizeNode(&clause, ce);
390                         nvec->edges[i] = (Edge) {clause};
391                 }
392         }
393         nvec->numVars += nvecedges;
394         return vec;
395 }
396
397 Edge disjoinAndFree(CNF *cnf, Edge newvec, Edge cnfform) {
398         Node *nnewvec = newvec.node_ptr;
399         Node *ncnfform = cnfform.node_ptr;
400         uint newvecedges = nnewvec->numEdges;
401         uint cnfedges = ncnfform->numEdges;
402         uint newvecvars = nnewvec->numVars;
403         uint cnfvars = ncnfform->numVars;
404
405         if (cnfedges > 3 ||
406                         ((cnfedges * newvecvars + newvecedges * cnfvars) > (cnfedges + newvecedges + newvecvars + cnfvars))) {
407                 Edge proxyVar = constraintNewVar(cnf);
408                 if (newvecedges > cnfedges) {
409                         outputCNFOR(cnf, newvec, constraintNegate(proxyVar));
410                         freeEdgeCNF(newvec);
411                         return disjoinLit(cnfform, proxyVar);
412                 } else {
413                         outputCNFOR(cnf, cnfform, constraintNegate(proxyVar));
414                         freeEdgeCNF(cnfform);
415                         return disjoinLit(newvec, proxyVar);
416                 }
417         }
418
419
420
421         if (newvecedges == 1 || cnfedges == 1) {
422                 if (cnfedges != 1) {
423                         Node *tmp = nnewvec;
424                         nnewvec = ncnfform;
425                         ncnfform = tmp;
426                         newvecedges = cnfedges;
427                         cnfedges = 1;
428                 }
429                 Edge e = ncnfform->edges[0];
430                 if (!edgeIsVarConst(e)) {
431                         Node *n = e.node_ptr;
432                         for (uint i = 0; i < newvecedges; i++) {
433                                 Edge ce = nnewvec->edges[i];
434                                 if (isNodeEdge(ce)) {
435                                         Node *cne = ce.node_ptr;
436                                         mergeNodeToResizeNode(&cne, n);
437                                         nnewvec->edges[i] = (Edge) {cne};
438                                 } else {
439                                         Node *clause = allocResizeNode(n->numEdges + 1);
440                                         mergeNodeToResizeNode(&clause, n);
441                                         addEdgeToResizeNode(&clause, ce);
442                                         nnewvec->edges[i] = (Edge) {clause};
443                                 }
444                         }
445                         nnewvec->numVars += newvecedges * n->numVars;
446                 } else {
447                         for (uint i = 0; i < newvecedges; i++) {
448                                 Edge ce = nnewvec->edges[i];
449                                 if (!edgeIsVarConst(ce)) {
450                                         Node *cne = ce.node_ptr;
451                                         addEdgeToResizeNode(&cne, e);
452                                         nnewvec->edges[i] = (Edge) {cne};
453                                 } else {
454                                         Node *clause = allocResizeNode(2);
455                                         addEdgeToResizeNode(&clause, e);
456                                         addEdgeToResizeNode(&clause, ce);
457                                         nnewvec->edges[i] = (Edge) {clause};
458                                 }
459                         }
460                         nnewvec->numVars += newvecedges;
461                 }
462                 freeEdgeCNF((Edge) {ncnfform});
463                 return (Edge) {nnewvec};
464         }
465
466         Node *result = allocResizeNode(1);
467
468         for (uint i = 0; i < newvecedges; i++) {
469                 Edge nedge = nnewvec->edges[i];
470                 uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1;
471                 for (uint j = 0; j < cnfedges; j++) {
472                         Edge cedge = ncnfform->edges[j];
473                         uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
474                         if (equalsEdge(cedge, nedge)) {
475                                 addEdgeToResizeNode(&result, cedge);
476                                 result->numVars += cSize;
477                         } else if (!sameNodeOppSign(nedge, cedge)) {
478                                 Node *clause = allocResizeNode(cSize + nSize);
479                                 if (isNodeEdge(nedge)) {
480                                         mergeNodeToResizeNode(&clause, nedge.node_ptr);
481                                 } else {
482                                         addEdgeToResizeNode(&clause, nedge);
483                                 }
484                                 if (isNodeEdge(cedge)) {
485                                         mergeNodeToResizeNode(&clause, cedge.node_ptr);
486                                 } else {
487                                         addEdgeToResizeNode(&clause, cedge);
488                                 }
489                                 addEdgeToResizeNode(&result, (Edge) {clause});
490                                 result->numVars += clause->numEdges;
491                         }
492                         //otherwise skip
493                 }
494         }
495         freeEdgeCNF(newvec);
496         freeEdgeCNF(cnfform);
497         return (Edge) {result};
498 }
499
500 Edge simplifyCNF(CNF *cnf, Edge input) {
501         if (edgeIsVarConst(input)) {
502                 Node *newvec = allocResizeNode(1);
503                 addEdgeToResizeNode(&newvec, input);
504                 newvec->numVars = 1;
505                 return (Edge) {newvec};
506         }
507         bool negated = isNegEdge(input);
508         Node *node = getNodePtrFromEdge(input);
509         NodeType type = node->type;
510         if (!negated) {
511                 if (type == NodeType_AND) {
512                         //AND case
513                         Node *newvec = allocResizeNode(node->numEdges);
514                         uint numEdges = node->numEdges;
515                         for (uint i = 0; i < numEdges; i++) {
516                                 Edge e = simplifyCNF(cnf, node->edges[i]);
517                                 uint enumvars = e.node_ptr->numVars;
518                                 mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
519                                 newvec->numVars += enumvars;
520                         }
521                         return (Edge) {newvec};
522                 } else {
523                         Edge cond = node->edges[0];
524                         Edge thenedge = node->edges[1];
525                         Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
526                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
527                         Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
528                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
529                         Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
530                         Edge thencnf = simplifyCNF(cnf, thencons);
531                         Edge elsecnf = simplifyCNF(cnf, elsecons);
532                         //free temporary nodes
533                         ourfree(getNodePtrFromEdge(thencons));
534                         ourfree(getNodePtrFromEdge(elsecons));
535                         Node *result = thencnf.node_ptr;
536                         uint elsenumvars = elsecnf.node_ptr->numVars;
537                         mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
538                         result->numVars += elsenumvars;
539                         return (Edge) {result};
540                 }
541         } else {
542                 if (type == NodeType_AND) {
543                         //OR Case
544                         uint numEdges = node->numEdges;
545
546                         Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
547                         for (uint i = 1; i < numEdges; i++) {
548                                 Edge e = node->edges[i];
549                                 Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
550                                 newvec = disjoinAndFree(cnf, newvec, cnfform);
551                         }
552                         return newvec;
553                 } else {
554                         Edge cond = node->edges[0];
555                         Edge thenedge = node->edges[1];
556                         Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
557
558
559                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
560                         Edge thencons = createNode(NodeType_AND, 2, thenedges);
561                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
562                         Edge elsecons = createNode(NodeType_AND, 2, elseedges);
563
564                         Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
565                         Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
566                         Edge result = simplifyCNF(cnf, combined);
567                         //free temporary nodes
568                         ourfree(getNodePtrFromEdge(thencons));
569                         ourfree(getNodePtrFromEdge(elsecons));
570                         ourfree(getNodePtrFromEdge(combined));
571                         return result;
572                 }
573         }
574 }
575
576 void addClause(CNF *cnf, uint numliterals, int *literals) {
577         cnf->clausecount++;
578         addArrayClauseLiteral(cnf->solver, numliterals, literals);
579 }
580
581 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
582         Node *andNode = cnfform.node_ptr;
583         int orvar = getEdgeVar(eorvar);
584         ASSERT(orvar != 0);
585         uint numEdges = andNode->numEdges;
586         for (uint i = 0; i < numEdges; i++) {
587                 Edge e = andNode->edges[i];
588                 if (edgeIsVarConst(e)) {
589                         int array[2] = {getEdgeVar(e), orvar};
590                         ASSERT(array[0] != 0);
591                         addClause(cnf, 2, array);
592                 } else {
593                         Node *clause = e.node_ptr;
594                         uint cnumEdges = clause->numEdges + 1;
595                         if (cnumEdges > cnf->asize) {
596                                 cnf->asize = cnumEdges << 1;
597                                 ourfree(cnf->array);
598                                 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
599                         }
600                         int *array = cnf->array;
601                         for (uint j = 0; j < (cnumEdges - 1); j++) {
602                                 array[j] = getEdgeVar(clause->edges[j]);
603                                 ASSERT(array[j] != 0);
604                         }
605                         array[cnumEdges - 1] = orvar;
606                         addClause(cnf, cnumEdges, array);
607                 }
608         }
609 }
610
611 void outputCNF(CNF *cnf, Edge cnfform) {
612         Node *andNode = cnfform.node_ptr;
613         uint numEdges = andNode->numEdges;
614         for (uint i = 0; i < numEdges; i++) {
615                 Edge e = andNode->edges[i];
616                 if (edgeIsVarConst(e)) {
617                         int array[1] = {getEdgeVar(e)};
618                         ASSERT(array[0] != 0);
619                         addClause(cnf, 1, array);
620                 } else {
621                         Node *clause = e.node_ptr;
622                         uint cnumEdges = clause->numEdges;
623                         if (cnumEdges > cnf->asize) {
624                                 cnf->asize = cnumEdges << 1;
625                                 ourfree(cnf->array);
626                                 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
627                         }
628                         int *array = cnf->array;
629                         for (uint j = 0; j < cnumEdges; j++) {
630                                 array[j] = getEdgeVar(clause->edges[j]);
631                                 ASSERT(array[j] != 0);
632                         }
633                         addClause(cnf, cnumEdges, array);
634                 }
635         }
636 }
637
638 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
639         ASSERT(p != P_UNDEFINED);
640         if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
641                 // proxy => expression
642                 Edge cnfexpr = simplifyCNF(cnf, expression);
643                 if (p == P_TRUE)
644                         freeEdgeRec(expression);
645                 outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
646                 freeEdgeCNF(cnfexpr);
647         }
648         if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
649                 // expression => proxy
650                 Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
651                 freeEdgeRec(expression);
652                 outputCNFOR(cnf, cnfnegexpr, proxy);
653                 freeEdgeCNF(cnfnegexpr);
654         }
655 }
656
657 void addConstraintCNF(CNF *cnf, Edge constraint) {
658         if (equalsEdge(constraint, E_True)) {
659                 return;
660         } else if (equalsEdge(constraint, E_False)) {
661                 cnf->unsat = true;
662                 return;
663         }
664         if (cnf->unsat) {
665                 freeEdgeRec(constraint);
666                 return;
667         }
668
669 #if 0
670         model_print("****SATC_ADDING NEW Constraint*****\n");
671         printCNF(constraint);
672         model_print("\n******************************\n");
673 #endif
674
675         Edge cnfform = simplifyCNF(cnf, constraint);
676         freeEdgeRec(constraint);
677         outputCNF(cnf, cnfform);
678         freeEdgeCNF(cnfform);
679 }
680
681 Edge constraintNewVar(CNF *cnf) {
682         uint varnum = cnf->varcount++;
683         Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
684         return e;
685 }
686
687 int solveCNF(CNF *cnf) {
688         long long startTime = getTimeNano();
689         finishedClauses(cnf->solver);
690         long long startSolve = getTimeNano();
691         model_print("#Clauses = %u\t#Vars = %u\n", cnf->clausecount, cnf->varcount);
692         int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
693         long long finishTime = getTimeNano();
694         cnf->encodeTime = startSolve - startTime;
695         model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
696         cnf->solveTime = finishTime - startSolve;
697         model_print("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0);
698         return result;
699 }
700
701 bool getValueCNF(CNF *cnf, Edge var) {
702         Literal l = getEdgeVar(var);
703         bool isneg = (l < 0);
704         l = abs(l);
705         return isneg ^ getValueSolver(cnf->solver, l);
706 }
707
708 void printCNF(Edge e) {
709         if (edgeIsVarConst(e)) {
710                 Literal l = getEdgeVar(e);
711                 model_print ("%d", l);
712                 return;
713         }
714         bool isNeg = isNegEdge(e);
715         if (edgeIsConst(e)) {
716                 if (isNeg)
717                         model_print("T");
718                 else
719                         model_print("F");
720                 return;
721         }
722         Node *n = getNodePtrFromEdge(e);
723         if (isNeg) {
724                 //Pretty print things that are equivalent to OR's
725                 if (getNodeType(e) == NodeType_AND) {
726                         model_print("or(");
727                         for (uint i = 0; i < n->numEdges; i++) {
728                                 Edge e = n->edges[i];
729                                 if (i != 0)
730                                         model_print(" ");
731                                 printCNF(constraintNegate(e));
732                         }
733                         model_print(")");
734                         return;
735                 }
736
737                 model_print("!");
738         }
739         switch (getNodeType(e)) {
740         case NodeType_AND:
741                 model_print("and");
742                 break;
743         case NodeType_ITE:
744                 model_print("ite");
745                 break;
746         case NodeType_IFF:
747                 model_print("iff");
748                 break;
749         }
750         model_print("(");
751         for (uint i = 0; i < n->numEdges; i++) {
752                 Edge e = n->edges[i];
753                 if (i != 0)
754                         model_print(" ");
755                 printCNF(e);
756         }
757         model_print(")");
758 }
759
760 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
761         Edge carray[numvars];
762         for (uint j = 0; j < numvars; j++) {
763                 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
764                 value = value >> 1;
765         }
766
767         return constraintAND(cnf, numvars, carray);
768 }
769
770 /** Generates a constraint to ensure that all encodings are less than value */
771 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
772         Edge orarray[numvars];
773         Edge andarray[numvars];
774         uint andi = 0;
775
776         while (true) {
777                 uint val = value;
778                 uint ori = 0;
779                 for (uint j = 0; j < numvars; j++) {
780                         if ((val & 1) == 1)
781                                 orarray[ori++] = constraintNegate(vars[j]);
782                         val = val >> 1;
783                 }
784                 //no ones to flip, so bail now...
785                 if (ori == 0) {
786                         return constraintAND(cnf, andi, andarray);
787                 }
788                 andarray[andi++] = constraintOR(cnf, ori, orarray);
789
790                 value = value + (1 << (__builtin_ctz(value)));
791                 //flip the last one
792         }
793 }
794
795 void generateAddConstraint(CNF *cnf, uint nSum, Edge *sum, uint nVar1, Edge *var1, uint nVar2, Edge *var2) {
796         //TO WRITE....
797 }
798
799 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
800         if (numvars == 0)
801                 return E_True;
802         Edge array[numvars];
803         for (uint i = 0; i < numvars; i++) {
804                 array[i] = constraintIFF(cnf, var1[i], var2[i]);
805         }
806         return constraintAND(cnf, numvars, array);
807 }
808
809 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
810         if (numvars == 0 )
811                 return E_False;
812         Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
813         for (uint i = 1; i < numvars; i++) {
814                 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
815                 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
816                 result = constraintOR2(cnf, lt, eq);
817         }
818         return result;
819 }
820
821 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
822         if (numvars == 0 )
823                 return E_True;
824         Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
825         for (uint i = 1; i < numvars; i++) {
826                 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
827                 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
828                 result = constraintOR2(cnf, lt, eq);
829         }
830         return result;
831 }