1 #include "constraint.h"
4 #include "inc_solver.h"
8 V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
9 Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
11 Permission is hereby granted, free of charge, to any person obtaining
12 a copy of this software and associated documentation files (the
13 "Software"), to deal in the Software without restriction, including
14 without limitation the rights to use, copy, modify, merge, publish,
15 distribute, sublicense, and/or sell copies of the Software, and to
16 permit persons to whom the Software is furnished to do so, subject to
17 the following conditions:
19 The above copyright notice and this permission notice shall be
20 included in all copies or substantial portions of the Software. If
21 you download or use the software, send email to Pete Manolios
22 (pete@ccs.neu.edu) with your name, contact information, and a short
23 note describing what you want to use BAT for. For any reuse or
24 distribution, you must make clear to others the license terms of this
27 Contact Pete Manolios if you want any of these conditions waived.
29 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
30 EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
31 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
32 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
33 LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
34 OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
35 WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
39 C port of CNF SAT Conversion Copyright Brian Demsky 2017.
43 VectorImpl(Edge, Edge, 16)
44 Edge E_True = {(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
45 Edge E_False = {(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
46 Edge E_BOGUS = {(Node *)0xffff5673};
47 Edge E_NULL = {(Node *)NULL};
51 CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
53 cnf->solver = allocIncrementalSolver();
59 void deleteCNF(CNF *cnf) {
60 deleteIncrementalSolver(cnf->solver);
64 void resetCNF(CNF *cnf) {
65 resetSolver(cnf->solver);
71 Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
72 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
73 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
74 n->numEdges = numEdges;
78 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
79 Edge e = {allocNode(type, numEdges, edges)};
83 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
84 Edge edgearray[numEdges];
86 for (uint i = 0; i < numEdges; i++) {
87 edgearray[i] = constraintNegate(edges[i]);
89 Edge eand = constraintAND(cnf, numEdges, edgearray);
90 return constraintNegate(eand);
93 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
94 Edge lneg = constraintNegate(left);
95 Edge rneg = constraintNegate(right);
96 Edge eand = constraintAND2(cnf, lneg, rneg);
97 return constraintNegate(eand);
100 int comparefunction(const Edge *e1, const Edge *e2) {
101 if (e1->node_ptr == e2->node_ptr)
103 if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
109 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
110 ASSERT(numEdges != 0);
111 bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
113 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
116 uint remainSize = numEdges - initindex;
120 else if (remainSize == 1)
121 return edges[initindex];
122 else if (equalsEdge(edges[initindex], E_False))
125 /** De-duplicate array */
127 edges[lowindex] = edges[initindex++];
129 for (; initindex < numEdges; initindex++) {
130 Edge e1 = edges[lowindex];
131 Edge e2 = edges[initindex];
132 if (sameNodeVarEdge(e1, e2)) {
133 if (!sameSignEdge(e1, e2)) {
137 edges[++lowindex] = edges[initindex];
139 lowindex++; //Make lowindex look like size
145 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
146 getNodeType(edges[0]) == NodeType_AND &&
147 getNodeType(edges[1]) == NodeType_AND &&
148 getNodeSize(edges[0]) == 2 &&
149 getNodeSize(edges[1]) == 2) {
150 Edge *e0edges = getEdgeArray(edges[0]);
151 Edge *e1edges = getEdgeArray(edges[1]);
152 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
153 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
154 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
155 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
156 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
157 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
158 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
159 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
163 return createNode(cnf, NodeType_AND, lowindex, edges);
166 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
167 Edge edges[2] = {left, right};
168 return constraintAND(cnf, 2, edges);
171 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
174 array[1] = constraintNegate(right);
175 Edge eand = constraintAND(cnf, 2, array);
176 return constraintNegate(eand);
179 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
180 bool negate = !sameSignEdge(left, right);
181 Edge lpos = getNonNeg(left);
182 Edge rpos = getNonNeg(right);
185 if (equalsEdge(lpos, rpos)) {
187 } else if (ltEdge(lpos, rpos)) {
188 Edge edges[] = {lpos, rpos};
189 e = (edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
191 Edge edges[] = {rpos, lpos};
192 e = (edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
195 e = constraintNegate(e);
199 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
200 if (isNegEdge(cond)) {
201 cond = constraintNegate(cond);
207 bool negate = isNegEdge(thenedge);
209 thenedge = constraintNegate(thenedge);
210 elseedge = constraintNegate(elseedge);
214 if (equalsEdge(cond, E_True)) {
216 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
217 Edge array[] = {cond, elseedge};
218 result = constraintOR(cnf, 2, array);
219 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
220 result = constraintIMPLIES(cnf, cond, thenedge);
221 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
222 Edge array[] = {cond, thenedge};
223 result = constraintAND(cnf, 2, array);
224 } else if (equalsEdge(thenedge, elseedge)) {
226 } else if (sameNodeOppSign(thenedge, elseedge)) {
227 if (ltEdge(cond, thenedge)) {
228 Edge array[] = {cond, thenedge};
229 result = createNode(cnf, NodeType_IFF, 2, array);
231 Edge array[] = {thenedge, cond};
232 result = createNode(cnf, NodeType_IFF, 2, array);
235 Edge edges[] = {cond, thenedge, elseedge};
236 result = createNode(cnf, NodeType_ITE, 3, edges);
239 result = constraintNegate(result);
243 void addConstraintCNF(CNF *cnf, Edge constraint) {
244 // pushVectorEdge(&cnf->constraints, constraint);
246 model_print("****SATC_ADDING NEW Constraint*****\n");
247 printCNF(constraint);
248 model_print("\n******************************\n");
252 Edge constraintNewVar(CNF *cnf) {
253 uint varnum = cnf->varcount++;
254 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
258 int solveCNF(CNF *cnf) {
259 long long startTime = getTimeNano();
260 finishedClauses(cnf->solver);
261 long long startSolve = getTimeNano();
262 int result = solve(cnf->solver);
263 long long finishTime = getTimeNano();
264 cnf->encodeTime = startSolve - startTime;
265 model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
266 cnf->solveTime = finishTime - startSolve;
267 model_print("Solve time: %f\n", cnf->solveTime / 1000000000.0);
271 bool getValueCNF(CNF *cnf, Edge var) {
272 Literal l = getEdgeVar(var);
273 bool isneg = (l < 0);
275 return isneg ^ getValueSolver(cnf->solver, l);
278 void printCNF(Edge e) {
279 if (edgeIsVarConst(e)) {
280 Literal l = getEdgeVar(e);
281 model_print ("%d", l);
284 bool isNeg = isNegEdge(e);
285 if (edgeIsConst(e)) {
292 Node *n = getNodePtrFromEdge(e);
294 //Pretty print things that are equivalent to OR's
295 if (getNodeType(e) == NodeType_AND) {
297 for (uint i = 0; i < n->numEdges; i++) {
298 Edge e = n->edges[i];
301 printCNF(constraintNegate(e));
309 switch (getNodeType(e)) {
321 for (uint i = 0; i < n->numEdges; i++) {
322 Edge e = n->edges[i];
330 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
331 Edge carray[numvars];
332 for (uint j = 0; j < numvars; j++) {
333 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
337 return constraintAND(cnf, numvars, carray);
340 /** Generates a constraint to ensure that all encodings are less than value */
341 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
342 Edge orarray[numvars];
343 Edge andarray[numvars];
349 for (uint j = 0; j < numvars; j++) {
351 orarray[ori++] = constraintNegate(vars[j]);
354 //no ones to flip, so bail now...
356 return constraintAND(cnf, andi, andarray);
358 andarray[andi++] = constraintOR(cnf, ori, orarray);
360 value = value + (1 << (__builtin_ctz(value)));
365 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
369 for (uint i = 0; i < numvars; i++) {
370 array[i] = constraintIFF(cnf, var1[i], var2[i]);
372 return constraintAND(cnf, numvars, array);
375 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
378 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
379 for (uint i = 1; i < numvars; i++) {
380 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
381 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
382 result = constraintOR2(cnf, lt, eq);
387 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
390 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
391 for (uint i = 1; i < numvars; i++) {
392 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
393 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
394 result = constraintOR2(cnf, lt, eq);