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