1 #include "constraint.h"
4 #include "inc_solver.h"
8 CNF SAT Conversion Copyright Brian Demsky 2017.
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};
20 CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
22 cnf->solver = allocIncrementalSolver();
25 cnf->asize = DEFAULT_CNF_ARRAY_SIZE;
26 cnf->array = (int *) ourmalloc(sizeof(int) * DEFAULT_CNF_ARRAY_SIZE);
31 void deleteCNF(CNF *cnf) {
32 deleteIncrementalSolver(cnf->solver);
37 void resetCNF(CNF *cnf) {
38 resetSolver(cnf->solver);
45 Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
46 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
48 n->numEdges = numEdges;
49 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
53 Node *allocBaseNode(NodeType type, uint numEdges) {
54 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
56 n->numEdges = numEdges;
60 Node *allocResizeNode(uint capacity) {
61 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * capacity);
63 n->capacity = capacity;
67 Edge cloneEdge(Edge e) {
68 if (edgeIsVarConst(e))
70 Node * node = getNodePtrFromEdge(e);
71 bool isneg = isNegEdge(e);
72 uint numEdges = node->numEdges;
73 Node * clone = allocBaseNode(node->type, numEdges);
74 for(uint i=0; i < numEdges; i++) {
75 clone->edges[i] = cloneEdge(node->edges[i]);
77 return isneg ? constraintNegate((Edge) {clone}) : (Edge) {clone};
80 void freeEdgeRec(Edge e) {
81 if (edgeIsVarConst(e))
83 Node * node = getNodePtrFromEdge(e);
84 uint numEdges = node->numEdges;
85 for(uint i=0; i < numEdges; i++) {
86 freeEdgeRec(node->edges[i]);
91 void freeEdge(Edge e) {
92 if (edgeIsVarConst(e))
94 Node * node = getNodePtrFromEdge(e);
98 void freeEdgesRec(uint numEdges, Edge * earray) {
99 for(uint i=0; i < numEdges; i++) {
105 void freeEdgeCNF(Edge e) {
106 Node * node = getNodePtrFromEdge(e);
107 uint numEdges = node->numEdges;
108 for(uint i=0; i < numEdges; i++) {
109 Edge ec = node->edges[i];
110 if (!edgeIsVarConst(ec)) {
111 ourfree(ec.node_ptr);
117 void addEdgeToResizeNode(Node ** node, Edge e) {
118 Node *currnode = *node;
119 if (currnode->capacity == currnode->numEdges) {
120 Node *newnode = allocResizeNode( currnode->capacity << 1);
121 newnode->numEdges = currnode->numEdges;
122 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
127 currnode->edges[currnode->numEdges++] = e;
130 void mergeFreeNodeToResizeNode(Node **node, Node * innode) {
131 Node * currnode = *node;
132 uint currEdges = currnode->numEdges;
133 uint inEdges = innode->numEdges;
135 uint newsize = currEdges + inEdges;
136 if (newsize >= currnode->capacity) {
137 if (newsize < innode->capacity) {
141 *node = currnode = tmp;
143 Node *newnode = allocResizeNode( newsize << 1);
144 newnode->numEdges = currnode->numEdges;
145 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
151 if (inEdges > currEdges && newsize < innode->capacity) {
155 *node = currnode = tmp;
158 memcpy(&currnode->edges[currnode->numEdges], innode->edges, innode->numEdges * sizeof(Edge));
159 currnode->numEdges += innode->numEdges;
163 void mergeNodeToResizeNode(Node **node, Node * innode) {
164 Node * currnode = *node;
165 uint currEdges = currnode->numEdges;
166 uint inEdges = innode->numEdges;
167 uint newsize = currEdges + inEdges;
168 if (newsize >= currnode->capacity) {
169 Node *newnode = allocResizeNode( newsize << 1);
170 newnode->numEdges = currnode->numEdges;
171 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
176 memcpy(&currnode->edges[currnode->numEdges], innode->edges, inEdges * sizeof(Edge));
177 currnode->numEdges += inEdges;
180 Edge createNode(NodeType type, uint numEdges, Edge *edges) {
181 Edge e = {allocNode(type, numEdges, edges)};
185 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
186 Edge edgearray[numEdges];
188 for (uint i = 0; i < numEdges; i++) {
189 edgearray[i] = constraintNegate(edges[i]);
191 Edge eand = constraintAND(cnf, numEdges, edgearray);
192 return constraintNegate(eand);
195 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
196 Edge lneg = constraintNegate(left);
197 Edge rneg = constraintNegate(right);
198 Edge eand = constraintAND2(cnf, lneg, rneg);
199 return constraintNegate(eand);
202 int comparefunction(const Edge *e1, const Edge *e2) {
203 if (e1->node_ptr == e2->node_ptr)
205 if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
211 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
212 ASSERT(numEdges != 0);
214 bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
216 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
219 uint remainSize = numEdges - initindex;
223 else if (remainSize == 1)
224 return edges[initindex];
225 else if (equalsEdge(edges[initindex], E_False)) {
226 freeEdgesRec(numEdges, edges);
230 /** De-duplicate array */
232 edges[lowindex] = edges[initindex++];
234 for (; initindex < numEdges; initindex++) {
235 Edge e1 = edges[lowindex];
236 Edge e2 = edges[initindex];
237 if (sameNodeVarEdge(e1, e2)) {
238 ASSERT(!isNodeEdge(e1));
239 if (!sameSignEdge(e1, e2)) {
240 freeEdgesRec(lowindex + 1, edges);
241 freeEdgesRec(numEdges-initindex, &edges[initindex]);
245 edges[++lowindex] = edges[initindex];
247 lowindex++; //Make lowindex look like size
253 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
254 getNodeType(edges[0]) == NodeType_AND &&
255 getNodeType(edges[1]) == NodeType_AND &&
256 getNodeSize(edges[0]) == 2 &&
257 getNodeSize(edges[1]) == 2) {
258 Edge *e0edges = getEdgeArray(edges[0]);
259 Edge *e1edges = getEdgeArray(edges[1]);
260 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
261 Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
265 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
266 Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
270 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
271 Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
275 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
276 Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
283 return createNode(NodeType_AND, lowindex, edges);
286 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
287 Edge edges[2] = {left, right};
288 return constraintAND(cnf, 2, edges);
291 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
294 array[1] = constraintNegate(right);
295 Edge eand = constraintAND(cnf, 2, array);
296 return constraintNegate(eand);
299 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
300 bool negate = !sameSignEdge(left, right);
301 Edge lpos = getNonNeg(left);
302 Edge rpos = getNonNeg(right);
305 if (equalsEdge(lpos, rpos)) {
309 } else if (ltEdge(lpos, rpos)) {
310 Edge edges[] = {lpos, rpos};
311 e = (edgeIsConst(lpos)) ? rpos : createNode(NodeType_IFF, 2, edges);
313 Edge edges[] = {rpos, lpos};
314 e = (edgeIsConst(rpos)) ? lpos : createNode(NodeType_IFF, 2, edges);
317 e = constraintNegate(e);
321 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
322 if (isNegEdge(cond)) {
323 cond = constraintNegate(cond);
329 bool negate = isNegEdge(thenedge);
331 thenedge = constraintNegate(thenedge);
332 elseedge = constraintNegate(elseedge);
336 if (equalsEdge(cond, E_True)) {
337 freeEdgeRec(elseedge);
339 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
340 Edge array[] = {cond, elseedge};
341 result = constraintOR(cnf, 2, array);
342 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
343 result = constraintIMPLIES(cnf, cond, thenedge);
344 } else if (equalsEdge(elseedge, E_False) || equalsEdge(cond, elseedge)) {
345 Edge array[] = {cond, thenedge};
346 result = constraintAND(cnf, 2, array);
347 } else if (equalsEdge(thenedge, elseedge)) {
350 } else if (sameNodeOppSign(thenedge, elseedge)) {
351 if (ltEdge(cond, thenedge)) {
352 Edge array[] = {cond, thenedge};
353 result = createNode(NodeType_IFF, 2, array);
355 Edge array[] = {thenedge, cond};
356 result = createNode(NodeType_IFF, 2, array);
359 Edge edges[] = {cond, thenedge, elseedge};
360 result = createNode(NodeType_ITE, 3, edges);
363 result = constraintNegate(result);
367 Edge disjoinLit(Edge vec, Edge lit) {
368 Node *nvec = vec.node_ptr;
369 uint nvecedges = nvec->numEdges;
371 for(uint i=0; i < nvecedges; i++) {
372 Edge ce = nvec->edges[i];
373 if (!edgeIsVarConst(ce)) {
374 Node *cne = ce.node_ptr;
375 addEdgeToResizeNode(&cne, lit);
376 nvec->edges[i] = (Edge) {cne};
378 Node *clause = allocResizeNode(2);
379 addEdgeToResizeNode(&clause, lit);
380 addEdgeToResizeNode(&clause, ce);
381 nvec->edges[i] = (Edge) {clause};
387 Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
388 Node * result = allocResizeNode(1);
389 Node *nnewvec = newvec.node_ptr;
390 Node *ncnfform = cnfform.node_ptr;
391 uint newvecedges = nnewvec->numEdges;
392 uint cnfedges = ncnfform->numEdges;
393 if (newvecedges == 1 || cnfedges ==1) {
398 newvecedges = cnfedges;
401 Edge e = ncnfform->edges[0];
402 if (!edgeIsVarConst(e)) {
403 Node *n = e.node_ptr;
404 for(uint i=0; i < newvecedges; i++) {
405 Edge ce = nnewvec->edges[i];
406 if (isNodeEdge(ce)) {
407 Node *cne = ce.node_ptr;
408 mergeNodeToResizeNode(&cne, n);
409 nnewvec->edges[i] = (Edge) {cne};
411 Node *clause = allocResizeNode(n->numEdges + 1);
412 mergeNodeToResizeNode(&clause, n);
413 addEdgeToResizeNode(&clause, ce);
414 nnewvec->edges[i] = (Edge) {clause};
418 for(uint i=0; i < newvecedges; i++) {
419 Edge ce = nnewvec->edges[i];
420 if (!edgeIsVarConst(ce)) {
421 Node *cne = ce.node_ptr;
422 addEdgeToResizeNode(&cne, e);
423 nnewvec->edges[i] = (Edge) {cne};
425 Node *clause = allocResizeNode(2);
426 addEdgeToResizeNode(&clause, e);
427 addEdgeToResizeNode(&clause, ce);
428 nnewvec->edges[i] = (Edge) {clause};
432 freeEdgeCNF((Edge){ncnfform});
433 return (Edge) {nnewvec};
435 if ((newvecedges > 3 && cnfedges > 3) ||
436 (newvecedges > 10 && cnfedges >=2) ||
437 (newvecedges >= 2 && cnfedges > 10)) {
438 Edge proxyVar = constraintNewVar(cnf);
439 if (newvecedges > cnfedges) {
440 outputCNFOR(cnf, newvec, constraintNegate(proxyVar));
442 return disjoinLit(cnfform, proxyVar);
444 outputCNFOR(cnf, cnfform, constraintNegate(proxyVar));
445 freeEdgeCNF(cnfform);
446 return disjoinLit(newvec, proxyVar);
449 for(uint i=0; i <newvecedges; i++) {
450 Edge nedge = nnewvec->edges[i];
451 uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1;
452 for(uint j=0; j < cnfedges; j++) {
453 Edge cedge = ncnfform->edges[j];
454 uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
455 if (equalsEdge(cedge, nedge)) {
456 addEdgeToResizeNode(&result, cedge);
457 } else if (!sameNodeOppSign(nedge, cedge)) {
458 Node *clause = allocResizeNode(cSize + nSize);
459 if (isNodeEdge(nedge)) {
460 mergeNodeToResizeNode(&clause, nedge.node_ptr);
462 addEdgeToResizeNode(&clause, nedge);
464 if (isNodeEdge(cedge)) {
465 mergeNodeToResizeNode(&clause, cedge.node_ptr);
467 addEdgeToResizeNode(&clause, cedge);
469 addEdgeToResizeNode(&result, (Edge){clause});
475 freeEdgeCNF(cnfform);
476 return (Edge) {result};
479 Edge simplifyCNF(CNF *cnf, Edge input) {
480 if (edgeIsVarConst(input)) {
481 Node *newvec = allocResizeNode(1);
482 addEdgeToResizeNode(&newvec, input);
483 return (Edge) {newvec};
485 bool negated = isNegEdge(input);
486 Node * node = getNodePtrFromEdge(input);
487 NodeType type = node->type;
489 if (type == NodeType_AND) {
491 Node *newvec = allocResizeNode(node->numEdges);
492 uint numEdges = node->numEdges;
493 for(uint i = 0; i < numEdges; i++) {
494 Edge e = simplifyCNF(cnf, node->edges[i]);
495 mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
497 return (Edge) {newvec};
499 Edge cond = node->edges[0];
500 Edge thenedge = node->edges[1];
501 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
502 Edge thenedges[] = {cond, constraintNegate(thenedge)};
503 Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
504 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
505 Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
506 Edge thencnf = simplifyCNF(cnf, thencons);
507 Edge elsecnf = simplifyCNF(cnf, elsecons);
508 //free temporary nodes
509 ourfree(getNodePtrFromEdge(thencons));
510 ourfree(getNodePtrFromEdge(elsecons));
511 Node * result = thencnf.node_ptr;
512 mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
513 return (Edge) {result};
516 if (type == NodeType_AND) {
518 uint numEdges = node->numEdges;
520 Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
521 for(uint i = 1; i < numEdges; i++) {
522 Edge e = node->edges[i];
523 Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
524 newvec = disjoinAndFree(cnf, newvec, cnfform);
528 Edge cond = node->edges[0];
529 Edge thenedge = node->edges[1];
530 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
533 Edge thenedges[] = {cond, constraintNegate(thenedge)};
534 Edge thencons = createNode(NodeType_AND, 2, thenedges);
535 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
536 Edge elsecons = createNode(NodeType_AND, 2, elseedges);
538 Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
539 Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
540 Edge result = simplifyCNF(cnf, combined);
541 //free temporary nodes
542 ourfree(getNodePtrFromEdge(thencons));
543 ourfree(getNodePtrFromEdge(elsecons));
544 ourfree(getNodePtrFromEdge(combined));
551 Edge simplifyCNF(CNF *cnf, Edge input) {
552 if (edgeIsVarConst(input)) {
553 Node *newvec = allocResizeNode(1);
554 addEdgeToResizeNode(&newvec, input);
555 return (Edge) {newvec};
557 bool negated = isNegEdge(input);
558 Node * node = getNodePtrFromEdge(input);
559 NodeType type = node->type;
561 if (type == NodeType_AND) {
563 Node *newvec = allocResizeNode(node->numEdges);
564 uint numEdges = node->numEdges;
565 for(uint i = 0; i < numEdges; i++) {
566 Edge e = simplifyCNF(cnf, node->edges[i]);
567 mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
569 return (Edge) {newvec};
571 Edge cond = node->edges[0];
572 Edge thenedge = node->edges[1];
573 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
574 Edge thenedges[] = {cond, constraintNegate(thenedge)};
575 Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
576 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
577 Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
578 Edge thencnf = simplifyCNF(cnf, thencons);
579 Edge elsecnf = simplifyCNF(cnf, elsecons);
580 //free temporary nodes
581 ourfree(getNodePtrFromEdge(thencons));
582 ourfree(getNodePtrFromEdge(elsecons));
583 Node * result = thencnf.node_ptr;
584 mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
585 return (Edge) {result};
588 if (type == NodeType_AND) {
590 uint numEdges = node->numEdges;
592 for(uint i = 0; i < numEdges; i++) {
593 Edge e = node->edges[i];
594 bool enegate = isNegEdge(e);
595 if (!edgeIsVarConst(e)) {
596 Node * enode = getNodePtrFromEdge(e);
597 NodeType etype = enode->type;
599 if (etype == NodeType_AND) {
601 uint eNumEdges = enode->numEdges;
602 Node * newnode = allocResizeNode(0);
603 Node * clause = allocBaseNode(NodeType_AND, numEdges);
604 memcpy(clause->edges, node->edges, sizeof(Edge) * i);
605 if ((i + 1) < numEdges) {
606 memcpy(&clause->edges[i+1], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
609 for(uint j = 0; j < eNumEdges; j++) {
610 clause->edges[i] = constraintNegate(enode->edges[j]);
611 Edge simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
612 mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
615 return (Edge) {newnode};
618 Edge cond = enode->edges[0];
619 Edge thenedge = enode->edges[1];
620 Edge elseedge = (enode->type == NodeType_IFF) ? constraintNegate(thenedge) : enode->edges[2];
621 Edge thenedges[] = {cond, constraintNegate(thenedge)};
622 Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
623 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
624 Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
627 Node * newnode = allocResizeNode(0);
628 Node * clause = allocBaseNode(NodeType_AND, numEdges);
629 memcpy(clause->edges, node->edges, sizeof(Edge) * i);
630 if ((i + 1) < numEdges) {
631 memcpy(&clause->edges[i+1], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
634 clause->edges[i] = constraintNegate(thencons);
635 Edge simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
636 mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
638 clause->edges[i] = constraintNegate(elsecons);
639 simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
640 mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
642 //free temporary nodes
643 ourfree(getNodePtrFromEdge(thencons));
644 ourfree(getNodePtrFromEdge(elsecons));
646 return (Edge) {newnode};
649 if (etype == NodeType_AND) {
651 uint eNumEdges = enode->numEdges;
652 Node * clause = allocBaseNode(NodeType_AND, eNumEdges + numEdges - 1);
653 memcpy(clause->edges, node->edges, sizeof(Edge) * i);
654 if ((i + 1) < numEdges) {
655 memcpy(&clause->edges[i], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
657 memcpy(&clause->edges[numEdges-1], enode->edges, sizeof(Edge) * eNumEdges);
658 Edge eclause = {clause};
659 Edge result = simplifyCNF(cnf, constraintNegate(eclause));
663 //OR of !(IFF or ITE)
664 Edge cond = node->edges[0];
665 Edge thenedge = node->edges[1];
666 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
667 Edge thenedges[] = {cond, constraintNegate(thenedge)};
668 Edge thencons = createNode(NodeType_AND, 2, thenedges);
669 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
670 Edge elsecons = createNode(NodeType_AND, 2, elseedges);
673 Node * clause = allocBaseNode(NodeType_AND, numEdges + 1);
674 memcpy(clause->edges, node->edges, sizeof(Edge) * i);
675 if ((i + 1) < numEdges) {
676 memcpy(&clause->edges[i], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
678 clause->edges[numEdges-1] = constraintNegate(thencons);
679 clause->edges[numEdges] = constraintNegate(elsecons);
680 Edge result = simplifyCNF(cnf, constraintNegate((Edge) {clause}));
681 //free temporary nodes
682 ourfree(getNodePtrFromEdge(thencons));
683 ourfree(getNodePtrFromEdge(elsecons));
691 Node *newvec = allocResizeNode(numEdges);
692 for(uint i=0; i < numEdges; i++) {
693 addEdgeToResizeNode(&newvec, constraintNegate(node->edges[i]));
695 Node * result = allocResizeNode(1);
696 addEdgeToResizeNode(&result, (Edge){newvec});
697 return (Edge) {result};
699 Edge cond = node->edges[0];
700 Edge thenedge = node->edges[1];
701 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
704 Edge thenedges[] = {cond, constraintNegate(thenedge)};
705 Edge thencons = createNode(NodeType_AND, 2, thenedges);
706 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
707 Edge elsecons = createNode(NodeType_AND, 2, elseedges);
709 Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
710 Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
711 Edge result = simplifyCNF(cnf, combined);
712 //free temporary nodes
713 ourfree(getNodePtrFromEdge(thencons));
714 ourfree(getNodePtrFromEdge(elsecons));
715 ourfree(getNodePtrFromEdge(combined));
721 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
722 Node * andNode = cnfform.node_ptr;
723 int orvar = getEdgeVar(eorvar);
725 uint numEdges = andNode->numEdges;
726 for(uint i=0; i < numEdges; i++) {
727 Edge e = andNode->edges[i];
728 if (edgeIsVarConst(e)) {
729 int array[2] = {getEdgeVar(e), orvar};
730 ASSERT(array[0] != 0);
731 addArrayClauseLiteral(cnf->solver, 2, array);
733 Node * clause = e.node_ptr;
734 uint cnumEdges = clause->numEdges + 1;
735 if (cnumEdges > cnf->asize) {
736 cnf->asize = cnumEdges << 1;
738 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
740 int * array = cnf->array;
741 for(uint j=0; j < (cnumEdges - 1); j++) {
742 array[j] = getEdgeVar(clause->edges[j]);
743 ASSERT(array[j] != 0);
745 array[cnumEdges - 1] = orvar;
746 addArrayClauseLiteral(cnf->solver, cnumEdges, array);
752 void outputCNF(CNF *cnf, Edge cnfform) {
753 Node * andNode = cnfform.node_ptr;
754 uint numEdges = andNode->numEdges;
755 for(uint i=0; i < numEdges; i++) {
756 Edge e = andNode->edges[i];
757 if (edgeIsVarConst(e)) {
758 int array[1] = {getEdgeVar(e)};
759 ASSERT(array[0] != 0);
760 addArrayClauseLiteral(cnf->solver, 1, array);
762 Node * clause = e.node_ptr;
763 uint cnumEdges = clause->numEdges;
764 if (cnumEdges > cnf->asize) {
765 cnf->asize = cnumEdges << 1;
767 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
769 int * array = cnf->array;
770 for(uint j=0; j < cnumEdges; j++) {
771 array[j] = getEdgeVar(clause->edges[j]);
772 ASSERT(array[j] != 0);
774 addArrayClauseLiteral(cnf->solver, cnumEdges, array);
779 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
780 ASSERT(p != P_UNDEFINED);
781 if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
782 // proxy => expression
783 Edge cnfexpr = simplifyCNF(cnf, expression);
785 freeEdgeRec(expression);
786 outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
787 freeEdgeCNF(cnfexpr);
789 if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
790 // expression => proxy
791 Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
792 freeEdgeRec(expression);
793 outputCNFOR(cnf, cnfnegexpr, proxy);
794 freeEdgeCNF(cnfnegexpr);
798 void addConstraintCNF(CNF *cnf, Edge constraint) {
799 if (equalsEdge(constraint, E_True)) {
801 } else if (equalsEdge(constraint, E_False)) {
806 freeEdgeRec(constraint);
811 model_print("****SATC_ADDING NEW Constraint*****\n");
812 printCNF(constraint);
813 model_print("\n******************************\n");
816 Edge cnfform = simplifyCNF(cnf, constraint);
817 freeEdgeRec(constraint);
818 outputCNF(cnf, cnfform);
819 freeEdgeCNF(cnfform);
822 Edge constraintNewVar(CNF *cnf) {
823 uint varnum = cnf->varcount++;
824 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
828 int solveCNF(CNF *cnf) {
829 long long startTime = getTimeNano();
830 finishedClauses(cnf->solver);
831 long long startSolve = getTimeNano();
832 int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
833 long long finishTime = getTimeNano();
834 cnf->encodeTime = startSolve - startTime;
835 model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
836 cnf->solveTime = finishTime - startSolve;
837 model_print("Solve time: %f\n", cnf->solveTime / 1000000000.0);
841 bool getValueCNF(CNF *cnf, Edge var) {
842 Literal l = getEdgeVar(var);
843 bool isneg = (l < 0);
845 return isneg ^ getValueSolver(cnf->solver, l);
848 void printCNF(Edge e) {
849 if (edgeIsVarConst(e)) {
850 Literal l = getEdgeVar(e);
851 model_print ("%d", l);
854 bool isNeg = isNegEdge(e);
855 if (edgeIsConst(e)) {
862 Node *n = getNodePtrFromEdge(e);
864 //Pretty print things that are equivalent to OR's
865 if (getNodeType(e) == NodeType_AND) {
867 for (uint i = 0; i < n->numEdges; i++) {
868 Edge e = n->edges[i];
871 printCNF(constraintNegate(e));
879 switch (getNodeType(e)) {
891 for (uint i = 0; i < n->numEdges; i++) {
892 Edge e = n->edges[i];
900 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
901 Edge carray[numvars];
902 for (uint j = 0; j < numvars; j++) {
903 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
907 return constraintAND(cnf, numvars, carray);
910 /** Generates a constraint to ensure that all encodings are less than value */
911 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
912 Edge orarray[numvars];
913 Edge andarray[numvars];
919 for (uint j = 0; j < numvars; j++) {
921 orarray[ori++] = constraintNegate(vars[j]);
924 //no ones to flip, so bail now...
926 return constraintAND(cnf, andi, andarray);
928 andarray[andi++] = constraintOR(cnf, ori, orarray);
930 value = value + (1 << (__builtin_ctz(value)));
935 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
939 for (uint i = 0; i < numvars; i++) {
940 array[i] = constraintIFF(cnf, var1[i], var2[i]);
942 return constraintAND(cnf, numvars, array);
945 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
948 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
949 for (uint i = 1; i < numvars; i++) {
950 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
951 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
952 result = constraintOR2(cnf, lt, eq);
957 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
960 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
961 for (uint i = 1; i < numvars; i++) {
962 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
963 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
964 result = constraintOR2(cnf, lt, eq);