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    V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
   9    Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
  10
  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:
  18
  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
  25    work.
  26
  27    Contact Pete Manolios if you want any of these conditions waived.
  28
  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.
  36  */
  37
  38 /*
  39    C port of CNF SAT Conversion Copyright Brian Demsky 2017.
  40  */
  41
  42
  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};
  48
  49
  50 CNF *createCNF() {
  51         CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
  52         cnf->varcount = 1;
  53         cnf->solver = allocIncrementalSolver();
  54         cnf->solveTime = 0;
  55         cnf->encodeTime = 0;
  56         return cnf;
  57 }
  58
  59 void deleteCNF(CNF *cnf) {
  60         deleteIncrementalSolver(cnf->solver);
  61         ourfree(cnf);
  62 }
  63
  64 void resetCNF(CNF *cnf) {
  65         resetSolver(cnf->solver);
  66         cnf->varcount = 1;
  67         cnf->solveTime = 0;
  68         cnf->encodeTime = 0;
  69 }
  70
  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;
  75         return n;
  76 }
  77
  78 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
  79         Edge e = {allocNode(type, numEdges, edges)};
  80         return e;
  81 }
  82
  83 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
  84         Edge edgearray[numEdges];
  85
  86         for (uint i = 0; i < numEdges; i++) {
  87                 edgearray[i] = constraintNegate(edges[i]);
  88         }
  89         Edge eand = constraintAND(cnf, numEdges, edgearray);
  90         return constraintNegate(eand);
  91 }
  92
  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);
  98 }
  99
 100 int comparefunction(const Edge *e1, const Edge *e2) {
 101         if (e1->node_ptr == e2->node_ptr)
 102                 return 0;
 103         if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
 104                 return -1;
 105         else
 106                 return 1;
 107 }
 108
 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);
 112         uint initindex = 0;
 113         while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
 114                 initindex++;
 115
 116         uint remainSize = numEdges - initindex;
 117
 118         if (remainSize == 0)
 119                 return E_True;
 120         else if (remainSize == 1)
 121                 return edges[initindex];
 122         else if (equalsEdge(edges[initindex], E_False))
 123                 return E_False;
 124
 125         /** De-duplicate array */
 126         uint lowindex = 0;
 127         edges[lowindex] = edges[initindex++];
 128
 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)) {
 134                                 return E_False;
 135                         }
 136                 } else
 137                         edges[++lowindex] = edges[initindex];
 138         }
 139         lowindex++;     //Make lowindex look like size
 140
 141         if (lowindex == 1)
 142                 return edges[0];
 143
 144         if (lowindex == 2 &&
 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]));
 160                 }
 161         }
 162
 163         return createNode(cnf, NodeType_AND, lowindex, edges);
 164 }
 165
 166 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
 167         Edge edges[2] = {left, right};
 168         return constraintAND(cnf, 2, edges);
 169 }
 170
 171 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
 172         Edge array[2];
 173         array[0] = left;
 174         array[1] = constraintNegate(right);
 175         Edge eand = constraintAND(cnf, 2, array);
 176         return constraintNegate(eand);
 177 }
 178
 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);
 183
 184         Edge e;
 185         if (equalsEdge(lpos, rpos)) {
 186                 e = E_True;
 187         } else if (ltEdge(lpos, rpos)) {
 188                 Edge edges[] = {lpos, rpos};
 189                 e = (edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
 190         } else {
 191                 Edge edges[] = {rpos, lpos};
 192                 e = (edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
 193         }
 194         if (negate)
 195                 e = constraintNegate(e);
 196         return e;
 197 }
 198
 199 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
 200         if (isNegEdge(cond)) {
 201                 cond = constraintNegate(cond);
 202                 Edge tmp = thenedge;
 203                 thenedge = elseedge;
 204                 elseedge = tmp;
 205         }
 206
 207         bool negate = isNegEdge(thenedge);
 208         if (negate) {
 209                 thenedge = constraintNegate(thenedge);
 210                 elseedge = constraintNegate(elseedge);
 211         }
 212
 213         Edge result;
 214         if (equalsEdge(cond, E_True)) {
 215                 result = thenedge;
 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)) {
 225                 result = thenedge;
 226         } else if (sameNodeOppSign(thenedge, elseedge)) {
 227                 if (ltEdge(cond, thenedge)) {
 228                         Edge array[] = {cond, thenedge};
 229                         result = createNode(cnf, NodeType_IFF, 2, array);
 230                 } else {
 231                         Edge array[] = {thenedge, cond};
 232                         result = createNode(cnf, NodeType_IFF, 2, array);
 233                 }
 234         } else {
 235                 Edge edges[] = {cond, thenedge, elseedge};
 236                 result = createNode(cnf, NodeType_ITE, 3, edges);
 237         }
 238         if (negate)
 239                 result = constraintNegate(result);
 240         return result;
 241 }
 242
 243 void addConstraintCNF(CNF *cnf, Edge constraint) {
 244         //      pushVectorEdge(&cnf->constraints, constraint);
 245 #ifdef CONFIG_DEBUG
 246         model_print("****SATC_ADDING NEW Constraint*****\n");
 247         printCNF(constraint);
 248         model_print("\n******************************\n");
 249 #endif
 250 }
 251
 252 Edge constraintNewVar(CNF *cnf) {
 253         uint varnum = cnf->varcount++;
 254         Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
 255         return e;
 256 }
 257
 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);
 268         return result;
 269 }
 270
 271 bool getValueCNF(CNF *cnf, Edge var) {
 272         Literal l = getEdgeVar(var);
 273         bool isneg = (l < 0);
 274         l = abs(l);
 275         return isneg ^ getValueSolver(cnf->solver, l);
 276 }
 277
 278 void printCNF(Edge e) {
 279         if (edgeIsVarConst(e)) {
 280                 Literal l = getEdgeVar(e);
 281                 model_print ("%d", l);
 282                 return;
 283         }
 284         bool isNeg = isNegEdge(e);
 285         if (edgeIsConst(e)) {
 286                 if (isNeg)
 287                         model_print("T");
 288                 else
 289                         model_print("F");
 290                 return;
 291         }
 292         Node *n = getNodePtrFromEdge(e);
 293         if (isNeg) {
 294                 //Pretty print things that are equivalent to OR's
 295                 if (getNodeType(e) == NodeType_AND) {
 296                         model_print("or(");
 297                         for (uint i = 0; i < n->numEdges; i++) {
 298                                 Edge e = n->edges[i];
 299                                 if (i != 0)
 300                                         model_print(" ");
 301                                 printCNF(constraintNegate(e));
 302                         }
 303                         model_print(")");
 304                         return;
 305                 }
 306
 307                 model_print("!");
 308         }
 309         switch (getNodeType(e)) {
 310         case NodeType_AND:
 311                 model_print("and");
 312                 break;
 313         case NodeType_ITE:
 314                 model_print("ite");
 315                 break;
 316         case NodeType_IFF:
 317                 model_print("iff");
 318                 break;
 319         }
 320         model_print("(");
 321         for (uint i = 0; i < n->numEdges; i++) {
 322                 Edge e = n->edges[i];
 323                 if (i != 0)
 324                         model_print(" ");
 325                 printCNF(e);
 326         }
 327         model_print(")");
 328 }
 329
 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]);
 334                 value = value >> 1;
 335         }
 336
 337         return constraintAND(cnf, numvars, carray);
 338 }
 339
 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];
 344         uint andi = 0;
 345
 346         while (true) {
 347                 uint val = value;
 348                 uint ori = 0;
 349                 for (uint j = 0; j < numvars; j++) {
 350                         if ((val & 1) == 1)
 351                                 orarray[ori++] = constraintNegate(vars[j]);
 352                         val = val >> 1;
 353                 }
 354                 //no ones to flip, so bail now...
 355                 if (ori == 0) {
 356                         return constraintAND(cnf, andi, andarray);
 357                 }
 358                 andarray[andi++] = constraintOR(cnf, ori, orarray);
 359
 360                 value = value + (1 << (__builtin_ctz(value)));
 361                 //flip the last one
 362         }
 363 }
 364
 365 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 366         if (numvars == 0)
 367                 return E_True;
 368         Edge array[numvars];
 369         for (uint i = 0; i < numvars; i++) {
 370                 array[i] = constraintIFF(cnf, var1[i], var2[i]);
 371         }
 372         return constraintAND(cnf, numvars, array);
 373 }
 374
 375 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 376         if (numvars == 0 )
 377                 return E_False;
 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);
 383         }
 384         return result;
 385 }
 386
 387 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 388         if (numvars == 0 )
 389                 return E_True;
 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);
 395         }
 396         return result;
 397 }