zsolve/libzsolve.c

   1 /*
   2 4ti2 -- A software package for algebraic, geometric and combinatorial
   3 problems on linear spaces.
   4
   5 Copyright (C) 2006 4ti2 team.
   6 Main author(s): Matthias Walter.
   7
   8 This program is free software; you can redistribute it and/or
   9 modify it under the terms of the GNU General Public License
  10 as published by the Free Software Foundation; either version 2
  11 of the License, or (at your option) any later version.
  12
  13 This program is distributed in the hope that it will be useful,
  14 but WITHOUT ANY WARRANTY; without even the implied warranty of
  15 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
  16 GNU General Public License for more details.
  17
  18 You should have received a copy of the GNU General Public License
  19 along with this program; if not, write to the Free Software
  20 Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
  21 */
  22
  23 #include <assert.h>
  24 #include <stdlib.h>
  25
  26 #include "libzsolve.h"
  27 #include "valuetrees.h"
  28 #include "lattice.h"
  29
  30 int chooseNext(ZSolveContext ctx, Vector possible, int value)
  31 {
  32         int i,j,zeros;
  33
  34         assert(possible);
  35
  36         if (value<0)
  37                 value = 0;
  38         for (i=0; i<ctx->Variables; i++)
  39         {
  40                 possible[i] = (possible[i]==value) ? 1 : 0;
  41                 zeros = 1;
  42                 for (j=0; j<ctx->Lattice->Size; j++)
  43                         if (ctx->Lattice->Data[j][i]==0)
  44                                 zeros++;
  45                 possible[i] *= zeros;
  46         }
  47
  48         j = -1;
  49         for (i=0; i<ctx->Variables; i++)
  50                 if (possible[i]>0 && (j<0 || possible[i]>possible[j]))
  51                         j = i;
  52
  53         return j;
  54 }
  55
  56 int nextVariable(ZSolveContext ctx)
  57 {
  58         IndexArray Zeros;
  59         Vector gcds;
  60         int i,j,k,col = -1;
  61         int factor, value;
  62         bool flag;
  63
  64         assert(ctx);
  65
  66         // Zeros is the list of vectors v with ||v|| = 0
  67         Zeros = createIndexArray();
  68         for (i=0; i<ctx->Lattice->Size; i++)
  69                 if (normVector(ctx->Lattice->Data[i], ctx->Current)==0)
  70                         appendToIndexArray(Zeros, i);
  71
  72         if (Zeros->Size)
  73         {
  74                 gcds = createVector(ctx->Variables);
  75                 for (i=0; i<ctx->Variables; i++)
  76                         gcds[i] = -1;
  77                 value = -1;
  78                 for (i=ctx->Current; i<ctx->Variables; i++)
  79                 {
  80                         if (!ctx->Lattice->Properties[i].Free)
  81                         {
  82                                 gcds[i] = abs(ctx->Lattice->Data[Zeros->Data[0]][i]);
  83                                 for (j=1; j<Zeros->Size; j++)
  84                                         gcds[i] = gcd(gcds[i], abs(ctx->Lattice->Data[Zeros->Data[j]][i]));
  85                                 if ((value<0 || gcds[i]<value) && gcds[i]>0)
  86                                         value = gcds[i];
  87                         }
  88                 }
  89
  90                 col = chooseNext(ctx, gcds, value);
  91
  92                 deleteVector(gcds);
  93                 if (col<0)
  94                         return -1;
  95                 // minimize Zeros
  96                 do
  97                 {
  98                         j = -1;
  99                         for (i=0; i<Zeros->Size; i++)
 100                         {
 101                                 if (ctx->Lattice->Data[Zeros->Data[i]][col]!=0 && (j<0 || abs(ctx->Lattice->Data[Zeros->Data[i]][col])<abs(ctx->Lattice->Data[Zeros->Data[j]][col])))
 102                                         j = i;
 103                         }
 104                         if (j<0)
 105                                 break;
 106                         j = Zeros->Data[j];
 107 /*
 108                         printf("Current Norm[0]: ");
 109                         printVector(Zeros->Data, Zeros->Size, VECTOR_NEWLINE);
 110                         printf("ctx->Lattice:\n");
 111                         printVectorArray(ctx->Lattice, VECTORARRAY_INDENT);
 112                         printf("Reducing Slot: Row = %d, Col = %d\n\n", j, col);
 113 */
 114                         flag = false;
 115                         for (i=0; i<ctx->Lattice->Size; i++)
 116                         {
 117                                 if (ctx->Lattice->Data[i][col]!=0 && i!=j)
 118                                 {
 119                                         factor = ctx->Lattice->Data[i][col] / ctx->Lattice->Data[j][col];
 120                                         for (k=0; k<ctx->Variables; k++)
 121                                                 if (ctx->Lattice->Data[i][k]+ctx->Lattice->Data[j][k]!=0)
 122                                                         break;
 123                                         if (k==ctx->Variables)
 124                                                 continue;
 125                                         if (factor!=0)
 126                                         {
 127 //                                              printf("factor = %d\n", factor);
 128                                                 flag = true;
 129                                         }
 130                                         for (k=0; k<ctx->Variables; k++)
 131                                                 ctx->Lattice->Data[i][k] -= factor * ctx->Lattice->Data[j][k];
 132                                 }
 133                         }
 134                 } while (flag);
 135         }
 136         else
 137         {
 138                 gcds = createVector(ctx->Variables);
 139                 for (i=0; i<ctx->Variables; i++)
 140                         gcds[i] = (i<ctx->Current || ctx->Lattice->Properties[i].Free) ? 0 : 1;
 141                 col = chooseNext(ctx, gcds, 1);
 142                 deleteVector(gcds);
 143         }
 144
 145         deleteIndexArray(Zeros);
 146
 147         return col;
 148 }
 149
 150 void filterLimits(ZSolveContext ctx)
 151 {
 152         int i;
 153
 154         assert(ctx);
 155
 156         for (i=0; i<ctx->Lattice->Size; i++)
 157         {
 158                 if (ctx->Lattice->Properties[ctx->Current].Lower>ctx->Lattice->Data[i][ctx->Current] || ctx->Lattice->Properties[ctx->Current].Upper<ctx->Lattice->Data[i][ctx->Current])
 159                 {
 160                         ctx->Lattice->Size--;
 161                         deleteVector(ctx->Lattice->Data[i]);
 162                         ctx->Lattice->Data[i] = ctx->Lattice->Data[ctx->Lattice->Size];
 163                         i--;
 164                 }
 165         }
 166         ctx->Lattice->Memory = ctx->Lattice->Size;
 167         ctx->Lattice->Data = (Vector *)realloc(ctx->Lattice->Data, ctx->Lattice->Memory * sizeof(Vector));
 168 }
 169
 170 void zsolveLogCallbackDefault(FILE *stream, int level, int type, int var, int sum, int norm, int vectors, CPUTime alltime, CPUTime steptime)
 171 {
 172         switch (level)
 173         {
 174         case 1:
 175                 if (type == ZSOLVE_LOG_VARIABLE_STARTED)
 176                         fprintf(stream, "Appending variable %d... ", var+1);
 177                 else if (type == ZSOLVE_LOG_VARIABLE_FINISHED)
 178                 {
 179                         fprintf(stream, "Solutions: %d, Step: ", vectors);
 180                         fprintCPUTime(stream, steptime);
 181                         fprintf(stream, ", Time: ");
 182                         fprintCPUTime(stream, alltime);
 183                         fprintf(stream, "\n");
 184                 }
 185         break;
 186         case 2:
 187                 if (type == ZSOLVE_LOG_VARIABLE_STARTED)
 188                         fprintf(stream, "%sAppending variable %d.\n\n", var ? "\n" : "", var+1);
 189                 else if (type == ZSOLVE_LOG_VARIABLE_FINISHED)
 190                 {
 191                         fprintf(stream, "\nFinished variable %d. Solutions: %d, Step: ", var+1, vectors);
 192                         fprintCPUTime(stream, steptime);
 193                         fprintf(stream, ", Time: ");
 194                         fprintCPUTime(stream, alltime);
 195                         fprintf(stream, "\n");
 196                 }
 197                 else if (type == ZSOLVE_LOG_SUM_STARTED)
 198                         fprintf(stream, " Var = %d, Sum = %d... ", var+1, sum);
 199                 else if (type == ZSOLVE_LOG_SUM_FINISHED)
 200                 {
 201                         fprintf(stream, "Solutions: %d, Step: ", vectors);
 202                         fprintCPUTime(stream, steptime);
 203                         fprintf(stream, ", Time: ");
 204                         fprintCPUTime(stream, alltime);
 205                         fprintf(stream, "\n");
 206                 }
 207         break;
 208         case 3:
 209                 if (type == ZSOLVE_LOG_VARIABLE_STARTED)
 210                         fprintf(stream, "%sAppending variable %d.\n\n", var ? "\n" : "", var+1);
 211                 else if (type == ZSOLVE_LOG_VARIABLE_FINISHED)
 212                 {
 213                         fprintf(stream, "\nFinished variable %d. Solutions: %d, Step: ", var+1, vectors);
 214                         fprintCPUTime(stream, steptime);
 215                         fprintf(stream, ", Time: ");
 216                         fprintCPUTime(stream, alltime);
 217                         fprintf(stream, "\n");
 218                 }
 219                 else if (type == ZSOLVE_LOG_SUM_STARTED)
 220                         fprintf(stream, "%s Var = %d, Sum = %d.\n\n", sum ? "\n" : "", var+1, sum);
 221                 else if (type == ZSOLVE_LOG_SUM_FINISHED)
 222                 {
 223                         fprintf(stream, "\n Finished sum %d. Solutions: %d, Step: ", sum, vectors);
 224                         fprintCPUTime(stream, steptime);
 225                         fprintf(stream, ", Time: ");
 226                         fprintCPUTime(stream, alltime);
 227                         fprintf(stream, "\n");
 228                 }
 229                 else if (type == ZSOLVE_LOG_NORM_STARTED)
 230                         fprintf(stream, " Var = %d, Norm = %d + %d... ", var+1, norm, sum-norm);
 231                 else if (type == ZSOLVE_LOG_NORM_FINISHED)
 232                 {
 233                         fprintf(stream, "Solutions: %d, Step: ", vectors);
 234                         fprintCPUTime(stream, steptime);
 235                         fprintf(stream, ", Time: ");
 236                         fprintCPUTime(stream, alltime);
 237                         fprintf(stream, "\n");
 238                 }
 239         break;
 240         }
 241         if (level>0)
 242         {
 243                 if (type == ZSOLVE_LOG_STARTED)
 244                 {
 245                         // need linearsystem - maybe with va
 246                 }
 247                 else if (type == ZSOLVE_LOG_RESUMED)
 248                 {
 249                         fprintf(stream, "Resuming from backup, starting at Var = %d, Norm = %d + %d... Solutions: %d, Time: ", var, norm, sum - norm, vectors);
 250                         fprintCPUTime(stream, getCPUTime() - alltime);
 251                         fprintf(stream, "\n\n");
 252                 }
 253                 else if (type == ZSOLVE_LOG_FINISHED)
 254                 {
 255                         // need homs / inhoms - maybe with va
 256                 }
 257         }
 258         if (stream)
 259                 fflush(stream);
 260
 261 }
 262
 263 void splitLog(ZSolveContext ctx, int type, CPUTime steptime)
 264 {
 265         CPUTime currenttime = getCPUTime();
 266
 267         if (ctx->LogCallback)
 268         {
 269                 ctx->LogCallback(stdout, ctx->Verbosity, type, ctx->Current, ctx->SumNorm, ctx->FirstNorm, ctx->Lattice->Size, maxd(currenttime - ctx->AllTime, 0.0), maxd(steptime, 0.0));
 270                 if (ctx->LogFile)
 271                         ctx->LogCallback(ctx->LogFile, ctx->LogLevel, type, ctx->Current, ctx->SumNorm, ctx->FirstNorm, ctx->Lattice->Size, maxd(currenttime - ctx->AllTime, 0.0), maxd(steptime, 0.0));
 272         }
 273 }
 274
 275 void backupZSolveContext(FILE *stream, ZSolveContext ctx)
 276 {
 277         CPUTime currenttime = getCPUTime();
 278
 279         assert(stream);
 280         assert(ctx);
 281
 282         fprintf(stream, "%d %d %d\n%d\n\n", ctx->Current, ctx->SumNorm, ctx->FirstNorm, ctx->Symmetric);
 283
 284         fprintf(stream, "%d %d %d\n\n", ctx->Verbosity, ctx->LogLevel, ctx->BackupTime);
 285
 286         fprintf(stream, "%.2f %.2f %.2f %.2f\n\n" , currenttime - ctx->AllTime, currenttime - ctx->VarTime, currenttime - ctx->SumTime, currenttime - ctx->NormTime);
 287
 288         fprintVectorArray(stream, ctx->Lattice, true);
 289 }
 290
 291 int originalCompare(int a, int b)
 292 {
 293         if (a>=0 && b<0)
 294                 return -1;
 295         if (a<0 && b>=0)
 296                 return 1;
 297         return a-b;
 298 }
 299
 300 ZSolveContext createZSolveContextFromSystem(LinearSystem initialsystem, FILE *logfile, int loglevel, int verbosity, ZSolveLogCallback logcallback, ZSolveBackupCallback backupcallback)
 301 {
 302         ZSolveContext ctx;
 303         LinearSystem finalsystem;
 304
 305         ctx = (ZSolveContext)malloc(sizeof(zsolvecontext_t));
 306         if (ctx==NULL)
 307         {
 308                 fprintf(stderr, "Fatal Error (%s/%d): Could not allocate memory for ZSolveContext in createZSolveContextFromSystem!\n", __FILE__, __LINE__);
 309                 exit(1);
 310         }
 311
 312         ctx->BackupTime = 0;
 313         ctx->Verbosity = verbosity;
 314         ctx->LogLevel = loglevel;
 315         ctx->LogFile = logfile;
 316
 317         if (ctx->Verbosity>0)
 318         {
 319                 printf("Linear integer system to solve:\n\n");
 320                 printLinearSystem(initialsystem);
 321         }
 322         if (ctx->LogLevel>0)
 323         {
 324                 fprintf(ctx->LogFile, "Linear integer system to solve:\n\n");
 325                 fprintLinearSystem(ctx->LogFile, initialsystem);
 326         }
 327
 328         finalsystem = homogenizeLinearSystem(initialsystem);
 329         deleteLinearSystem(initialsystem);
 330
 331         if (ctx->Verbosity>0)
 332         {
 333                 printf("\nLinear integer system of homogeneous equalities to solve:\n\n");
 334                 printLinearSystem(finalsystem);
 335                 printf("\n\n");
 336         }
 337         if (ctx->LogLevel>0)
 338         {
 339                 fprintf(ctx->LogFile, "\nLinear integer system of homogeneous equalities to solve:\n\n");
 340                 fprintLinearSystem(ctx->LogFile, finalsystem);
 341                 fprintf(ctx->LogFile, "\n\n");
 342         }
 343
 344         ctx->Lattice = generateLattice(finalsystem);
 345         deleteLinearSystem(finalsystem);
 346
 347         // sort 0, 1, 2, ... , -2, -2, -2, -2, -1 (original order, then slackvars, then -b)
 348
 349         sortVectorArrayColumns(ctx->Lattice, originalCompare);
 350
 351         ctx->Variables = ctx->Lattice->Variables;
 352         ctx->MaxNorm = 0;
 353         ctx->Symmetric = true;
 354         ctx->Current = 0;
 355         ctx->SumNorm = 0;
 356         ctx->FirstNorm = 0;
 357         ctx->AllTime = getCPUTime();
 358         ctx->BackupCallback = backupcallback;
 359         ctx->LogCallback = logcallback;
 360         ctx->Homs = NULL;
 361         ctx->Inhoms = NULL;
 362         ctx->Frees = NULL;
 363         ctx->Graver = NULL;
 364
 365         return ctx;
 366 }
 367
 368 ZSolveContext createZSolveContextFromLattice(VectorArray lattice, FILE *logfile, int loglevel, int verbosity, ZSolveLogCallback logcallback, ZSolveBackupCallback backupcallback)
 369 {
 370         ZSolveContext ctx;
 371
 372         assert(lattice);
 373
 374         ctx = (ZSolveContext)malloc(sizeof(zsolvecontext_t));
 375         if (ctx==NULL)
 376         {
 377                 fprintf(stderr, "Fatal Error (%s/%d): Could not allocate memory for ZSolveContext in createZSolveContextFromLattice!\n", __FILE__, __LINE__);
 378                 exit(1);
 379         }
 380
 381         ctx->BackupTime = 0;
 382         ctx->Verbosity = verbosity;
 383         ctx->LogLevel = loglevel;
 384         ctx->LogFile = logfile;
 385         ctx->Lattice = lattice;
 386         ctx->Variables = ctx->Lattice->Variables;
 387         ctx->MaxNorm = 0;
 388         ctx->Symmetric = true;
 389         ctx->Current = 0;
 390         ctx->SumNorm = 0;
 391         ctx->FirstNorm = 0;
 392         ctx->AllTime = getCPUTime();
 393         ctx->BackupCallback = backupcallback;
 394         ctx->LogCallback = logcallback;
 395         ctx->Homs = NULL;
 396         ctx->Inhoms = NULL;
 397         ctx->Frees = NULL;
 398         ctx->Graver = NULL;
 399
 400         return ctx;
 401 }
 402
 403 ZSolveContext createZSolveContextFromBackup(FILE *stream, ZSolveLogCallback logcallback, ZSolveBackupCallback backupcallback)
 404 {
 405         ZSolveContext ctx;
 406         CPUTime currenttime = getCPUTime();
 407
 408         assert(stream);
 409
 410         ctx = (ZSolveContext)malloc(sizeof(zsolvecontext_t));
 411         if (ctx==NULL)
 412         {
 413                 fprintf(stderr, "Fatal Error (%s/%d): Could not allocate memory for ZSolveContext in createZSolveContextFromBackup!\n", __FILE__, __LINE__);
 414                 exit(1);
 415         }
 416
 417         fscanf(stream, "%d %d %d %d", &(ctx->Current), &(ctx->SumNorm), &(ctx->FirstNorm), &(ctx->Symmetric));
 418         ctx->SecondNorm = ctx->SumNorm - ctx->FirstNorm;
 419
 420         fscanf(stream, "%d %d %d", &(ctx->Verbosity), &(ctx->LogLevel), &(ctx->BackupTime));
 421
 422         fscanf(stream, "%lf %lf %lf %lf", &(ctx->AllTime), &(ctx->VarTime), &(ctx->SumTime), &(ctx->NormTime));
 423         ctx->AllTime = currenttime - ctx->AllTime;
 424         ctx->VarTime = currenttime - ctx->VarTime;
 425         ctx->SumTime = currenttime - ctx->SumTime;
 426         ctx->NormTime = currenttime - ctx->NormTime;
 427
 428         ctx->Lattice = readVectorArray(stream, true);
 429
 430         ctx->Variables = ctx->Lattice->Variables;
 431
 432         ctx->BackupCallback = backupcallback;
 433         ctx->LogCallback = logcallback;
 434         ctx->Homs = NULL;
 435         ctx->Inhoms = NULL;
 436         ctx->Frees = NULL;
 437         ctx->Graver = NULL;
 438
 439         return ctx;
 440 }
 441
 442 void zsolveSystem(ZSolveContext ctx, bool appendnegatives)
 443 {
 444         int next;
 445         int split;
 446         int count;
 447         int i,j,k;
 448         bool is_hom, is_free, has_symmetric;
 449         int lex_cmp;
 450         Vector vector;
 451         CPUTime lastbackup = getCPUTime();
 452
 453         if (appendnegatives)
 454                 appendVectorArrayNegatives(ctx->Lattice);
 455
 456         ctx->Sum = createVector(ctx->Variables);
 457
 458         if (ctx->SumNorm != 0)
 459                 createValueTrees(ctx);
 460
 461         while (ctx->Current < ctx->Lattice->Variables)
 462         {
 463                 if (ctx->BackupTime > 0 && ctx->BackupCallback && (getCPUTime() - lastbackup >= (double)ctx->BackupTime))
 464                 {
 465                         ctx->BackupCallback(ctx);
 466                         lastbackup = getCPUTime();
 467                 }
 468
 469                 if (ctx->SumNorm == 0) // start of var loop
 470                 {
 471                         ctx->VarTime = getCPUTime();
 472                         next = nextVariable(ctx);
 473 //                      printf("next variable = %d\n", next);
 474                         if (next<0)
 475                                 break;
 476                         splitLog(ctx, ZSOLVE_LOG_VARIABLE_STARTED, 0.0);
 477                         swapVectorArrayColumns(ctx->Lattice, next, ctx->Current);
 478 //                      printf("after next_var_swap:\n");
 479 //                      printVectorArray(ctx->Lattice, true);
 480                         createValueTrees(ctx);
 481                 }
 482
 483                 if (ctx->FirstNorm == 0) // start of sum loop
 484                 {
 485                         ctx->SumTime = getCPUTime();
 486                         splitLog(ctx, ZSOLVE_LOG_SUM_STARTED, 0.0);
 487                 }
 488
 489                 // start of norm loop
 490
 491                 ctx->SecondNorm = ctx->SumNorm - ctx->FirstNorm;
 492                 ctx->NormTime = getCPUTime();
 493                 splitLog(ctx, ZSOLVE_LOG_NORM_STARTED, 0.0);
 494
 495                 if (ctx->FirstNorm <= ctx->MaxNorm && ctx->SecondNorm <= ctx->MaxNorm && ctx->Norm[ctx->FirstNorm]!=NULL && ctx->Norm[ctx->SecondNorm]!=NULL)
 496                 {
 497                         // start completition procedure
 498                         completeValueTrees(ctx, ctx->FirstNorm, ctx->SumNorm - ctx->FirstNorm);
 499                 }
 500
 501                 // end of norm loop
 502
 503                 splitLog(ctx, ZSOLVE_LOG_NORM_FINISHED, ctx->NormTime);
 504                 ctx->FirstNorm++;
 505
 506                 if (ctx->FirstNorm > ctx->SumNorm/2) // end of sum loop?
 507                 {
 508                         splitLog(ctx, ZSOLVE_LOG_SUM_FINISHED, ctx->SumTime);
 509                         ctx->SumNorm++;
 510
 511                         if (ctx->SumNorm > 2*ctx->MaxNorm) // end of var loop?
 512                         {
 513                                 deleteValueTrees(ctx);
 514                                 if (ctx->Lattice->Properties[ctx->Current].Lower+ctx->Lattice->Properties[ctx->Current].Upper!=0)
 515                                         ctx->Symmetric = false;
 516                                 filterLimits(ctx);
 517                                 splitLog(ctx, ZSOLVE_LOG_VARIABLE_FINISHED, ctx->VarTime);
 518                                 ctx->Current++;
 519                                 ctx->SumNorm = 0;
 520
 521 //                              printf("After COMPLETE and FILTER\n");
 522 //                              printVectorArray(ctx->Lattice, true);
 523                         }
 524
 525                         ctx->FirstNorm = 0;
 526                 }
 527
 528         }
 529
 530         // algorithm completed
 531
 532         split = -1;
 533         count = 0;
 534
 535         // repermute
 536
 537         for (i = 0; i<ctx->Variables-1; i++) {
 538                 k = i;
 539                 for (j=i+1; j<ctx->Variables; j++) {
 540                         if (ctx->Lattice->Properties[k].Column < 0 || (ctx->Lattice->Properties[j].Column >=0 && ctx->Lattice->Properties[j].Column < ctx->Lattice->Properties[k].Column))
 541                                 k = j;
 542                 }
 543                 swapVectorArrayColumns(ctx->Lattice, i, k);
 544         }
 545
 546         // DEBUG
 547 //      printVectorArray(ctx->Lattice, true);
 548
 549         // split - variable for hom / inhom
 550         // count - number of columns for output
 551
 552         for (i=0; i<ctx->Variables; i++)
 553         {
 554                 if (ctx->Lattice->Properties[i].Column == -2)
 555                         split = i;
 556                 else if (ctx->Lattice->Properties[i].Column >=0 )
 557                         count = maxi(count, ctx->Lattice->Properties[i].Column+1);
 558         }
 559
 560         ctx->Homs = createVectorArray(count);
 561         ctx->Inhoms = createVectorArray(count);
 562         ctx->Frees = createVectorArray(count);
 563         ctx->Graver = createVectorArray(count);
 564
 565         // if no splitting, inhom only contains (0,...,0)
 566
 567         if (split<0)
 568                 appendToVectorArray(ctx->Inhoms, createZeroVector(count));
 569
 570         for (i=0; i<ctx->Lattice->Size; i++)
 571         {
 572                 vector = ctx->Lattice->Data[i];
 573                 // hom depends on splitting variable
 574                 is_hom = split < 0 || vector[split] == 0;
 575                 // free, if all nonzero-vars are free
 576                 is_free = true;
 577                 for (j=0; j<ctx->Lattice->Variables; j++)
 578                         if (vector[j] != 0 && !ctx->Lattice->Properties[j].Free)
 579                                 is_free = false;
 580                 // has_symmetric, if inverse fits the bounds
 581                 has_symmetric = true;
 582                 for (j=0; j<ctx->Lattice->Variables; j++)
 583                         if (!checkVariableBounds(ctx->Lattice->Properties, j, -vector[j]))
 584                                 has_symmetric = false;
 585                 // lex compare of vector with its inverse
 586                 lex_cmp = lexCompareInverseVector(vector, ctx->Lattice->Variables);
 587
 588                 assert(!is_free || has_symmetric);
 589
 590                 if (is_free) {
 591                         if (!has_symmetric || lex_cmp>0) {
 592                                 appendToVectorArray(ctx->Frees, copyVector(vector, count));
 593                                 appendToVectorArray(ctx->Graver, copyVector(vector, count));
 594                         }
 595                 }
 596                 else {
 597                         if (is_hom) {
 598                                 appendToVectorArray(ctx->Homs, copyVector(vector, count));
 599                                 if (!has_symmetric || lex_cmp>0)
 600                                         appendToVectorArray(ctx->Graver, copyVector(vector, count));
 601                         }
 602                         else {
 603                                 appendToVectorArray(ctx->Inhoms, copyVector(vector, count));
 604                         }
 605                 }
 606         }
 607
 608         if (ctx->Verbosity>0)
 609                 printf("\nFinal basis has %d inhomogeneous, %d homogeneous and %d free elements.\n", ctx->Inhoms->Size, ctx->Homs->Size, ctx->Frees->Size);
 610         if (ctx->LogLevel>0)
 611                 fprintf(ctx->LogFile, "\nFinal basis has %d inhomogeneous, %d homogeneous and %d free elements.\n", ctx->Inhoms->Size, ctx->Homs->Size, ctx->Frees->Size);
 612 }
 613
 614 void deleteZSolveContext(ZSolveContext ctx, bool deleteresult)
 615 {
 616         deleteVector(ctx->Sum);
 617         deleteVectorArray(ctx->Lattice);
 618
 619         if (deleteresult)
 620         {
 621                 deleteVectorArray(ctx->Homs);
 622                 deleteVectorArray(ctx->Inhoms);
 623                 deleteVectorArray(ctx->Frees);
 624                 deleteVectorArray(ctx->Graver);
 625         }
 626
 627         free(ctx);
 628 }