src/csolver.cc

   1 #include "csolver.h"
   2 #include "set.h"
   3 #include "mutableset.h"
   4 #include "element.h"
   5 #include "boolean.h"
   6 #include "predicate.h"
   7 #include "order.h"
   8 #include "table.h"
   9 #include "function.h"
  10 #include "satencoder.h"
  11 #include "sattranslator.h"
  12 #include "tunable.h"
  13 #include "polarityassignment.h"
  14 #include "decomposeordertransform.h"
  15 #include "autotuner.h"
  16 #include "astops.h"
  17 #include "structs.h"
  18 #include "orderresolver.h"
  19 #include "integerencoding.h"
  20 #include "qsort.h"
  21 #include "preprocess.h"
  22 #include "serializer.h"
  23 #include "deserializer.h"
  24 #include "encodinggraph.h"
  25 #include "ordergraph.h"
  26 #include "orderedge.h"
  27 #include "orderanalysis.h"
  28 #include "elementopt.h"
  29 #include "varorderingopt.h"
  30 #include <time.h>
  31 #include <stdarg.h>
  32
  33 CSolver::CSolver() :
  34         boolTrue(BooleanEdge(new BooleanConst(true))),
  35         boolFalse(boolTrue.negate()),
  36         unsat(false),
  37         booleanVarUsed(false),
  38         tuner(NULL),
  39         elapsedTime(0),
  40         satsolverTimeout(NOTIMEOUT)
  41 {
  42         satEncoder = new SATEncoder(this);
  43 }
  44
  45 /** This function tears down the solver and the entire AST */
  46
  47 CSolver::~CSolver() {
  48         //serialize();
  49         uint size = allBooleans.getSize();
  50         for (uint i = 0; i < size; i++) {
  51                 delete allBooleans.get(i);
  52         }
  53
  54         size = allSets.getSize();
  55         for (uint i = 0; i < size; i++) {
  56                 delete allSets.get(i);
  57         }
  58
  59         size = allElements.getSize();
  60         for (uint i = 0; i < size; i++) {
  61                 Element *el = allElements.get(i);
  62                 delete el;
  63         }
  64
  65         size = allTables.getSize();
  66         for (uint i = 0; i < size; i++) {
  67                 delete allTables.get(i);
  68         }
  69
  70         size = allPredicates.getSize();
  71         for (uint i = 0; i < size; i++) {
  72                 delete allPredicates.get(i);
  73         }
  74
  75         size = allOrders.getSize();
  76         for (uint i = 0; i < size; i++) {
  77                 delete allOrders.get(i);
  78         }
  79         size = allFunctions.getSize();
  80         for (uint i = 0; i < size; i++) {
  81                 delete allFunctions.get(i);
  82         }
  83
  84         delete boolTrue.getBoolean();
  85         delete satEncoder;
  86 }
  87
  88 void CSolver::resetSolver() {
  89         //serialize();
  90         uint size = allBooleans.getSize();
  91         for (uint i = 0; i < size; i++) {
  92                 delete allBooleans.get(i);
  93         }
  94
  95         size = allSets.getSize();
  96         for (uint i = 0; i < size; i++) {
  97                 delete allSets.get(i);
  98         }
  99
 100         size = allElements.getSize();
 101         for (uint i = 0; i < size; i++) {
 102                 Element *el = allElements.get(i);
 103                 delete el;
 104         }
 105
 106         size = allTables.getSize();
 107         for (uint i = 0; i < size; i++) {
 108                 delete allTables.get(i);
 109         }
 110
 111         size = allPredicates.getSize();
 112         for (uint i = 0; i < size; i++) {
 113                 delete allPredicates.get(i);
 114         }
 115
 116         size = allOrders.getSize();
 117         for (uint i = 0; i < size; i++) {
 118                 delete allOrders.get(i);
 119         }
 120         size = allFunctions.getSize();
 121         for (uint i = 0; i < size; i++) {
 122                 delete allFunctions.get(i);
 123         }
 124         delete boolTrue.getBoolean();
 125         allBooleans.clear();
 126         allSets.clear();
 127         allElements.clear();
 128         allTables.clear();
 129         allPredicates.clear();
 130         allOrders.clear();
 131         allFunctions.clear();
 132         constraints.reset();
 133         activeOrders.reset();
 134         boolMap.reset();
 135         elemMap.reset();
 136
 137         boolTrue = BooleanEdge(new BooleanConst(true));
 138         boolFalse = boolTrue.negate();
 139         unsat = false;
 140         booleanVarUsed = false;
 141         elapsedTime = 0;
 142         tuner = NULL;
 143         satEncoder->resetSATEncoder();
 144
 145 }
 146
 147 CSolver *CSolver::clone() {
 148         CSolver *copy = new CSolver();
 149         CloneMap map;
 150         SetIteratorBooleanEdge *it = getConstraints();
 151         while (it->hasNext()) {
 152                 BooleanEdge b = it->next();
 153                 copy->addConstraint(cloneEdge(copy, &map, b));
 154         }
 155         delete it;
 156         return copy;
 157 }
 158
 159 CSolver *CSolver::deserialize(const char *file) {
 160         model_print("deserializing %s ...\n", file);
 161         Deserializer deserializer(file);
 162         return deserializer.deserialize();
 163 }
 164
 165 void CSolver::serialize() {
 166         model_print("serializing ...\n");
 167         char buffer[255];
 168         long long nanotime = getTimeNano();
 169         int numchars = sprintf(buffer, "DUMP%llu", nanotime);
 170         Serializer serializer(buffer);
 171         SetIteratorBooleanEdge *it = getConstraints();
 172         while (it->hasNext()) {
 173                 BooleanEdge b = it->next();
 174                 serializeBooleanEdge(&serializer, b, true);
 175         }
 176         delete it;
 177 }
 178
 179 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
 180         Set *set = new Set(type, elements, numelements);
 181         allSets.push(set);
 182         return set;
 183 }
 184
 185 Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange) {
 186         Set *set = new Set(type, lowrange, highrange);
 187         allSets.push(set);
 188         return set;
 189 }
 190
 191 bool CSolver::itemExistInSet(Set *set, uint64_t item) {
 192         return set->exists(item);
 193 }
 194
 195 VarType CSolver::getSetVarType(Set *set) {
 196         return set->getType();
 197 }
 198
 199 Element *CSolver::createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange) {
 200         Set *s = createRangeSet(type, lowrange, highrange);
 201         return getElementVar(s);
 202 }
 203
 204 MutableSet *CSolver::createMutableSet(VarType type) {
 205         MutableSet *set = new MutableSet(type);
 206         allSets.push(set);
 207         return set;
 208 }
 209
 210 void CSolver::addItem(MutableSet *set, uint64_t element) {
 211         set->addElementMSet(element);
 212 }
 213
 214 uint64_t CSolver::createUniqueItem(MutableSet *set) {
 215         uint64_t element = set->getNewUniqueItem();
 216         set->addElementMSet(element);
 217         return element;
 218 }
 219
 220 void CSolver::finalizeMutableSet(MutableSet *set) {
 221         set->finalize();
 222 }
 223
 224 Element *CSolver::getElementVar(Set *set) {
 225         Element *element = new ElementSet(set);
 226         allElements.push(element);
 227         return element;
 228 }
 229
 230 void CSolver::mustHaveValue(Element *element) {
 231         element->anyValue = true;
 232 }
 233
 234 Set *CSolver::getElementRange (Element *element) {
 235         return element->getRange();
 236 }
 237
 238
 239 Element *CSolver::getElementConst(VarType type, uint64_t value) {
 240         uint64_t array[] = {value};
 241         Set *set = new Set(type, array, 1);
 242         Element *element = new ElementConst(value, set);
 243         Element *e = elemMap.get(element);
 244         if (e == NULL) {
 245                 allSets.push(set);
 246                 allElements.push(element);
 247                 elemMap.put(element, element);
 248                 return element;
 249         } else {
 250                 delete set;
 251                 delete element;
 252                 return e;
 253         }
 254 }
 255
 256
 257 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
 258         ASSERT(numArrays == 2);
 259         Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
 260         Element *e = elemMap.get(element);
 261         if (e == NULL) {
 262                 element->updateParents();
 263                 allElements.push(element);
 264                 elemMap.put(element, element);
 265                 return element;
 266         } else {
 267                 delete element;
 268                 return e;
 269         }
 270 }
 271
 272 Function *CSolver::createFunctionOperator(ArithOp op, Set *range, OverFlowBehavior overflowbehavior) {
 273         Function *function = new FunctionOperator(op, range, overflowbehavior);
 274         allFunctions.push(function);
 275         return function;
 276 }
 277
 278 Predicate *CSolver::createPredicateOperator(CompOp op) {
 279         Predicate *predicate = new PredicateOperator(op);
 280         allPredicates.push(predicate);
 281         return predicate;
 282 }
 283
 284 Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavior) {
 285         Predicate *predicate = new PredicateTable(table, behavior);
 286         allPredicates.push(predicate);
 287         return predicate;
 288 }
 289
 290 Table *CSolver::createTable(Set *range) {
 291         Table *table = new Table(range);
 292         allTables.push(table);
 293         return table;
 294 }
 295
 296 Table *CSolver::createTableForPredicate() {
 297         return createTable(NULL);
 298 }
 299
 300 void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
 301         table->addNewTableEntry(inputs, inputSize, result);
 302 }
 303
 304 Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
 305         Function *function = new FunctionTable(table, behavior);
 306         allFunctions.push(function);
 307         return function;
 308 }
 309
 310 BooleanEdge CSolver::getBooleanVar(VarType type) {
 311         Boolean *boolean = new BooleanVar(type);
 312         allBooleans.push(boolean);
 313         if(!booleanVarUsed)
 314                 booleanVarUsed = true;
 315         return BooleanEdge(boolean);
 316 }
 317
 318 BooleanEdge CSolver::getBooleanTrue() {
 319         return boolTrue;
 320 }
 321
 322 BooleanEdge CSolver::getBooleanFalse() {
 323         return boolFalse;
 324 }
 325
 326 BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
 327         return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL));
 328 }
 329
 330 BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) {
 331         BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
 332         Boolean *b = boolMap.get(boolean);
 333         if (b == NULL) {
 334                 boolean->updateParents();
 335                 boolMap.put(boolean, boolean);
 336                 allBooleans.push(boolean);
 337                 return BooleanEdge(boolean);
 338         } else {
 339                 delete boolean;
 340                 return BooleanEdge(b);
 341         }
 342 }
 343
 344 bool CSolver::isTrue(BooleanEdge b) {
 345         return b.isNegated() ? b->isFalse() : b->isTrue();
 346 }
 347
 348 bool CSolver::isFalse(BooleanEdge b) {
 349         return b.isNegated() ? b->isTrue() : b->isFalse();
 350 }
 351
 352 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
 353         BooleanEdge array[] = {arg1, arg2};
 354         return applyLogicalOperation(op, array, 2);
 355 }
 356
 357 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
 358         BooleanEdge array[] = {arg};
 359         return applyLogicalOperation(op, array, 1);
 360 }
 361
 362 static int booleanEdgeCompares(const void *p1, const void *p2) {
 363         BooleanEdge be1 = *(BooleanEdge const *) p1;
 364         BooleanEdge be2 = *(BooleanEdge const *) p2;
 365         uint64_t b1 = be1->id;
 366         uint64_t b2 = be2->id;
 367         if (b1 < b2)
 368                 return -1;
 369         else if (b1 == b2)
 370                 return 0;
 371         else
 372                 return 1;
 373 }
 374
 375 BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
 376         BooleanEdge newarray[asize];
 377         memcpy(newarray, array, asize * sizeof(BooleanEdge));
 378         for (uint i = 0; i < asize; i++) {
 379                 BooleanEdge b = newarray[i];
 380                 if (b->type == LOGICOP) {
 381                         if (((BooleanLogic *) b.getBoolean())->replaced) {
 382                                 newarray[i] = doRewrite(newarray[i]);
 383                                 i--;//Check again
 384                         }
 385                 }
 386         }
 387         return applyLogicalOperation(op, newarray, asize);
 388 }
 389
 390 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
 391         BooleanEdge newarray[asize];
 392         switch (op) {
 393         case SATC_NOT: {
 394                 return array[0].negate();
 395         }
 396         case SATC_IFF: {
 397                 for (uint i = 0; i < 2; i++) {
 398                         if (isTrue(array[i])) { // It can be undefined
 399                                 return array[1 - i];
 400                         } else if (isFalse(array[i])) {
 401                                 newarray[0] = array[1 - i];
 402                                 return applyLogicalOperation(SATC_NOT, newarray, 1);
 403                         } else if (array[i]->type == LOGICOP) {
 404                                 BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
 405                                 if (b->replaced) {
 406                                         return rewriteLogicalOperation(op, array, asize);
 407                                 }
 408                         }
 409                 }
 410                 break;
 411         }
 412         case SATC_OR: {
 413                 for (uint i = 0; i < asize; i++) {
 414                         newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
 415                 }
 416                 return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
 417         }
 418         case SATC_AND: {
 419                 uint newindex = 0;
 420                 for (uint i = 0; i < asize; i++) {
 421                         BooleanEdge b = array[i];
 422                         if (b->type == LOGICOP) {
 423                                 if (((BooleanLogic *)b.getBoolean())->replaced)
 424                                         return rewriteLogicalOperation(op, array, asize);
 425                         }
 426                         if (isTrue(b))
 427                                 continue;
 428                         else if (isFalse(b)) {
 429                                 return boolFalse;
 430                         } else
 431                                 newarray[newindex++] = b;
 432                 }
 433                 if (newindex == 0) {
 434                         return boolTrue;
 435                 } else if (newindex == 1) {
 436                         return newarray[0];
 437                 } else {
 438                         bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
 439                         array = newarray;
 440                         asize = newindex;
 441                 }
 442                 break;
 443         }
 444         case SATC_XOR: {
 445                 //handle by translation
 446                 return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
 447         }
 448         case SATC_IMPLIES: {
 449                 //handle by translation
 450                 return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
 451         }
 452         }
 453
 454         ASSERT(asize != 0);
 455         Boolean *boolean = new BooleanLogic(this, op, array, asize);
 456         Boolean *b = boolMap.get(boolean);
 457         if (b == NULL) {
 458                 boolean->updateParents();
 459                 boolMap.put(boolean, boolean);
 460                 allBooleans.push(boolean);
 461                 return BooleanEdge(boolean);
 462         } else {
 463                 delete boolean;
 464                 return BooleanEdge(b);
 465         }
 466 }
 467
 468 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
 469         //      ASSERT(first != second);
 470         if (first == second)
 471                 return getBooleanFalse();
 472
 473         bool negate = false;
 474         if (order->type == SATC_TOTAL) {
 475                 if (first > second) {
 476                         uint64_t tmp = first;
 477                         first = second;
 478                         second = tmp;
 479                         negate = true;
 480                 }
 481         }
 482         Boolean *constraint = new BooleanOrder(order, first, second);
 483         Boolean *b = boolMap.get(constraint);
 484
 485         if (b == NULL) {
 486                 allBooleans.push(constraint);
 487                 boolMap.put(constraint, constraint);
 488                 constraint->updateParents();
 489                 if (order->graph != NULL) {
 490                         OrderGraph *graph = order->graph;
 491                         OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
 492                         if (from != NULL) {
 493                                 OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
 494                                 if (to != NULL) {
 495                                         OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
 496                                         OrderEdge *invedge;
 497
 498                                         if (edge != NULL && edge->mustPos) {
 499                                                 replaceBooleanWithTrueNoRemove(constraint);
 500                                         } else if (edge != NULL && edge->mustNeg) {
 501                                                 replaceBooleanWithFalseNoRemove(constraint);
 502                                         } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
 503                                                                                  && invedge->mustPos) {
 504                                                 replaceBooleanWithFalseNoRemove(constraint);
 505                                         }
 506                                 }
 507                         }
 508                 }
 509         } else {
 510                 delete constraint;
 511                 constraint = b;
 512         }
 513
 514         BooleanEdge be = BooleanEdge(constraint);
 515         return negate ? be.negate() : be;
 516 }
 517
 518 void CSolver::addConstraint(BooleanEdge constraint) {
 519         if (isTrue(constraint))
 520                 return;
 521         else if (isFalse(constraint)) {
 522                 setUnSAT();
 523         }
 524         else {
 525                 if (constraint->type == LOGICOP) {
 526                         BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
 527                         if (!constraint.isNegated()) {
 528                                 if (b->op == SATC_AND) {
 529                                         uint size = b->inputs.getSize();
 530                                         //Handle potential concurrent modification
 531                                         BooleanEdge array[size];
 532                                         for (uint i = 0; i < size; i++) {
 533                                                 array[i] = b->inputs.get(i);
 534                                         }
 535                                         for (uint i = 0; i < size; i++) {
 536                                                 addConstraint(array[i]);
 537                                         }
 538                                         return;
 539                                 }
 540                         }
 541                         if (b->replaced) {
 542                                 addConstraint(doRewrite(constraint));
 543                                 return;
 544                         }
 545                 }
 546                 constraints.add(constraint);
 547                 Boolean *ptr = constraint.getBoolean();
 548
 549                 if (ptr->boolVal == BV_UNSAT) {
 550                         setUnSAT();
 551                 }
 552
 553                 replaceBooleanWithTrueNoRemove(constraint);
 554                 constraint->parents.clear();
 555         }
 556 }
 557
 558 Order *CSolver::createOrder(OrderType type, Set *set) {
 559         Order *order = new Order(type, set);
 560         allOrders.push(order);
 561         activeOrders.add(order);
 562         return order;
 563 }
 564
 565 /** Computes static ordering information to allow isTrue/isFalse
 566     queries on newly created orders to work. */
 567
 568 void CSolver::inferFixedOrder(Order *order) {
 569         if (order->graph != NULL) {
 570                 delete order->graph;
 571         }
 572         order->graph = buildMustOrderGraph(order);
 573         reachMustAnalysis(this, order->graph, true);
 574 }
 575
 576 void CSolver::inferFixedOrders() {
 577         SetIteratorOrder *orderit = activeOrders.iterator();
 578         while (orderit->hasNext()) {
 579                 Order *order = orderit->next();
 580                 inferFixedOrder(order);
 581         }
 582 }
 583
 584 int CSolver::solve() {
 585         long long startTime = getTimeNano();
 586         bool deleteTuner = false;
 587         if (tuner == NULL) {
 588                 tuner = new DefaultTuner();
 589                 deleteTuner = true;
 590         }
 591
 592
 593         {
 594                 SetIteratorOrder *orderit = activeOrders.iterator();
 595                 while (orderit->hasNext()) {
 596                         Order *order = orderit->next();
 597                         if (order->graph != NULL) {
 598                                 delete order->graph;
 599                                 order->graph = NULL;
 600                         }
 601                 }
 602                 delete orderit;
 603         }
 604         computePolarities(this);
 605         long long time1 = getTimeNano();
 606         model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
 607         Preprocess pp(this);
 608         pp.doTransform();
 609         long long time2 = getTimeNano();
 610         model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
 611
 612         DecomposeOrderTransform dot(this);
 613         dot.doTransform();
 614         time1 = getTimeNano();
 615         model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
 616
 617         IntegerEncodingTransform iet(this);
 618         iet.doTransform();
 619
 620         ElementOpt eop(this);
 621         eop.doTransform();
 622
 623         EncodingGraph eg(this);
 624         eg.encode();
 625
 626         naiveEncodingDecision(this);
 627 //      eg.validate();
 628
 629         VarOrderingOpt bor(this, satEncoder);
 630         bor.doTransform();
 631
 632         time2 = getTimeNano();
 633         model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
 634
 635         satEncoder->encodeAllSATEncoder(this);
 636         time1 = getTimeNano();
 637
 638         model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
 639
 640         model_print("Is problem UNSAT after encoding: %d\n", unsat);
 641         int result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
 642         model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
 643         time2 = getTimeNano();
 644         elapsedTime = time2 - startTime;
 645         model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
 646         if (deleteTuner) {
 647                 delete tuner;
 648                 tuner = NULL;
 649         }
 650         return result;
 651 }
 652
 653 void CSolver::printConstraints() {
 654         SetIteratorBooleanEdge *it = getConstraints();
 655         while (it->hasNext()) {
 656                 BooleanEdge b = it->next();
 657                 b.print();
 658         }
 659         delete it;
 660 }
 661
 662 void CSolver::printConstraint(BooleanEdge b) {
 663         b.print();
 664 }
 665
 666 uint64_t CSolver::getElementValue(Element *element) {
 667         switch (element->type) {
 668         case ELEMSET:
 669         case ELEMCONST:
 670         case ELEMFUNCRETURN:
 671                 return getElementValueSATTranslator(this, element);
 672         default:
 673                 ASSERT(0);
 674         }
 675         exit(-1);
 676 }
 677
 678 bool CSolver::getBooleanValue(BooleanEdge bedge) {
 679         Boolean *boolean = bedge.getBoolean();
 680         switch (boolean->type) {
 681         case BOOLEANVAR:
 682                 return getBooleanVariableValueSATTranslator(this, boolean);
 683         default:
 684                 ASSERT(0);
 685         }
 686         exit(-1);
 687 }
 688
 689 bool CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
 690         return order->encoding.resolver->resolveOrder(first, second);
 691 }
 692
 693 long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
 694
 695 long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
 696
 697 void CSolver::autoTune(uint budget) {
 698         AutoTuner *autotuner = new AutoTuner(budget);
 699         autotuner->addProblem(this);
 700         autotuner->tune();
 701         delete autotuner;
 702 }
 703
 704