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 void CSolver::mustHaveValue(Element *element){
 226         element->getElementEncoding()->anyValue = true;
 227 }
 228
 229 Set *CSolver::getElementRange (Element *element) {
 230         return element->getRange();
 231 }
 232
 233
 234 Element *CSolver::getElementConst(VarType type, uint64_t value) {
 235         uint64_t array[] = {value};
 236         Set *set = new Set(type, array, 1);
 237         Element *element = new ElementConst(value, set);
 238         Element *e = elemMap.get(element);
 239         if (e == NULL) {
 240                 allSets.push(set);
 241                 allElements.push(element);
 242                 elemMap.put(element, element);
 243                 return element;
 244         } else {
 245                 delete set;
 246                 delete element;
 247                 return e;
 248         }
 249 }
 250
 251
 252 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
 253         Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
 254         Element *e = elemMap.get(element);
 255         if (e == NULL) {
 256                 element->updateParents();
 257                 allElements.push(element);
 258                 elemMap.put(element, element);
 259                 return element;
 260         } else {
 261                 delete element;
 262                 return e;
 263         }
 264 }
 265
 266 Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
 267         Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior);
 268         allFunctions.push(function);
 269         return function;
 270 }
 271
 272 Predicate *CSolver::createPredicateOperator(CompOp op, Set **domain, uint numDomain) {
 273         Predicate *predicate = new PredicateOperator(op, domain,numDomain);
 274         allPredicates.push(predicate);
 275         return predicate;
 276 }
 277
 278 Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavior) {
 279         Predicate *predicate = new PredicateTable(table, behavior);
 280         allPredicates.push(predicate);
 281         return predicate;
 282 }
 283
 284 Table *CSolver::createTable(Set **domains, uint numDomain, Set *range) {
 285         Table *table = new Table(domains,numDomain,range);
 286         allTables.push(table);
 287         return table;
 288 }
 289
 290 Table *CSolver::createTableForPredicate(Set **domains, uint numDomain) {
 291         return createTable(domains, numDomain, NULL);
 292 }
 293
 294 void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
 295         table->addNewTableEntry(inputs, inputSize, result);
 296 }
 297
 298 Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
 299         Function *function = new FunctionTable(table, behavior);
 300         allFunctions.push(function);
 301         return function;
 302 }
 303
 304 BooleanEdge CSolver::getBooleanVar(VarType type) {
 305         Boolean *boolean = new BooleanVar(type);
 306         allBooleans.push(boolean);
 307         return BooleanEdge(boolean);
 308 }
 309
 310 BooleanEdge CSolver::getBooleanTrue() {
 311         return boolTrue;
 312 }
 313
 314 BooleanEdge CSolver::getBooleanFalse() {
 315         return boolFalse;
 316 }
 317
 318 BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
 319         return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL));
 320 }
 321
 322 BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) {
 323         BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
 324         Boolean *b = boolMap.get(boolean);
 325         if (b == NULL) {
 326                 boolean->updateParents();
 327                 boolMap.put(boolean, boolean);
 328                 allBooleans.push(boolean);
 329                 return BooleanEdge(boolean);
 330         } else {
 331                 delete boolean;
 332                 return BooleanEdge(b);
 333         }
 334 }
 335
 336 bool CSolver::isTrue(BooleanEdge b) {
 337         return b.isNegated() ? b->isFalse() : b->isTrue();
 338 }
 339
 340 bool CSolver::isFalse(BooleanEdge b) {
 341         return b.isNegated() ? b->isTrue() : b->isFalse();
 342 }
 343
 344 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
 345         BooleanEdge array[] = {arg1, arg2};
 346         return applyLogicalOperation(op, array, 2);
 347 }
 348
 349 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
 350         BooleanEdge array[] = {arg};
 351         return applyLogicalOperation(op, array, 1);
 352 }
 353
 354 static int booleanEdgeCompares(const void *p1, const void *p2) {
 355         BooleanEdge be1 = *(BooleanEdge const *) p1;
 356         BooleanEdge be2 = *(BooleanEdge const *) p2;
 357         uint64_t b1 = be1->id;
 358         uint64_t b2 = be2->id;
 359         if (b1 < b2)
 360                 return -1;
 361         else if (b1 == b2)
 362                 return 0;
 363         else
 364                 return 1;
 365 }
 366
 367 BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
 368         BooleanEdge newarray[asize];
 369         memcpy(newarray, array, asize * sizeof(BooleanEdge));
 370         for (uint i = 0; i < asize; i++) {
 371                 BooleanEdge b = newarray[i];
 372                 if (b->type == LOGICOP) {
 373                         if (((BooleanLogic *) b.getBoolean())->replaced) {
 374                                 newarray[i] = doRewrite(newarray[i]);
 375                                 i--;//Check again
 376                         }
 377                 }
 378         }
 379         return applyLogicalOperation(op, newarray, asize);
 380 }
 381
 382 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
 383         BooleanEdge newarray[asize];
 384         switch (op) {
 385         case SATC_NOT: {
 386                 return array[0].negate();
 387         }
 388         case SATC_IFF: {
 389                 for (uint i = 0; i < 2; i++) {
 390                         if (isTrue(array[i])) { // It can be undefined
 391                                 return array[1 - i];
 392                         } else if (isFalse(array[i])) {
 393                                 newarray[0] = array[1 - i];
 394                                 return applyLogicalOperation(SATC_NOT, newarray, 1);
 395                         } else if (array[i]->type == LOGICOP) {
 396                                 BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
 397                                 if (b->replaced) {
 398                                         return rewriteLogicalOperation(op, array, asize);
 399                                 }
 400                         }
 401                 }
 402                 break;
 403         }
 404         case SATC_OR: {
 405                 for (uint i = 0; i < asize; i++) {
 406                         newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
 407                 }
 408                 return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
 409         }
 410         case SATC_AND: {
 411                 uint newindex = 0;
 412                 for (uint i = 0; i < asize; i++) {
 413                         BooleanEdge b = array[i];
 414                         if (b->type == LOGICOP) {
 415                                 if (((BooleanLogic *)b.getBoolean())->replaced)
 416                                         return rewriteLogicalOperation(op, array, asize);
 417                         }
 418                         if (isTrue(b))
 419                                 continue;
 420                         else if (isFalse(b)) {
 421                                 return boolFalse;
 422                         } else
 423                                 newarray[newindex++] = b;
 424                 }
 425                 if (newindex == 0) {
 426                         return boolTrue;
 427                 } else if (newindex == 1) {
 428                         return newarray[0];
 429                 } else {
 430                         bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
 431                         array = newarray;
 432                         asize = newindex;
 433                 }
 434                 break;
 435         }
 436         case SATC_XOR: {
 437                 //handle by translation
 438                 return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
 439         }
 440         case SATC_IMPLIES: {
 441                 //handle by translation
 442                 return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
 443         }
 444         }
 445
 446         ASSERT(asize != 0);
 447         Boolean *boolean = new BooleanLogic(this, op, array, asize);
 448         Boolean *b = boolMap.get(boolean);
 449         if (b == NULL) {
 450                 boolean->updateParents();
 451                 boolMap.put(boolean, boolean);
 452                 allBooleans.push(boolean);
 453                 return BooleanEdge(boolean);
 454         } else {
 455                 delete boolean;
 456                 return BooleanEdge(b);
 457         }
 458 }
 459
 460 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
 461         //      ASSERT(first != second);
 462         if (first == second)
 463                 return getBooleanFalse();
 464
 465         bool negate = false;
 466         if (order->type == SATC_TOTAL) {
 467                 if (first > second) {
 468                         uint64_t tmp = first;
 469                         first = second;
 470                         second = tmp;
 471                         negate = true;
 472                 }
 473         }
 474         Boolean *constraint = new BooleanOrder(order, first, second);
 475         Boolean *b = boolMap.get(constraint);
 476
 477         if (b == NULL) {
 478                 allBooleans.push(constraint);
 479                 boolMap.put(constraint, constraint);
 480                 constraint->updateParents();
 481                 if (order->graph != NULL) {
 482                         OrderGraph *graph = order->graph;
 483                         OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
 484                         if (from != NULL) {
 485                                 OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
 486                                 if (to != NULL) {
 487                                         OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
 488                                         OrderEdge *invedge;
 489
 490                                         if (edge != NULL && edge->mustPos) {
 491                                                 replaceBooleanWithTrueNoRemove(constraint);
 492                                         } else if (edge != NULL && edge->mustNeg) {
 493                                                 replaceBooleanWithFalseNoRemove(constraint);
 494                                         } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
 495                                                                                  && invedge->mustPos) {
 496                                                 replaceBooleanWithFalseNoRemove(constraint);
 497                                         }
 498                                 }
 499                         }
 500                 }
 501         } else {
 502                 delete constraint;
 503                 constraint = b;
 504         }
 505
 506         BooleanEdge be = BooleanEdge(constraint);
 507         return negate ? be.negate() : be;
 508 }
 509
 510 void CSolver::addConstraint(BooleanEdge constraint) {
 511         if (isTrue(constraint))
 512                 return;
 513         else if (isFalse(constraint)) {
 514                 int t = 0;
 515                 setUnSAT();
 516         }
 517         else {
 518                 if (constraint->type == LOGICOP) {
 519                         BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
 520                         if (!constraint.isNegated()) {
 521                                 if (b->op == SATC_AND) {
 522                                         for (uint i = 0; i < b->inputs.getSize(); i++) {
 523                                                 addConstraint(b->inputs.get(i));
 524                                         }
 525                                         return;
 526                                 }
 527                         }
 528                         if (b->replaced) {
 529                                 addConstraint(doRewrite(constraint));
 530                                 return;
 531                         }
 532                 }
 533                 constraints.add(constraint);
 534                 Boolean *ptr = constraint.getBoolean();
 535
 536                 if (ptr->boolVal == BV_UNSAT) {
 537                         setUnSAT();
 538                 }
 539
 540                 replaceBooleanWithTrueNoRemove(constraint);
 541                 constraint->parents.clear();
 542         }
 543 }
 544
 545 Order *CSolver::createOrder(OrderType type, Set *set) {
 546         Order *order = new Order(type, set);
 547         allOrders.push(order);
 548         activeOrders.add(order);
 549         return order;
 550 }
 551
 552 /** Computes static ordering information to allow isTrue/isFalse
 553     queries on newly created orders to work. */
 554
 555 void CSolver::inferFixedOrder(Order *order) {
 556         if (order->graph != NULL) {
 557                 delete order->graph;
 558         }
 559         order->graph = buildMustOrderGraph(order);
 560         reachMustAnalysis(this, order->graph, true);
 561 }
 562
 563 void CSolver::inferFixedOrders() {
 564         SetIteratorOrder *orderit = activeOrders.iterator();
 565         while (orderit->hasNext()) {
 566                 Order *order = orderit->next();
 567                 inferFixedOrder(order);
 568         }
 569 }
 570
 571 #define NANOSEC 1000000000.0
 572 int CSolver::solve() {
 573         long long starttime = getTimeNano();
 574         bool deleteTuner = false;
 575         if (tuner == NULL) {
 576                 tuner = new DefaultTuner();
 577                 deleteTuner = true;
 578         }
 579
 580
 581         {
 582                 SetIteratorOrder *orderit = activeOrders.iterator();
 583                 while (orderit->hasNext()) {
 584                         Order *order = orderit->next();
 585                         if (order->graph != NULL) {
 586                                 delete order->graph;
 587                                 order->graph = NULL;
 588                         }
 589                 }
 590                 delete orderit;
 591         }
 592         computePolarities(this);
 593         long long time2 = getTimeNano();
 594         model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
 595         Preprocess pp(this);
 596         pp.doTransform();
 597         long long time3 = getTimeNano();
 598         model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC);
 599
 600         DecomposeOrderTransform dot(this);
 601         dot.doTransform();
 602         long long time4 = getTimeNano();
 603         model_print("Decompose Order: %f\n", (time4 - time3) / NANOSEC);
 604
 605         IntegerEncodingTransform iet(this);
 606         iet.doTransform();
 607
 608         EncodingGraph eg(this);
 609         eg.buildGraph();
 610         eg.encode();
 611
 612         naiveEncodingDecision(this);
 613         long long time5 = getTimeNano();
 614         model_print("Encoding Graph Time: %f\n", (time5 - time4) / NANOSEC);
 615
 616         long long startTime = getTimeNano();
 617         satEncoder->encodeAllSATEncoder(this);
 618         long long endTime = getTimeNano();
 619
 620         elapsedTime = endTime - startTime;
 621         model_print("Elapse Encode time: %f\n", elapsedTime / NANOSEC);
 622
 623         model_print("Is problem UNSAT after encoding: %d\n", unsat);
 624         int result = unsat ? IS_UNSAT : satEncoder->solve();
 625         model_print("Result Computed in SAT solver: %d\n", result);
 626
 627         if (deleteTuner) {
 628                 delete tuner;
 629                 tuner = NULL;
 630         }
 631         return result;
 632 }
 633
 634 void CSolver::printConstraints() {
 635         SetIteratorBooleanEdge *it = getConstraints();
 636         while (it->hasNext()) {
 637                 BooleanEdge b = it->next();
 638                 if (b.isNegated())
 639                         model_print("!");
 640                 b->print();
 641                 model_print("\n");
 642         }
 643         delete it;
 644 }
 645
 646 void CSolver::printConstraint(BooleanEdge b) {
 647         if (b.isNegated())
 648                 model_print("!");
 649         b->print();
 650         model_print("\n");
 651 }
 652
 653 uint64_t CSolver::getElementValue(Element *element) {
 654         switch (element->type) {
 655         case ELEMSET:
 656         case ELEMCONST:
 657         case ELEMFUNCRETURN:
 658                 return getElementValueSATTranslator(this, element);
 659         default:
 660                 ASSERT(0);
 661         }
 662         exit(-1);
 663 }
 664
 665 bool CSolver::getBooleanValue(BooleanEdge bedge) {
 666         Boolean *boolean = bedge.getBoolean();
 667         switch (boolean->type) {
 668         case BOOLEANVAR:
 669                 return getBooleanVariableValueSATTranslator(this, boolean);
 670         default:
 671                 ASSERT(0);
 672         }
 673         exit(-1);
 674 }
 675
 676 bool CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
 677         return order->encoding.resolver->resolveOrder(first, second);
 678 }
 679
 680 long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
 681
 682 long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
 683
 684 void CSolver::autoTune(uint budget) {
 685         AutoTuner *autotuner = new AutoTuner(budget);
 686         autotuner->addProblem(this);
 687         autotuner->tune();
 688         delete autotuner;
 689 }
 690
 691 //Set* CSolver::addItemsToRange(Element* element, uint num, ...){
 692 //        va_list args;
 693 //        va_start(args, num);
 694 //        element->getRange()
 695 //        uint setSize = set->getSize();
 696 //        uint newSize = setSize+ num;
 697 //        uint64_t members[newSize];
 698 //        for(uint i=0; i<setSize; i++){
 699 //                members[i] = set->getElement(i);
 700 //        }
 701 //        for( uint i=0; i< num; i++){
 702 //                uint64_t arg = va_arg(args, uint64_t);
 703 //                members[setSize+i] = arg;
 704 //        }
 705 //        va_end(args);
 706 //        return createSet(set->getType(), members, newSize);
 707 //}