zsolve/solve.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 <stdio.h>
  24 #include <stdlib.h>
  25 #include <string.h>
  26 #include <ctype.h>
  27 #include <assert.h>
  28
  29 #include "banner.h"
  30 #include "opts.h"
  31 #include "libzsolve.h"
  32
  33 int OVerbose;
  34 int OLogging;
  35 int OBackup;
  36 bool OForce;
  37 bool ORightHandSide;
  38 bool OResume;
  39 bool OHilbert;
  40 bool OGraver;
  41
  42 int BaseLength;
  43 char *BaseName;
  44
  45 FILE *LogFile;
  46
  47 int readTokenFromFile(FILE *stream, char *tokenchars, char **ptoken, int *pmemory)
  48 {
  49         int c;
  50         int len = 0;
  51
  52         assert(ptoken);
  53         assert(pmemory);
  54
  55         if (*ptoken==NULL)
  56         {
  57                 *ptoken = (char *)calloc(8, sizeof(char));
  58                 *pmemory = 1;
  59         }
  60         else
  61                 (*ptoken)[0] = '\0';
  62
  63         while ((c = fgetc(stream))!=EOF)
  64         {
  65                 if (strchr(tokenchars, c))
  66                 {
  67                         if (len+1 >= *pmemory)
  68                         {
  69                                 *pmemory *= 2;
  70                                 *ptoken = (char *)realloc(*ptoken, *pmemory*sizeof(char));
  71                         }
  72                         (*ptoken)[len++] = c;
  73                         (*ptoken)[len] = '\0';
  74                 }
  75                 else if (len>0)
  76                         return len;
  77         }
  78
  79         return len;
  80 }
  81
  82 void backupEvent(ZSolveContext ctx)
  83 {
  84         FILE *stream;
  85
  86         strcat(BaseName, ".backup");
  87         stream = fopen(BaseName, "w");
  88         BaseName[BaseLength] = '\0';
  89
  90         backupZSolveContext(stream, ctx);
  91
  92         fclose(stream);
  93 }
  94
  95 //                                                                            //
  96
  97 int main(int argc, char *argv[])
  98 {
  99         FILE *stream = NULL;
 100         int i, j, r, count;
 101         bool flag;
 102
 103         Matrix matrix = NULL;
 104         Vector rhs = NULL;
 105         VectorArray Lattice = NULL;
 106         Vector vector = NULL;
 107
 108         LinearSystem initialsystem;
 109         ZSolveContext ctx;
 110
 111         char *token;
 112         int memory;
 113
 114         getopts(argc, argv);
 115
 116         puts(FORTY_TWO_BANNER);
 117
 118         if (OResume)
 119         {
 120                 // START OF RESUME SECTION - READ FILES AND CREATE CONTEXT
 121
 122                 strcat(BaseName, ".backup");
 123                 stream = fopen(BaseName, "r");
 124                 BaseName[BaseLength] = '\0';
 125
 126                 if (stream==NULL)
 127                 {
 128                         printf("Unable to open backup file %s.backup\n", BaseName);
 129                         free(BaseName);
 130                         exit(1);
 131                 }
 132
 133                 // options
 134                 if (fscanf(stream, "%d %d %d", &OVerbose, &OLogging, &OBackup)!=3 || OVerbose<0 || OVerbose>3 || OLogging<0 || OLogging>3 || OBackup<0)
 135                 {
 136                         fclose(stream);
 137                         printf("Backup file %s.backup does not contain valid data.\n", BaseName);
 138                         free(BaseName);
 139                         exit(2);
 140                 }
 141
 142                 // get context
 143                 ctx = createZSolveContextFromBackup(stream, zsolveLogCallbackDefault, backupEvent);
 144                 fclose(stream);
 145
 146                 // logfile
 147                 if (OLogging>0)
 148                 {
 149                         strcat(BaseName, ".log");
 150                         stream = fopen(BaseName, "a");
 151                         BaseName[BaseLength] = '\0';
 152                         if (stream==NULL)
 153                         {
 154                                 printf("Unable to open log file %s.log\n", BaseName);
 155                                 free(BaseName);
 156                                 exit(1);
 157                         }
 158                         ctx->LogFile = LogFile = stream;
 159                 }
 160
 161                 // END OF RESUME SECTION
 162         }
 163         else
 164         {
 165                 // logfile
 166                 if (OLogging>0)
 167                 {
 168                         strcat(BaseName, ".log");
 169                         stream = fopen(BaseName, "w");
 170                         BaseName[BaseLength] = '\0';
 171                         if (stream==NULL)
 172                         {
 173                                 printf("Unable to open log file %s.log\n", BaseName);
 174                                 free(BaseName);
 175                                 exit(1);
 176                         }
 177                         LogFile = stream;
 178                 }
 179                 // check for existance of solution files
 180                 if (!OForce)
 181                 {
 182                         strcat(BaseName, ".zhom");
 183                         stream = fopen(BaseName, "r");
 184                         BaseName[BaseLength] = '\0';
 185                         if (stream!=NULL)
 186                         {
 187                                 fclose(stream);
 188                                 if (OVerbose>0)
 189                                         printf("%s.hom already exists! Use -f to force calculation.\n", BaseName);
 190                                 if (OLogging>0)
 191                                 {
 192                                         fprintf(LogFile, "%s.hom already exists! Use -f to force calculation.\n", BaseName);
 193                                         fclose(LogFile);
 194                                 }
 195                                 free(BaseName);
 196                                 exit(1);
 197                         }
 198                         strcat(BaseName, ".zinhom");
 199                         stream = fopen(BaseName, "r");
 200                         BaseName[BaseLength] = '\0';
 201                         if (stream!=NULL)
 202                         {
 203                                 fclose(stream);
 204                                 if (OVerbose>0)
 205                                         printf("%s.inhom already exists! Use -f to force calculation.\n", BaseName);
 206                                 if (LogFile)
 207                                 {
 208                                         fprintf(LogFile, "%s.inhom already exists! Use -f to force calculation.\n", BaseName);
 209                                         fclose(LogFile);
 210                                 }
 211                                 free(BaseName);
 212                                 exit(1);
 213                         }
 214                 }
 215
 216                 // matrix
 217                 strcat(BaseName, ".mat");
 218                 stream = fopen(BaseName, "r");
 219                 BaseName[BaseLength] = '\0';
 220
 221                 if (stream == NULL)
 222                 {
 223                         stream = fopen(BaseName, "r");
 224                         if (stream) {
 225                                 if (OVerbose>0)
 226                                         printf("Matrix file %s.mat not found, falling back to project file %s.\n\n", BaseName, BaseName);
 227                                 if (OLogging>0)
 228                                 {
 229                                         fprintf(LogFile, "Matrix file %s.mat not found, falling back to project file %s.\n\n", BaseName, BaseName);
 230                                         fclose(LogFile);
 231                                 }
 232                         }
 233                 }
 234
 235                 if (stream==NULL)
 236                 {
 237                         strcat(BaseName, ".lat");
 238                         stream = fopen(BaseName, "r");
 239                         BaseName[BaseLength] = '\0';
 240                         if (stream==NULL)
 241                         {
 242                                 // lattice
 243                                 if (OVerbose>0)
 244                                         printf("Neither matrix file %s.mat nor lattice file %s.lat exists!\n", BaseName, BaseName);
 245                                 if (OLogging>0)
 246                                 {
 247                                         fprintf(LogFile, "Neither matrix file %s.mat nor lattice file %s.lat exists!\n", BaseName, BaseName);
 248                                         fclose(LogFile);
 249                                 }
 250                                 free(BaseName);
 251                                 exit(1);
 252                         }
 253                         else
 254                         {
 255                                 // START OF LATTICE SECTION - READ FILES AND CREATE CONTEXT
 256
 257                                 Lattice = readVectorArray(stream, false);
 258                                 fclose(stream);
 259                                 if (Lattice == NULL)
 260                                 {
 261                                         if (OVerbose>0)
 262                                                 printf("Lattice file %s.lat does not contain valid data.\n", BaseName);
 263                                         if (OLogging>0)
 264                                         {
 265                                                 fprintf(LogFile, "Lattice file %s.lat does not contain valid data.\n", BaseName);
 266                                                 fclose(LogFile);
 267                                         }
 268                                         free(BaseName);
 269                                         exit(1);
 270                                 }
 271
 272                                 // rhs
 273                                 if (ORightHandSide)
 274                                 {
 275                                         strcat(BaseName, ".rhs");
 276                                         stream = fopen(BaseName, "r");
 277                                         BaseName[BaseLength] = '\0';
 278                                         if (stream!=NULL)
 279                                         {
 280                                                 fscanf(stream, "%d", &i);
 281                                                 if (i!=1)
 282                                                 {
 283                                                         fclose(stream);
 284                                                         printf("Height of RHS must be 1!\n");
 285                                                         if (LogFile)
 286                                                         {
 287                                                                 fprintf(LogFile, "Height of RHS must be 1!\n");
 288                                                                 fclose(LogFile);
 289                                                         }
 290                                                         deleteMatrix(matrix);
 291                                                         free(BaseName);
 292                                                         exit(1);
 293                                                 }
 294                                                 fscanf(stream, "%d", &i);
 295                                                 while (i--)
 296                                                 {
 297                                                         if (fscanf(stream, "%d", &j) || j!=0)
 298                                                         {
 299                                                                 printf("When reading from %s.lat, RHS file %s.rhs must contain a zero vector.\n", BaseName, BaseName);
 300                                                                 if (LogFile)
 301                                                                 {
 302                                                                         fprintf(LogFile, "When reading from %s.lat, RHS file %s.rhs must contain a zero vector.\n", BaseName, BaseName);
 303                                                                         fclose(LogFile);
 304                                                                 }
 305                                                                 deleteMatrix(matrix);
 306                                                                 free(BaseName);
 307                                                                 exit(1);
 308                                                         }
 309                                                 }
 310                                         }
 311                                 }
 312
 313                                 // variable properties
 314
 315                                 for (i=0; i<Lattice->Variables; i++)
 316                                 {
 317                                         Lattice->Properties[i].Column = i;
 318                                         Lattice->Properties[i].Lower = OHilbert ? 0 : -MAXINT;
 319                                         Lattice->Properties[i].Upper = MAXINT;
 320                                         Lattice->Properties[i].Free = (!OGraver && !OHilbert);
 321                                 }
 322
 323                                 // read .rel
 324                                 strcat(BaseName, ".rel");
 325                                 stream = fopen(BaseName, "r");
 326                                 BaseName[BaseLength] = '\0';
 327                                 if (stream!=NULL)
 328                                 {
 329                                         token = NULL;
 330                                         memory = 0;
 331                                         flag = false;
 332
 333                                         if (fscanf(stream, "%d %d", &r, &j)<2 || r != 1)
 334                                         {
 335                                                 printf("RELATION file %s.rel must start with the dimensions.\n", BaseName);
 336                                                 flag = true;
 337                                         }
 338
 339                                         for (i=0; i<j; i++)
 340                                         {
 341                                                 if (readTokenFromFile(stream, "0123456789=<>", &token, &memory) == 0)
 342                                                 {
 343                                                         printf("RELATION file %s.rel ends unexpectedly.\n", BaseName);
 344                                                         flag = true;
 345                                                 }
 346                                                 else if (!strcmp(token, "<") || !strcmp(token, ">"))
 347                                                 {
 348                                                         printf("When reading from %s.lat, inequalities are not allowed.\n", BaseName);
 349                                                         flag = true;
 350                                                 }
 351                                                 else if (strcmp(token, "="))
 352                                                 {
 353                                                         printf("Unknown token '%s' in RELATION file %s.rel.\n", token, BaseName);
 354                                                         flag = true;
 355                                                 }
 356                                         }
 357                                         free(token);
 358                                         fclose(stream);
 359
 360                                         if (flag)
 361                                         {
 362                                                 free(BaseName);
 363                                                 exit(1);
 364                                         }
 365                                 }
 366
 367                                 // read .sign
 368                                 strcat(BaseName, ".sign");
 369                                 stream = fopen(BaseName, "r");
 370                                 BaseName[BaseLength] = '\0';
 371                                 if (stream!=NULL)
 372                                 {
 373                                         token = NULL;
 374                                         memory = 0;
 375                                         flag = false;
 376
 377                                         if (fscanf(stream, "%d %d", &r, &i)<2 || i != Lattice->Variables || r != 1)
 378                                         {
 379                                                 printf("SIGN file %s.sign must start with '1 %d'.\n", BaseName, Lattice->Variables);
 380                                                 flag = true;
 381                                         }
 382
 383                                         for (i=0; i<Lattice->Variables; i++)
 384                                         {
 385                                                 if (readTokenFromFile(stream, "0123456789-abcdefghijklmnopqrstuvwxyz", &token, &memory) == 0)
 386                                                 {
 387                                                         printf("SIGN file %s.sign ends unexpectedly.\n", BaseName);
 388                                                         flag = true;
 389                                                 }
 390                                                 if (!strcmp(token, "0") || !strcmp(token, "free") || !strcmp(token, "f"))
 391                                                 {
 392                                                         Lattice->Properties[i].Upper = MAXINT;
 393                                                         Lattice->Properties[i].Lower = -MAXINT;
 394                                                         Lattice->Properties[i].Free = true;
 395                                                 }
 396                                                 else if (!strcmp(token, "1") || !strcmp(token, "hil") || !strcmp(token, "h"))
 397                                                 {
 398                                                         Lattice->Properties[i].Upper = MAXINT;
 399                                                         Lattice->Properties[i].Lower = 0;
 400                                                         Lattice->Properties[i].Free = false;
 401                                                 }
 402                                                 else if (!strcmp(token, "-1") || !strcmp(token, "-hil") || !strcmp(token, "-h"))
 403                                                 {
 404                                                         Lattice->Properties[i].Upper = 0;
 405                                                         Lattice->Properties[i].Lower = -MAXINT;
 406                                                         Lattice->Properties[i].Free = false;
 407                                                 }
 408                                                 else if (!strcmp(token, "2") || !strcmp(token, "graver") || !strcmp(token, "g"))
 409                                                 {
 410                                                         if (OHilbert)
 411                                                         {
 412                                                                 printf("Input Error: Graver components for `hilbert' executable.\nInput Error: Use the `graver' executable instead.\n");
 413                                                                 flag = true;
 414                                                         }
 415                                                         else
 416                                                         {
 417                                                                 Lattice->Properties[i].Upper = MAXINT;
 418                                                                 Lattice->Properties[i].Lower = -MAXINT;
 419                                                                 Lattice->Properties[i].Free = false;
 420                                                         }
 421                                                 }
 422                                                 else
 423                                                 {
 424                                                         printf("Unknown token '%s' in SIGN file %s.sign.\n", token, BaseName);
 425                                                         flag = true;
 426                                                 }
 427                                         }
 428                                         free(token);
 429                                         fclose(stream);
 430
 431                                         if (flag)
 432                                         {
 433                                                 deleteVectorArray(Lattice);
 434                                                 free(BaseName);
 435                                                 exit(1);
 436                                         }
 437                                 }
 438
 439                                 // read .ub
 440                                 strcat(BaseName, ".ub");
 441                                 stream = fopen(BaseName, "r");
 442                                 BaseName[BaseLength] = '\0';
 443                                 if (stream!=NULL)
 444                                 {
 445                                         token = NULL;
 446                                         memory = 0;
 447                                         flag = false;
 448
 449                                         if (fscanf(stream, "%d %d", &r, &i)<2 || i != Lattice->Variables || r != 1)
 450                                         {
 451                                                 printf("UPPER BOUNDS file %s.ub must start with '1 %d'.\n", BaseName, Lattice->Variables);
 452                                                 flag = true;
 453                                         }
 454
 455                                         for (i=0; i<Lattice->Variables; i++)
 456                                         {
 457                                                 if (readTokenFromFile(stream, "0123456789*-", &token, &memory) == 0)
 458                                                 {
 459                                                         printf("UPPER BOUNDS file %s.ub ends unexpectedly.\n", BaseName);
 460                                                         flag = true;
 461                                                 }
 462                                                 if (!strcmp(token, "*"))
 463                                                         Lattice->Properties[i].Upper = MAXINT;
 464                                                 else if (sscanf(token, "%d", &j) == 1)
 465                                                 {
 466                                                         if (Lattice->Properties[i].Free)
 467                                                         {
 468                                                                 printf("Upper bound '%s' cannot be set for free variables.\n", token);
 469                                                                 flag = true;
 470                                                         }
 471                                                         else if (j>=0)
 472                                                                 Lattice->Properties[i].Upper = j;
 473                                                         else
 474                                                         {
 475                                                                 printf("Negative upper bound '%s' in UPPER BOUNDS file %s.ub.\n", token, BaseName);
 476                                                                 flag = true;
 477                                                         }
 478                                                 }
 479                                                 else
 480                                                 {
 481                                                         printf("Unknown token '%s' in UPPER BOUNDS file %s.ub.\n", token, BaseName);
 482                                                         flag = true;
 483                                                 }
 484                                         }
 485                                         free(token);
 486                                         fclose(stream);
 487
 488                                         if (flag)
 489                                         {
 490                                                 deleteVectorArray(Lattice);
 491                                                 free(BaseName);
 492                                                 exit(1);
 493                                         }
 494                                 }
 495
 496                                 // read .lb
 497                                 strcat(BaseName, ".lb");
 498                                 stream = fopen(BaseName, "r");
 499                                 BaseName[BaseLength] = '\0';
 500                                 if (stream!=NULL)
 501                                 {
 502                                         token = NULL;
 503                                         memory = 0;
 504                                         flag = false;
 505
 506                                         if (fscanf(stream, "%d %d", &r, &i)<2 || i != Lattice->Variables || r != 1)
 507                                         {
 508                                                 printf("LOWER BOUNDS file %s.lb must start with '1 %d'.\n", BaseName, Lattice->Variables);
 509                                                 flag = true;
 510                                         }
 511
 512                                         for (i=0; i<Lattice->Variables; i++)
 513                                         {
 514                                                 if (readTokenFromFile(stream, "0123456789*-", &token, &memory) == 0)
 515                                                 {
 516                                                         printf("LOWER BOUNDS file %s.lb ends unexpectedly.\n", BaseName);
 517                                                         flag = true;
 518                                                 }
 519                                                 if (!strcmp(token, "*"))
 520                                                         Lattice->Properties[i].Lower = -MAXINT;
 521                                                 else if (sscanf(token, "%d", &j) == 1)
 522                                                 {
 523                                                         if (Lattice->Properties[i].Free)
 524                                                         {
 525                                                                 printf("Lower bound '%s' cannot be set for free variables.\n", token);
 526                                                                 flag = true;
 527                                                         }
 528                                                         else if (j<=0)
 529                                                                 Lattice->Properties[i].Lower = j;
 530                                                         else
 531                                                         {
 532                                                                 printf("Positive lower bound '%s' in LOWER BOUNDS file %s.lb.\n", token, BaseName);
 533                                                                 flag = true;
 534                                                         }
 535                                                 }
 536                                                 else
 537                                                 {
 538                                                         printf("Unknown token '%s' in LOWER BOUNDS file %s.lb.\n", token, BaseName);
 539                                                         flag = true;
 540                                                 }
 541                                         }
 542                                         free(token);
 543                                         fclose(stream);
 544
 545                                         if (flag)
 546                                         {
 547                                                 deleteVectorArray(Lattice);
 548                                                 free(BaseName);
 549                                                 exit(1);
 550                                         }
 551                                 }
 552
 553                                 ctx = createZSolveContextFromLattice(Lattice, LogFile, OLogging, OVerbose, zsolveLogCallbackDefault, backupEvent);
 554
 555                                 // print lattice
 556                                 if (ctx->Verbosity>0)
 557                                 {
 558                                         printf("\nLattice to use:\n\n");
 559                                         printVectorArray(ctx->Lattice, false);
 560                                         printf("\n\n");
 561                                 }
 562                                 if (ctx->LogLevel>0)
 563                                 {
 564                                         fprintf(ctx->LogFile, "\nLattice to use:\n\n");
 565                                         fprintVectorArray(ctx->LogFile, ctx->Lattice, false);
 566                                         fprintf(ctx->LogFile, "\n\n");
 567                                 }
 568
 569                                 // END OF LATTICE SECTION
 570                         }
 571                 }
 572                 else
 573                 {
 574                         // START OF SYSTEM SECTION - READ FILES AND CREATE CONTEXT
 575
 576                         matrix = readMatrix(stream);
 577                         fclose(stream);
 578                         if (matrix==NULL)
 579                         {
 580                                 printf("Matrix file %s does not contain valid data.\n", BaseName);
 581                                 if (LogFile)
 582                                 {
 583                                         fprintf(LogFile, "Matrix file %s does not contain valid data.\n", BaseName);
 584                                         fclose(LogFile);
 585                                 }
 586                                 free(BaseName);
 587                                 exit(1);
 588                         }
 589
 590                         // rhs
 591                         if (ORightHandSide)
 592                         {
 593                                 strcat(BaseName, ".rhs");
 594                                 stream = fopen(BaseName, "r");
 595                                 BaseName[BaseLength] = '\0';
 596                                 if (stream!=NULL)
 597                                 {
 598                                         if (OGraver || OHilbert)
 599                                         {
 600                                                 fclose(stream);
 601                                                 printf("Input Error: No rhs file is allowed with --graver and --hilbert!\n");
 602                                                 printf("Input Error: Please delete %s.rhs and rerun zsolve\n", BaseName);
 603                                                 if (LogFile)
 604                                                 {
 605                                                         fprintf(LogFile, "Input Error: No rhs file is allowed with --graver and --hilbert!\n");
 606                                                         fprintf(LogFile, "Input Error: Please delete %s.rhs and rerun zsolve\n", BaseName);
 607                                                         fclose(LogFile);
 608                                                 }
 609                                                 deleteMatrix(matrix);
 610                                                 free(BaseName);
 611                                                 exit(1);
 612                                         }
 613
 614                                         fscanf(stream, "%d", &i);
 615                                         if (i!=1)
 616                                         {
 617                                                 fclose(stream);
 618                                                 printf("Height of RHS must be 1!\n");
 619                                                 if (LogFile)
 620                                                 {
 621                                                         fprintf(LogFile, "Height of RHS must be 1!\n");
 622                                                         fclose(LogFile);
 623                                                 }
 624                                                 deleteMatrix(matrix);
 625                                                 free(BaseName);
 626                                                 exit(1);
 627                                         }
 628                                         fscanf(stream, "%d", &i);
 629                                         if (i!=matrix->Height)
 630                                         {
 631                                                 fclose(stream);
 632                                                 printf("Matrix height conflicts with width of rhs!\n");
 633                                                 if (LogFile)
 634                                                 {
 635                                                         fprintf(LogFile, "Matrix height conflicts with width of rhs!\n");
 636                                                         fclose(LogFile);
 637                                                 }
 638                                                 deleteMatrix(matrix);
 639                                                 free(BaseName);
 640                                                 exit(1);
 641                                         }
 642                                         rhs = readVector(stream, matrix->Height);
 643                                         fclose(stream);
 644                                         if (rhs==NULL)
 645                                         {
 646                                                 printf("RHS file %s.rhs does not contain valid data.\n", BaseName);
 647                                                 if (LogFile)
 648                                                 {
 649                                                         fprintf(LogFile, "RHS file %s.rhs does not contain valid data.\n", BaseName);
 650                                                         fclose(LogFile);
 651                                                 }
 652                                                 deleteMatrix(matrix);
 653                                                 free(BaseName);
 654                                                 exit(1);
 655                                         }
 656                                 }
 657                         }
 658
 659                         // fill with zeros
 660                         if (rhs==NULL)
 661                         {
 662                                 rhs = createVector(matrix->Height);
 663                                 for (i=0; i<matrix->Height; i++)
 664                                         rhs[i] = 0;
 665                         }
 666
 667                         // create system
 668                         initialsystem = createLinearSystem();
 669
 670                         setLinearSystemMatrix(initialsystem, matrix);
 671                         deleteMatrix(matrix);
 672
 673                         setLinearSystemRHS(initialsystem, rhs);
 674                         deleteVector(rhs);
 675
 676                         // default limits
 677
 678                         if (OGraver)
 679                                 setLinearSystemLimit(initialsystem, -1, -MAXINT, MAXINT, false);
 680                         else if (OHilbert)
 681                                 setLinearSystemLimit(initialsystem, -1, 0, MAXINT, false);
 682                         else
 683                                 setLinearSystemLimit(initialsystem, -1, -MAXINT, MAXINT, true);
 684
 685                         // default equation type
 686
 687                         setLinearSystemEquationType(initialsystem, -1, EQUATION_EQUAL, 0);
 688
 689                         // read .rel
 690                         strcat(BaseName, ".rel");
 691                         stream = fopen(BaseName, "r");
 692                         BaseName[BaseLength] = '\0';
 693                         if (stream!=NULL)
 694                         {
 695                                 token = NULL;
 696                                 memory = 0;
 697                                 flag = false;
 698
 699                                 if (fscanf(stream, "%d %d", &r, &i)<2 || i != initialsystem->Equations || r != 1)
 700                                 {
 701                                         printf("RELATION file %s.rel must start with '1 %d'.\n", BaseName, initialsystem->Equations);
 702                                         flag = true;
 703                                 }
 704
 705                                 for (i=0; i<initialsystem->Equations; i++)
 706                                 {
 707                                         if (readTokenFromFile(stream, "0123456789=<>", &token, &memory) == 0)
 708                                         {
 709                                                 printf("RELATION file %s.rel ends unexpectedly.\n", BaseName);
 710                                                 flag = true;
 711                                         }
 712                                         if (!strcmp(token, "="))
 713                                                 setLinearSystemEquationType(initialsystem, i, EQUATION_EQUAL, 0);
 714                                         // BUG: Not a real bug, but maybe misdefinition?? <= is not so hard to type :-)
 715                                         else if (!strcmp(token, "<"))
 716                                                 setLinearSystemEquationType(initialsystem, i, EQUATION_LESSEREQUAL, 0);
 717                                         else if (!strcmp(token, ">"))
 718                                                 setLinearSystemEquationType(initialsystem, i, EQUATION_GREATEREQUAL, 0);
 719                                         else
 720                                         {
 721                                                 printf("Unknown token '%s' in RELATION file %s.rel.\n", token, BaseName);
 722                                                 flag = true;
 723                                         }
 724                                 }
 725                                 free(token);
 726                                 fclose(stream);
 727
 728                                 if (flag)
 729                                 {
 730                                         deleteLinearSystem(initialsystem);
 731                                         free(BaseName);
 732                                         exit(1);
 733                                 }
 734                         }
 735
 736                         // read .sign
 737                         strcat(BaseName, ".sign");
 738                         stream = fopen(BaseName, "r");
 739                         BaseName[BaseLength] = '\0';
 740                         if (stream!=NULL)
 741                         {
 742                                 token = NULL;
 743                                 memory = 0;
 744                                 flag = false;
 745
 746                                 if (fscanf(stream, "%d %d", &r, &i)<2 || i != initialsystem->Variables || r != 1)
 747                                 {
 748                                         printf("SIGN file %s.sign must start with '1 %d'.\n", BaseName, initialsystem->Variables);
 749                                         flag = true;
 750                                 }
 751
 752                                 for (i=0; i<initialsystem->Variables; i++)
 753                                 {
 754                                         if (readTokenFromFile(stream, "0123456789-abcdefghijklmnopqrstuvwxyz", &token, &memory) == 0)
 755                                         {
 756                                                 printf("SIGN file %s.sign ends unexpectedly.\n", BaseName);
 757                                                 flag = true;
 758                                         }
 759                                         if (!strcmp(token, "0") || !strcmp(token, "free") || !strcmp(token, "f"))
 760                                                 setLinearSystemLimit(initialsystem, i, -MAXINT, MAXINT, true);
 761                                         else if (!strcmp(token, "1") || !strcmp(token, "hil") || !strcmp(token, "h"))
 762                                                 setLinearSystemLimit(initialsystem, i, 0, MAXINT, false);
 763                                         else if (!strcmp(token, "-1") || !strcmp(token, "-hil") || !strcmp(token, "-h"))
 764                                                 setLinearSystemLimit(initialsystem, i, -MAXINT, 0, false);
 765                                         else if (!strcmp(token, "2") || !strcmp(token, "graver") || !strcmp(token, "g"))
 766                                         {
 767                                                 if (OHilbert)
 768                                                 {
 769                                                         if (!flag)
 770                                                                 printf("Input Error: Graver components for `hilbert' executable.\nInput Error: Use the `graver' executable instead.\n");
 771                                                         flag = true;
 772                                                 }
 773                                                 else
 774                                                         setLinearSystemLimit(initialsystem, i, -MAXINT, MAXINT, false);
 775                                         }
 776                                         else
 777                                         {
 778                                                 printf("Unknown token '%s' in SIGN file %s.sign.\n", token, BaseName);
 779                                                 flag = true;
 780                                         }
 781                                 }
 782                                 free(token);
 783                                 fclose(stream);
 784
 785                                 if (flag)
 786                                 {
 787                                         deleteLinearSystem(initialsystem);
 788                                         free(BaseName);
 789                                         exit(1);
 790                                 }
 791                         }
 792
 793                         // read .ub
 794                         strcat(BaseName, ".ub");
 795                         stream = fopen(BaseName, "r");
 796                         BaseName[BaseLength] = '\0';
 797                         if (stream!=NULL)
 798                         {
 799                                 token = NULL;
 800                                 memory = 0;
 801                                 flag = false;
 802
 803                                 if (fscanf(stream, "%d %d", &r, &i)<2 || i != initialsystem->Variables || r != 1)
 804                                 {
 805                                         printf("UPPER BOUNDS file %s.ub must start with '1 %d'.\n", BaseName, initialsystem->Variables);
 806                                         flag = true;
 807                                 }
 808
 809                                 for (i=0; i<initialsystem->Variables; i++)
 810                                 {
 811                                         if (readTokenFromFile(stream, "0123456789*-", &token, &memory) == 0)
 812                                         {
 813                                                 printf("UPPER BOUNDS file %s.ub ends unexpectedly.\n", BaseName);
 814                                                 flag = true;
 815                                         }
 816                                         if (!strcmp(token, "*"))
 817                                                 setLinearSystemBound(initialsystem, i, 'u', MAXINT);
 818                                         else if (sscanf(token, "%d", &j) == 1)
 819                                         {
 820                                                 if (initialsystem->VarProperties[i].Free)
 821                                                 {
 822                                                         printf("Upper bound '%s' cannot be set for free variables.\n", token);
 823                                                         flag = true;
 824                                                 }
 825                                                 else if (j>=0)
 826                                                         setLinearSystemBound(initialsystem, i, 'u', j);
 827                                                 else
 828                                                 {
 829                                                         printf("Negative upper bound '%s' in UPPER BOUNDS file %s.ub.\n", token, BaseName);
 830                                                         flag = true;
 831                                                 }
 832                                         }
 833                                         else
 834                                         {
 835                                                 printf("Unknown token '%s' in UPPER BOUNDS file %s.ub.\n", token, BaseName);
 836                                                 flag = true;
 837                                         }
 838                                 }
 839                                 free(token);
 840                                 fclose(stream);
 841
 842                                 if (flag)
 843                                 {
 844                                         deleteLinearSystem(initialsystem);
 845                                         free(BaseName);
 846                                         exit(1);
 847                                 }
 848                         }
 849
 850                         // read .lb
 851                         strcat(BaseName, ".lb");
 852                         stream = fopen(BaseName, "r");
 853                         BaseName[BaseLength] = '\0';
 854                         if (stream!=NULL)
 855                         {
 856                                 token = NULL;
 857                                 memory = 0;
 858                                 flag = false;
 859
 860                                 if (fscanf(stream, "%d %d", &r, &i)<2 || i != initialsystem->Variables || r != 1)
 861                                 {
 862                                         printf("LOWER BOUNDS file %s.lb must start with '1 %d'.\n", BaseName, initialsystem->Variables);
 863                                         flag = true;
 864                                 }
 865
 866                                 for (i=0; i<initialsystem->Variables; i++)
 867                                 {
 868                                         if (readTokenFromFile(stream, "0123456789*-", &token, &memory) == 0)
 869                                         {
 870                                                 printf("LOWER BOUNDS file %s.lb ends unexpectedly.\n", BaseName);
 871                                                 flag = true;
 872                                         }
 873                                         if (!strcmp(token, "*"))
 874                                                 setLinearSystemBound(initialsystem, i, 'l', -MAXINT);
 875                                         else if (sscanf(token, "%d", &j) == 1)
 876                                         {
 877                                                 if (initialsystem->VarProperties[i].Free)
 878                                                 {
 879                                                         printf("Lower bound '%s' cannot be set for free variables.\n", token);
 880                                                         flag = true;
 881                                                 }
 882                                                 else if (j<=0)
 883                                                         setLinearSystemBound(initialsystem, i, 'l', j);
 884                                                 else
 885                                                 {
 886                                                         printf("Positive lower bound '%s' in LOWER BOUNDS file %s.lb.\n", token, BaseName);
 887                                                         flag = true;
 888                                                 }
 889                                         }
 890                                         else
 891                                         {
 892                                                 printf("Unknown token '%s' in LOWER BOUNDS file %s.lb.\n", token, BaseName);
 893                                                 flag = true;
 894                                         }
 895                                 }
 896                                 free(token);
 897                                 fclose(stream);
 898
 899                                 if (flag)
 900                                 {
 901                                         deleteLinearSystem(initialsystem);
 902                                         free(BaseName);
 903                                         exit(1);
 904                                 }
 905                         }
 906
 907                         ctx = createZSolveContextFromSystem(initialsystem, LogFile, OLogging, OVerbose, zsolveLogCallbackDefault, backupEvent);
 908
 909                         // END OF SYSTEM SECTION
 910                 }
 911         }
 912
 913         // DEBUG
 914 //      printVectorArray(ctx->Lattice, true);
 915
 916         zsolveSystem(ctx, !OResume);
 917
 918         if (OGraver)
 919         {
 920                 printf("Writing %d vectors to graver file, with respect to symmetry.\n", ctx->Graver->Size);
 921                 if (LogFile)
 922                         fprintf(LogFile, "Writing %d vectors to graver file, with respect to symmetry.\n", ctx->Graver->Size);
 923
 924                 strcat(BaseName, ".gra");
 925                 stream = fopen(BaseName, "w");
 926                 BaseName[BaseLength] = '\0';
 927                 if (stream)
 928                 {
 929                         fprintf(stream, "%d %d\n\n", ctx->Graver->Size, ctx->Graver->Variables);
 930                         fprintVectorArray(stream, ctx->Graver, false);
 931                         fclose(stream);
 932                 }
 933         }
 934         else if (OHilbert)
 935         {
 936                 strcat(BaseName, ".hil");
 937                 stream = fopen(BaseName, "w");
 938                 BaseName[BaseLength] = '\0';
 939                 if (stream)
 940                 {
 941                         fprintf(stream, "%d %d\n\n", ctx->Homs->Size + ctx->Frees->Size, ctx->Homs->Variables);
 942                         fprintVectorArray(stream, ctx->Homs, false);
 943                         fprintf(stream, "\n");
 944                         fprintVectorArray(stream, ctx->Frees, false);
 945                         fclose(stream);
 946                 }
 947         }
 948         else
 949         {
 950                 strcat(BaseName, ".zinhom");
 951                 stream = fopen(BaseName, "w");
 952                 BaseName[BaseLength] = '\0';
 953                 if (stream)
 954                 {
 955                         fprintf(stream, "%d %d\n\n", ctx->Inhoms->Size, ctx->Inhoms->Variables);
 956                         fprintVectorArray(stream, ctx->Inhoms, false);
 957                         fclose(stream);
 958                 }
 959
 960                 strcat(BaseName, ".zhom");
 961                 stream = fopen(BaseName, "w");
 962                 BaseName[BaseLength] = '\0';
 963                 if (stream)
 964                 {
 965                         fprintf(stream, "%d %d\n\n", ctx->Homs->Size, ctx->Homs->Variables);
 966                         fprintVectorArray(stream, ctx->Homs, false);
 967                         fclose(stream);
 968                 }
 969
 970                 if (ctx->Frees->Size>0)
 971                 {
 972                         strcat(BaseName, ".zfree");
 973                         stream = fopen(BaseName, "w");
 974                         BaseName[BaseLength] = '\0';
 975                         if (stream)
 976                         {
 977                                 fprintf(stream, "%d %d\n\n", ctx->Frees->Size, ctx->Frees->Variables);
 978                                 fprintVectorArray(stream, ctx->Frees, false);
 979                                 fclose(stream);
 980                         }
 981                 }
 982         }
 983
 984
 985         printf("\n4ti2 Total Time: ");
 986         printCPUTime(maxd(getCPUTime() - ctx->AllTime, 0.0));
 987         printf("\n");
 988         if (LogFile) {
 989                 fprintf(LogFile, "\n4ti2 Total Time: ");
 990                 fprintCPUTime(LogFile, maxd(getCPUTime() - ctx->AllTime, 0.0));
 991                 fprintf(LogFile, "\n");
 992         }
 993
 994         deleteZSolveContext(ctx, true);
 995
 996         if (BaseName!=NULL)
 997                 free(BaseName);
 998
 999         if (LogFile)
1000                 fclose(LogFile);
1001
1002         return EXIT_SUCCESS;
1003 }
1004
1005 //                                                                            //