// resilient_cps.c
// Copyright 2018 Carnegie Mellon University. All Rights Reserved.
// NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING INSTITUTE MATERIAL IS FURNISHED ON AN "AS-IS" BASIS. CARNEGIE MELLON UNIVERSITY MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT, TRADEMARK, OR COPYRIGHT INFRINGEMENT.
// Released under a BSD (SEI)-style license, please see license.txt or contact permission@sei.cmu.edu for full terms.
// [DISTRIBUTION STATEMENT A] This material has been approved for public release and unlimited distribution.  Please see Copyright notice for non-US Government use and distribution.
// DM18-0526
// License.txt file:
// resilient_cps.c
// Copyright 2018 Carnegie Mellon University. All Rights Reserved.
// BSD (SEI)
// Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
// 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
// 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
// 3. Products derived from this software may not include “Carnegie Mellon University,” "SEI” and/or “Software Engineering Institute" in the name of such derived product, nor shall “Carnegie Mellon University,” "SEI” and/or “Software Engineering Institute" be used to endorse or promote products derived from this software without prior written permission. For written permission, please contact permission@sei.cmu.edu.
//
// ACKNOWLEDGMENTS AND DISCLAIMERS:
// This material is based upon work funded and supported by the Department of Defense under Contract No. FA8702-15-D-0002 with Carnegie Mellon University for the operation of the Software Engineering Institute, a federally funded research and development center.
// The view, opinions, and/or findings contained in this material are those of the author(s) and should not be construed as an official Government position, policy, or decision, unless designated by other documentation.
// NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING INSTITUTE MATERIAL IS FURNISHED ON AN "AS-IS" BASIS. CARNEGIE MELLON UNIVERSITY MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT, TRADEMARK, OR COPYRIGHT INFRINGEMENT.
// [DISTRIBUTION STATEMENT A] This material has been approved for public release and unlimited distribution.  Please see Copyright notice for non-US Government use and distribution.
// DM18-0526
//
// What does this program do?
//   It performs schedulability analysis of resilient CPS model.
// 
// How do I install it?
//   Install the SMT solver z3.
//   Compile the program as follows:
//     gcc -o resilient_cps resilient_cps.c -lm
//   Now, you have a file resilient_cps
//		    
// How do I actually run it?
//   Open a console. Then type:
//      resilient_cps -i system.txt -o system_results_from_analysis.txt
//   With this command, you tell the tool that it should read the file system.txt.txt and perform schedulability analysis and write the output of the analysis to
//     the file results_from_analysis.txt.
//   You can run it in meta mode (a mode where the program generates tasksets and analyzes them) with
//     ./resilient_cps -m &> outputlog.txt
//
// What is the format of the input file?
//   The input file is a text file with numbers and these numbers are not comma separated. 
//   An example of an input file is as follows:
// 1
// 2
// 1 2
//   20 20 10 8 8 2 2
// 2 1
//   25 25 12 8 8 2 2
//
// The 1st number is "1" and it indicates the method to be used.
// The 2nd number is "2" and it indicates the number of tasks

// The 3rd number is "1" and it indicates that the following information is for task 1
// The 4th number is "2"; it indicates the priority of task 1
// The 5th number is "20"; it indicates the T parameter of task 1
// The 6th number is "20"; it indicates the D parameter of task 1
// The 7th number is "10"; it indicates the Z parameter of task 1
// The 8th number is "8"; it indicates the C parameter of task 1
// The 9th number is "8"; it indicates the E parameter of task 1
// The 10th number is "2"; it indicates the MAXCOUNT parameter of task 1
// The 11th number is "2"; it indicates the RC parameter of task 1
// Analogous for the remaining lines.
// Note that priorities must be unique.
//   
//  You can learn about the input file format by reading the function "void readtasksetfromfile(char* fn)" in this source code file.
// 
// We add these in order to do file I/O like in UNIX.
#include <stdlib.h>
#include <stdio.h>

#include <time.h> // we add this in order to call the function time( ..)

#include <fcntl.h>

#include <math.h>

#include <sys/stat.h> // this is needed for the constant S_IWRITE

#include <string.h>   //  this is needed for strcmp

#include <unistd.h>

#include <stdio.h>
#include <stdlib.h>

#define MAXNTASKS      100

#define MAXNVARSUSEDFORPLOTTING 1000000

int metathing = 0;

char inputfilename[20000]="system.txt";
char outputfilename[20000]="system_results_from_analysis.txt";
char plotfilename[2000]="failure.svg";

int writeGurobilogfile = 1;
int writelpfile = 1;
int writesolfile = 1;

int enable_generate_latexpdf = 0;
int enable_generate_svg = 1;
int enable_drawprocessor_boxes = 0;
int enable_drawschedulerectanglesinhalfheight = 1;

struct task {
  int id;
  int prio;
  double T;
  double D;
  double Z;
  double C;
  double E;
  int MAXCOUNT;
  int RC;
};

int useanalysismethod;
int ntasks;
struct task tasks[MAXNTASKS+1];  // there is no element in index 0.

int counterforSMTsolver = 0;
FILE* z3throughcommandlinesmt2file;
char z3throughcommandlinesmt2filename[200];
FILE* commandstringwithscriptfile;
char commandstringwithscriptfilename[200];

char z3throughcommandline_result_filename[200];

int enableplot = 1;

int minint2(int a, int b) { if (a<b) { return a; } else { return b; } }

int is_in_hp(int j,int iD) { if (tasks[j].prio > tasks[iD].prio) { return 1; } else { return 0; } }

int getnpos(int iD) {
  int j; int sum;
  sum = 0;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      sum = sum + ceil(tasks[iD].D/tasks[j].T);
    }
  }
  return (4*sum-1);
}

void initialize_random_generator() {
  srand(137);
  srand48(137);
}

int myrandom() { return rand(); }
double myrand48() { return drand48(); }
int my_int_random(int lb, int ub)             { return lb + (myrandom() % (ub-lb+1) ); }
double my_double_random(double lo, double hi) { return lo + myrand48()*(hi-lo);        }

double mypow(double t1, double t2) { return exp(t2*log(t1)); }

void drawline_svg( FILE* f, double w, double h, double startx, double starty, double endx, double endy) {
  fprintf( f,
    "<line x1=\"%lf\" x2=\"%lf\"   y1=\"%lf\" y2=\"%lf\" stroke=\"black\" stroke-width=\"2\" />\n",
      w*(startx/10.0),
      w*(endx/10.0),
      h*((10.0-starty)/10.0),
      h*((10.0-endy)/10.0)
    );
}

void drawarrowright( FILE* f, double w, double h, double startx, double starty, double length) {
  drawline_svg( f, w, h, startx,                    starty,             startx+length, starty);
  drawline_svg( f, w, h, startx+length-0.03*length, starty+0.03*length, startx+length, starty);
  drawline_svg( f, w, h, startx+length-0.03*length, starty-0.03*length, startx+length, starty);
}

void drawarrowup( FILE* f, double w, double h, double startx, double starty, double length) {
  drawline_svg( f, w, h, startx,             starty,                    startx,        starty+length);
  drawline_svg( f, w, h, startx-0.03*length, starty+length-0.03*length, startx,        starty+length);
  drawline_svg( f, w, h, startx+0.03*length, starty+length-0.03*length, startx,        starty+length);
}

void drawarrowdown( FILE* f, double w, double h, double startx, double starty, double length) {
  drawline_svg( f, w, h, startx,             starty,                    startx,        starty-length);
  drawline_svg( f, w, h, startx-0.03*length, starty-length+0.03*length, startx,        starty-length);
  drawline_svg( f, w, h, startx+0.03*length, starty-length+0.03*length, startx,        starty-length);
}

void drawlineup( FILE* f, double w, double h, double startx, double starty, double length) {
  drawline_svg( f, w, h, startx,             starty,                    startx,        starty+length);
}

void drawlinedown( FILE* f, double w, double h, double startx, double starty, double length) {
  drawline_svg( f, w, h, startx,             starty,                    startx,        starty-length);
}

void drawtext_svg( FILE* f, double w, double h, double x, double y, char* s) {
  fprintf( f,
    "<text x=\"%lf\" y=\"%lf\"> %s </text>\n",
      w*(x/10.0),
      h*((10.0-y)/10.0),
      s
    );
}

void drawtext_vertical_svg( FILE* f, double w, double h, double x, double y, char* s) {
  fprintf( f,
    "<text x=\"%lf\" y=\"%lf\" transform=\"rotate(90,%lf,%lf)\"> %s </text>\n",
      w*(x/10.0),
      h*((10.0-y)/10.0),
      w*(x/10.0),
      h*((10.0-y)/10.0),
      s
    );
}
void drawtext_vertical_colorspecified_svg( FILE* f, double w, double h, double x, double y, char* colorspecified, char* s) {
  fprintf( f,
    "<text x=\"%lf\" y=\"%lf\" transform=\"rotate(90,%lf,%lf)\" stroke=\"%s\" fill=\"%s\"> %s </text>\n",
      w*(x/10.0),
      h*((10.0-y)/10.0),
      w*(x/10.0),
      h*((10.0-y)/10.0),
      colorspecified,
      colorspecified,
      s
    );
}

void drawintastext_svg( FILE* f, double w, double h, double x, double y, int t) {
  char tempstr[200];
  sprintf(tempstr,"%d", t);
  drawtext_svg( f, w, h, x, y, tempstr);
}

void drawdoubleastext_svg( FILE* f, double w, double h, double x, double y, double t) {
  char tempstr[200];
  sprintf(tempstr,"%lf", t);
  drawtext_svg( f, w, h, x, y, tempstr);
}

void drawdoubleastext_vertical_svg( FILE* f, double w, double h, double x, double y, double t) {
  char tempstr[200];
  sprintf(tempstr,"%lf", t);
  drawtext_vertical_svg( f, w, h, x, y, tempstr);
}
void drawdoubleastext_vertical_colorspecified_svg( FILE* f, double w, double h, double x, double y, char* colorspecified, double t) {
  char tempstr[200];
  sprintf(tempstr,"%lf", t);
  drawtext_vertical_colorspecified_svg( f, w, h, x, y, colorspecified, tempstr);
}

void drawbox_svg( FILE* f, double w, double h, double xstart,  double ystart, double xfinish, double yfinish, char* fillcolorstr) {
  fprintf( f,
    "<rect x=\"%lf\" y=\"%lf\" width=\"%lf\" height=\"%lf\" stroke=\"black\" stroke-width=\"4\" fill=\"%s\" />\n",
    w*(xstart/10.0), h*((10-yfinish)/10.0), w*((xfinish-xstart)/10.0), h*((yfinish-ystart)/10.0), fillcolorstr
  );
}

void drawintasprocessor_svg( FILE* f, double w, double h, double x, double y, int proc) {
  char tempstr[200];
  sprintf(tempstr,"P%d", proc);
  drawtext_svg( f, w, h, x, y, tempstr);
}

void drawtexttau_i_k_svg( FILE* f, double w, double h, double x, double y, int i, int k) {
  char tempstr[200];
  sprintf(tempstr,"t%d,%d", i,k);
  drawtext_svg( f, w, h, x, y, tempstr);
}
void drawtexttau_i_k_vertical_svg( FILE* f, double w, double h, double x, double y, int i, int k) {
  char tempstr[200];
  sprintf(tempstr,"t%d,%d", i,k);
  drawtext_vertical_svg( f, w, h, x, y, tempstr);
}
void drawtexttau_i_k_colorspecified_vertical_svg( FILE* f, double w, double h, double x, double y, int i, int k, char* colorspecified) {
  char tempstr[200];
  sprintf(tempstr,"t%d,%d", i,k);
  drawtext_vertical_colorspecified_svg( f, w, h, x, y, colorspecified, tempstr);
}

void drawtexttau_i_svg( FILE* f, double w, double h, double x, double y, int i) {
  char tempstr[200];
  sprintf(tempstr,"t%d", i);
  drawtext_svg( f, w, h, x, y, tempstr);
}

void readtasksetfromfile_task(FILE* myfile, int i) {
  fscanf( myfile, "%d %d",   &(tasks[i].id), &(tasks[i].prio) );
  fscanf( myfile, "%lf %lf %lf %lf %lf %d %d", &(tasks[i].T), &(tasks[i].D), &(tasks[i].Z), &(tasks[i].C), &(tasks[i].E), &(tasks[i].MAXCOUNT), &(tasks[i].RC) );
}

void readtasksetfromfile(char* fn) {
  FILE* myfile; int i;
  myfile = fopen( fn, "rt");
  if (myfile==NULL) { printf("Error opening file in function readtasksetfromfile. fn=%s\n", fn); fflush(stdout); exit(0); }
  fscanf( myfile, "%d",  &useanalysismethod);
  fscanf( myfile, "%d",  &ntasks);
  for (i=1;i<=ntasks;i++) { readtasksetfromfile_task(myfile,i); }
  fclose( myfile);
}

void writetasksettofile_task(FILE* myfile, int i) {
  fprintf( myfile, "%d %d ",   tasks[i].id, tasks[i].prio );
  fprintf( myfile, "%lf %lf %lf %lf %lf %d %d", tasks[i].T, tasks[i].D, tasks[i].Z, tasks[i].C, tasks[i].E, tasks[i].MAXCOUNT, tasks[i].RC );
  fprintf( myfile, "\n");
}

void writetasksettofile(char* fn) {
  FILE* myfile; int i;
  myfile = fopen( fn, "w");
  if (myfile==NULL) { printf("Error opening file in function writetasksettofile. fn=%s\n", fn); fflush(stdout); exit(0); }
  fprintf( myfile, "%d\n",  useanalysismethod);
  fprintf( myfile, "%d\n",  ntasks);
  for (i=1;i<=ntasks;i++) { writetasksettofile_task(myfile,i); }
  fclose( myfile);
}

void fillvariablestringandvaluestring(char* pvariablestring, char* pvaluestring, char* ptemps, char* ptemps2) {
  char s1[2000]; char s2[2000]; char s3[2000]; char s4[2000];
  char* p;
  sscanf(ptemps, "%s %s %s %s", s1, s2, s3, s4);
  
  // now we get the variable name
  strcpy( pvariablestring, s2 );

  // now we get the value
  // we start by deleting the end of line
  strcpy( s2, ptemps2 );
  while (s2[strlen(s2)-1]=='\n') {
    s2[strlen(s2)-1] = 0;
  }
  s2[strlen(s2)-1] = 0; // now we remove one parenthesis

  // now we delete spaces in the beginning
  p = s2;
  while ((*p)==' ') {
    p++;
  }
  strcpy( pvaluestring, p );
}

int is_there_an_beginning_and_trailing_parenthesis(char* p) {
  return ((strchr(p,'(')!=NULL) && (strchr(p,')')!=NULL));
}

void fillstringbydeletebeginningandtrailingparenthesis(char* temps,char* p) {
  char* p2;
  while ((*p)!='(') {
    p++;
  }
  p++;
  strcpy( temps, p);
  p2 = &(temps[ strlen(temps)]);
  while ((*p2)!=')') {
    p2--;
  }
  *p2 = 0;  
}

void getdoublebyevaluatingstring_fraction(char* p, double* p_v, int* p_errorcode) {
  char temps[2000]; char temps2[2000]; char s[2000]; double a; double b;
  int n_values_retrieved;
  if (!is_there_an_beginning_and_trailing_parenthesis(p)) {
    *p_errorcode = 0;
    return;
  }
  fillstringbydeletebeginningandtrailingparenthesis(temps,p);
  if (temps[0]=='-') {
    fillstringbydeletebeginningandtrailingparenthesis(temps2,temps);
    n_values_retrieved = sscanf(temps2,"%s %lf %lf", s, &a, &b);
    *p_errorcode = (n_values_retrieved==3);
    *p_v = a/b;
  } else {
    n_values_retrieved = sscanf(temps,"%s %lf %lf", s, &a, &b);
    *p_errorcode = (n_values_retrieved==3);
    *p_v = a/b;
  }
}
void getdoublebyevaluatingstring_notfraction(char* p, double* p_v, int* p_errorcode) {
  double temp;  
  int n_values_retrieved;
  n_values_retrieved = sscanf(p,"%lf", &temp);
  *p_errorcode = (n_values_retrieved==1);
  *p_v = temp;
}
double getdoublebyevaluatingstring(char* p) {
  double v1; int errorcode1;
  double v2; int errorcode2;
  getdoublebyevaluatingstring_fraction(p,   &v1, &errorcode1);
  getdoublebyevaluatingstring_notfraction(p,&v2, &errorcode2);
  if ((!errorcode1)  && (!errorcode2))  { printf("Error in getdoublebyevaluatingstring. Both failed.    v1=%lf errrocode1=%d v2=%lf errrocode2=%d.\n",v1,errorcode1,v2,errorcode2); exit(-1); }
  if ((errorcode1)   && (errorcode2))   { printf("Error in getdoublebyevaluatingstring. Both succeeded. v1=%lf errrocode1=%d v2=%lf errrocode2=%d.\n",v1,errorcode1,v2,errorcode2); exit(-1); }
  if ((errorcode1)   && (!errorcode2))  {
    return v1;
  } else {
    return v2;
  }
}

struct variableandvaluestruct {
  char variablestring[200];
  char valuestring[200];
};

int nvariableandvalues;
struct variableandvaluestruct variableandvalues[MAXNVARSUSEDFORPLOTTING];

int isstringboolean(char* s) {
  if (strncmp(s,"true",4)==0) { return 1; }
  if (strncmp(s,"false",5)==0) { return 1; }
  return 0;
}

int isstringinteger(char* s) {
  char* p; int isdig;
  p = s;
  while ((*p)!=0) {
    isdig = (('0'<=(*p)) && ((*p)<='9'));
    if (!isdig) { return 0; }
    p++;
  }
  return 1;
}

int isstringbooleanorinteger(char* s) {
  return (isstringboolean(s) || isstringinteger(s));
}

int getbooleanvaluefromvariablename(char* p) {
  int local_counter;
  for (local_counter=0;local_counter<nvariableandvalues;local_counter++) {
    if (strcmp(variableandvalues[local_counter].variablestring,p)==0) {
      if (strncmp(variableandvalues[local_counter].valuestring,"true",4)==0) { return 1; } else { return 0; }
    }
  }
  printf("Error in getbooleanvaluefromvariablename. p=%s.\n", p);
  exit(0);
}

double getrealvaluefromvariablename(char* p) {
  int local_counter; double va;
  for (local_counter=0;local_counter<nvariableandvalues;local_counter++) {
    if (strcmp(variableandvalues[local_counter].variablestring,p)==0) {
      va = getdoublebyevaluatingstring( variableandvalues[local_counter].valuestring );
      return va;
    }
  }
  printf("Error in getrealvaluefromvariablename. p=%s.\n", p);
  exit(0);
}

double mint; int assignedmint;
double maxt; int assignedmaxt;

void fill_in_variableandvaluestruct() {
  FILE* fin;
  char temps[2000];
  char temps2[2000];
  char variablestring[2000];
  char valuestring[2000];
  nvariableandvalues = 0;
  fin  = fopen( z3throughcommandline_result_filename, "r");
  while (fgets(temps,2000,fin)) {
    if (strncmp(temps,"  (define-fun",13)==0) {
      fgets(temps2,2000,fin);
      fillvariablestringandvaluestring( variablestring, valuestring, temps, temps2);
      strcpy( variableandvalues[ nvariableandvalues].variablestring, variablestring);
      strcpy( variableandvalues[ nvariableandvalues].valuestring,    valuestring);
      nvariableandvalues++; 
      if (nvariableandvalues>MAXNVARSUSEDFORPLOTTING) {
        printf("Error: Not enough memory allocated for plotting.\n");
        exit(-1);
      }
    }
  }
  fclose( fin );
}

void fill_in_mint_and_maxt() {
  int local_counter; double tprime;
  assignedmint = 0; assignedmaxt = 0;
  for (local_counter=0;local_counter<nvariableandvalues;local_counter++) {
    if (strncmp( variableandvalues[ local_counter].variablestring, "t^", 2 )==0) {
      tprime = getdoublebyevaluatingstring( variableandvalues[ local_counter].valuestring );
      if (!assignedmint) { assignedmint = 1; mint = tprime; }
      else               { if (tprime<mint) { mint = tprime; }   } 
      if (!assignedmaxt) { assignedmaxt = 1; maxt = tprime; }
      else               { if (tprime>maxt) { maxt = tprime; }   } 
    }
  }
}

double log10(double temp) {
  return log(temp)/log(10.0);
}

double pow10(double temp) {
  return exp( temp * log(10.0) );
}

void convertnumber_to_mantissa_and_exponent_for_positive_number(double temp, double* psign, double* pa, double* pb) {
  double temp2; double a; double b;
  if (temp == 0.0) { printf("Error in convertnumber_to_mantissa_and_exponent_for_positive_number\n"); exit(0); }
  temp2 = log10( temp);
  b = floor( temp2);
  a = pow10( temp2)/pow10(b);
  *psign = 1.0; *pa = a; *pb = b;
}

void convertnumber_to_mantissa_and_exponent(double temp, double* psign, double* pa, double* pb) {
  if (temp==0.0) {
    *psign = 1.0; *pa = 0; *pb = 0;
  } else {
    if (temp>0.0) {
      convertnumber_to_mantissa_and_exponent_for_positive_number( temp, psign, pa, pb);
    } else {
      convertnumber_to_mantissa_and_exponent_for_positive_number( -temp, psign, pa, pb);
      *psign = -1.0;
    }
  }
}

double from_time_to_x_coordinate(double tempt) {
  return 0 + 1.0 + ((tempt-mint)/(maxt-mint))*8.0;
}

void make_calculations_for_creating_latex_file() {
  double mintsign; double minta; double mintb;
  double maxtsign; double maxta; double maxtb;
  convertnumber_to_mantissa_and_exponent(mint, &mintsign, &minta, &mintb);
  convertnumber_to_mantissa_and_exponent(maxt, &maxtsign, &maxta, &maxtb);
}

void add_mint_and_maxt_mark(FILE* f) {
  fprintf(f, "\\put(%lf,5.1){\\line(0,-1){0.2}}\n", from_time_to_x_coordinate(mint) );
  fprintf(f, "\\put(%lf,4.7){\\tiny{%.2lf}}\n", from_time_to_x_coordinate(mint), mint);
  fprintf(f, "\\put(%lf,5.1){\\line(0,-1){0.2}}\n", from_time_to_x_coordinate(maxt) );
  fprintf(f, "\\put(%lf,4.7){\\tiny{%.2lf}}\n", from_time_to_x_coordinate(maxt), maxt);
}

void add_mint_and_maxt_mark_svg(FILE* f, double w, double h) {
  drawline_svg( f, w, h, from_time_to_x_coordinate(mint), 5.1, from_time_to_x_coordinate(mint), 4.9);
  drawdoubleastext_vertical_svg( f, w, h, from_time_to_x_coordinate(mint), 4.7, mint);
  drawline_svg( f, w, h, from_time_to_x_coordinate(maxt), 5.1, from_time_to_x_coordinate(maxt), 4.9);
  drawdoubleastext_vertical_svg( f, w, h, from_time_to_x_coordinate(maxt), 4.7, maxt);
}

void add_processor_boxes(FILE* f) {
  int proc; double heigth_per_layer; double y_coordinate;
  int nprocessors;
  nprocessors = 1;
  heigth_per_layer = 5.0/(2*nprocessors-1);
  for (proc=1;proc<=nprocessors;proc++) {
    y_coordinate = 10.0 - (proc-1)*2*heigth_per_layer;
    fprintf(f, "\\put(0,%lf){\\line(1,0){1}}\n", y_coordinate);
    fprintf(f, "\\put(0,%lf){\\line(1,0){1}}\n", y_coordinate-heigth_per_layer);
    fprintf(f, "\\put(0,%lf){\\line(0,-1){%lf}}\n", y_coordinate,heigth_per_layer);
    fprintf(f, "\\put(1,%lf){\\line(0,-1){%lf}}\n", y_coordinate,heigth_per_layer);
    fprintf(f, "\\put(0.1,%lf){\\tiny{$P_%d$}}\n", y_coordinate-heigth_per_layer/2, proc);
  }
}

void add_processor_boxes_svg(FILE* f, double w, double h) {
  int proc; double heigth_per_layer; double y_coordinate;
  int nprocessors;
  nprocessors = 1;
  heigth_per_layer = 5.0/(2*nprocessors-1);
  for (proc=1;proc<=nprocessors;proc++) {
    y_coordinate = 10.0 - (proc-1)*2*heigth_per_layer;
    drawline_svg( f, w, h, 0.0, y_coordinate,                  1.0,  y_coordinate                  );
    drawline_svg( f, w, h, 0.0, y_coordinate-heigth_per_layer, 1.0,  y_coordinate-heigth_per_layer );
    drawline_svg( f, w, h, 0.0, y_coordinate,                  0.0,  y_coordinate-heigth_per_layer );
    drawline_svg( f, w, h, 1.0, y_coordinate,                  1.0,  y_coordinate-heigth_per_layer );
    drawintasprocessor_svg( f, w, h, 0.1, y_coordinate-heigth_per_layer/2, proc); 
  }
}

void add_execution_on_processors(FILE* f, int iD) {
  int proc; double heigth_per_layer; double y_coordinate;
  int i; int k; int v; int pos;
  char varname[2000];
  int flag;
  double tstart; double tfinish; double xstart; double xfinish; double xwidth;
  int nprocessors;
  nprocessors = 1;
  heigth_per_layer = 5.0/(2*nprocessors-1);
  for (proc=1;proc<=nprocessors;proc++) {
    y_coordinate = 10.0 - (proc-1)*2*heigth_per_layer;
    for (i=1;i<=ntasks;i++) {
      if ((is_in_hp(i,iD)) || (i==iD)) {
          for (k=1;k<=ceil(tasks[iD].D/tasks[i].T);k++) {
            for (pos=1;pos<=getnpos(iD);pos++) {
              sprintf( varname,"x_%d_%d^%d", i,k,pos);
              flag = getbooleanvaluefromvariablename( varname);
              if (flag) {
                sprintf( varname,"t^%d", pos);
                tstart = getrealvaluefromvariablename( varname);
                sprintf( varname,"t^%d", pos+1);
                tfinish = getrealvaluefromvariablename( varname);
                xstart  = from_time_to_x_coordinate(tstart);
                xfinish = from_time_to_x_coordinate(tfinish);
                xwidth =  xfinish - xstart;
                if (xwidth<0) { printf("Error in add_execution_on_processors. proc=%d, i=%d, v=%d, k=%d, pos=%d.\n", proc,i,v,k,pos); printf("tstart=%lf, tfinish=%lf, xstart=%lf, xfinish=%lf\n", tstart, tfinish, xstart, xfinish); exit(0); }
                fprintf(f, "\\put(%lf,%lf){\\line(1,0){%lf}}\n",         xstart,  y_coordinate,                  xwidth);
                fprintf(f, "\\put(%lf,%lf){\\line(1,0){%lf}}\n",         xstart,  y_coordinate-heigth_per_layer, xwidth);
                fprintf(f, "\\put(%lf,%lf){\\line(0,-1){%lf}}\n",        xstart,  y_coordinate, heigth_per_layer);
                fprintf(f, "\\put(%lf,%lf){\\line(0,-1){%lf}}\n",        xfinish, y_coordinate, heigth_per_layer);
                fprintf(f, "\\put(%lf,%lf){\\tiny{$\\tau_{%d,%d}$}}\n", xstart,  y_coordinate-heigth_per_layer/2, i, k);
              }
            }
          }
      }
    }
  }
}

#define MAXNCOLORSFORBACKGROUNDOFTASKS 3
int ncolorsforbackgroundoftasks;
struct colorforbackgroundoftaskstruct {
  char thecolortext[200];
};
struct colorforbackgroundoftaskstruct colorforbackgroundoftask[MAXNCOLORSFORBACKGROUNDOFTASKS];

void initcolorforbackgroundoftask() {
  ncolorsforbackgroundoftasks = MAXNCOLORSFORBACKGROUNDOFTASKS;
  strcpy( colorforbackgroundoftask[0].thecolortext, "red" );
  strcpy( colorforbackgroundoftask[1].thecolortext, "blue" ); 
  strcpy( colorforbackgroundoftask[2].thecolortext, "green" ); 
}
void getbackgroundcolorfromtaskindex( int i, char* p_backgroundcolor_destination) {
  strcpy( p_backgroundcolor_destination, colorforbackgroundoftask[i % ncolorsforbackgroundoftasks].thecolortext );
}

void add_execution_on_processors_svg(FILE* f, double w, double h, int iD) {
  int proc; double heigth_per_layer; double y_coordinate;
  int i; int k; int v; int pos;
  char varname[2000];
  int flag;
  double tstart; double tfinish; double xstart; double xfinish; double xwidth;
  int nprocessors;
  char backgroundcolor[200];

  initcolorforbackgroundoftask();

  nprocessors = 1;
  heigth_per_layer = 5.0/(2*nprocessors-1);
  for (proc=1;proc<=nprocessors;proc++) {
    y_coordinate = 10.0 - (proc-1)*2*heigth_per_layer;
    for (i=1;i<=ntasks;i++) {
      if ((is_in_hp(i,iD)) || (i==iD)) {
          for (k=1;k<=ceil(tasks[iD].D/tasks[i].T);k++) {
            for (pos=1;pos<=getnpos(iD);pos++) {
              sprintf( varname,"x_%d_%d^%d", i,k,pos);
              flag = getbooleanvaluefromvariablename( varname);
              if (flag) {
                sprintf( varname,"t^%d", pos);
                tstart = getrealvaluefromvariablename( varname);
                sprintf( varname,"t^%d", pos+1);
                tfinish = getrealvaluefromvariablename( varname);
                xstart  = from_time_to_x_coordinate(tstart);
                xfinish = from_time_to_x_coordinate(tfinish);
                xwidth =  xfinish - xstart;
                if (xwidth<0) { printf("Error in add_execution_on_processors_svg. proc=%d, i=%d, v=%d, k=%d, pos=%d.\n", proc,i,v,k,pos); printf("tstart=%lf, tfinish=%lf, xstart=%lf, xfinish=%lf\n", tstart, tfinish, xstart, xfinish); exit(0); }

                getbackgroundcolorfromtaskindex( i-1, backgroundcolor);
                if (enable_drawschedulerectanglesinhalfheight) {
                  drawbox_svg( f, w, h, xstart,  y_coordinate-heigth_per_layer, xstart+xwidth,  y_coordinate-heigth_per_layer/2, backgroundcolor );
                  drawtexttau_i_k_colorspecified_vertical_svg( f, w, h, xstart, y_coordinate-heigth_per_layer+(heigth_per_layer/4), i, k, "white"); 
                } else {
                  drawbox_svg( f, w, h, xstart,  y_coordinate-heigth_per_layer, xstart+xwidth,  y_coordinate, backgroundcolor );
                  drawtexttau_i_k_colorspecified_vertical_svg( f, w, h, xstart, y_coordinate-heigth_per_layer/2, i, k, "white"); 
                }
              }
            }
          }
      }
    }
  }
}

void add_tau_symbols(FILE* f) {
  int i; double heigth_per_layer; double y_coordinate;
  heigth_per_layer = 5.0/(2*ntasks);
  for (i=1;i<=ntasks;i++) {
    y_coordinate = 5.0 - (heigth_per_layer + (i-1)*2*heigth_per_layer);
    fprintf(f, "\\put(0.1,%lf){\\tiny{$\\tau_%d$}}\n", y_coordinate-heigth_per_layer/2, i);
  }
}

void add_tau_symbols_svg(FILE* f, double w, double h) {
  int i; double heigth_per_layer; double y_coordinate;
  heigth_per_layer = 5.0/(2*ntasks);
  for (i=1;i<=ntasks;i++) {
    y_coordinate = 5.0 - (heigth_per_layer + (i-1)*2*heigth_per_layer);
    drawtexttau_i_svg( f, w, h, 0.1, y_coordinate-heigth_per_layer/2, i);
  }
}

void add_job_arrivals(FILE* f, int iD, int showZinstant, int showabsdeadlines) {
  int i; double heigth_per_layer; double y_coordinate;
  int k; char temps[2000]; double arrivaltime;
  heigth_per_layer = 5.0/(2*ntasks);
  for (i=1;i<=ntasks;i++) {
    if ((is_in_hp(i,iD)) || (i==iD)) {
      y_coordinate = 5.0 - (heigth_per_layer + (i-1)*2*heigth_per_layer);
      for (k=1;k<=ceil(tasks[iD].D/tasks[i].T);k++) {
        sprintf( temps,"A_%d_%d", i, k);
        arrivaltime = getrealvaluefromvariablename(temps);
        fprintf(f, "\\put(%lf,%lf){\\vector(0,1){%lf}}\n",    from_time_to_x_coordinate(arrivaltime), y_coordinate-heigth_per_layer, heigth_per_layer );
        if (showZinstant) {
          fprintf(f, "\\put(%lf,%lf){\\line(0,-1){%lf}}\n", from_time_to_x_coordinate(arrivaltime+tasks[i].Z), y_coordinate, heigth_per_layer );
        }
        if (showabsdeadlines) {
          fprintf(f, "\\put(%lf,%lf){\\vector(0,-1){%lf}}\n", from_time_to_x_coordinate(arrivaltime+tasks[i].D), y_coordinate, heigth_per_layer );
        }
      }
    }
  }  
}

void add_job_arrivals_svg(FILE* f, double w, double h, int iD, int showZinstant, int showabsdeadlines) {
  int i; double heigth_per_layer; double y_coordinate;
  int k; char temps[2000]; double arrivaltime;
  heigth_per_layer = 5.0/(2*ntasks);
  for (i=1;i<=ntasks;i++) {
    if ((is_in_hp(i,iD)) || (i==iD)) {
      y_coordinate = 5.0 - (heigth_per_layer + (i-1)*2*heigth_per_layer);
      for (k=1;k<=ceil(tasks[iD].D/tasks[i].T);k++) {
        sprintf( temps,"A_%d_%d", i, k);
        arrivaltime = getrealvaluefromvariablename(temps);
        drawarrowup( f, w, h, from_time_to_x_coordinate(arrivaltime), y_coordinate-heigth_per_layer, heigth_per_layer );
        if (showZinstant) {
          drawlinedown( f, w, h, from_time_to_x_coordinate(arrivaltime+tasks[i].Z), y_coordinate, heigth_per_layer );
        }
        if (showabsdeadlines) {
          drawarrowdown( f, w, h, from_time_to_x_coordinate(arrivaltime+tasks[i].D), y_coordinate, heigth_per_layer );
        }
      }
    }
  }  
}

void create_latex_file_with_visualization_of_failure(char* latexfn, int iD) {
  FILE* f;
  f = fopen( latexfn, "w");
  fprintf(f, "\\documentclass[12pt, letterpaper]{article}\n");
  fprintf(f, "\\begin{document}\n");
  fprintf(f, "\\setlength{\\unitlength}{1.0cm}\n");
  fprintf(f, "\\begin{picture}(10,10)\n");
  fprintf(f, "\\put(1,5){\\vector(1,0){9}}\n");
  make_calculations_for_creating_latex_file();
  add_mint_and_maxt_mark(f);
  if (enable_drawprocessor_boxes) {
    add_processor_boxes(f);
  }
  add_execution_on_processors(f,iD);
  add_tau_symbols(f);
  add_job_arrivals(f, iD, 1, 1);
  fprintf(f, "\\end{picture}\n");
  fprintf(f, "\\end{document}\n");   
  fclose( f);
}

// the code for creating svg assumes a canvas that is 1300x650 but the code for creating latex assumes a canvas that
// it 10x10.

void create_svg_file_with_visualization_of_failure(char* svgfn, int iD) {
  FILE* f; double w; double h;
  f = fopen( svgfn, "w");
  if (f==NULL) { printf("Error opening file in function create_svg_file_with_visualization_of_failure. svgfn=%s\n", svgfn); fflush(stdout); exit(0); }
  fprintf( f, "<!DOCTYPE html>\n");
  fprintf( f, "<html>\n");
  fprintf( f, "<body>\n");

  w = 1300; h = 650;

  fprintf( f, "<svg xmlns=\"http://www.w3.org/2000/svg\" width=\"%lf\" height=\"%lf\">\n", w,h);
  drawarrowright( f, w, h, 1, 5, 9 );
  
  make_calculations_for_creating_latex_file();
  add_mint_and_maxt_mark_svg(f,w,h);
  if (enable_drawprocessor_boxes) {
    add_processor_boxes_svg(f,w,h);
  }
  add_execution_on_processors_svg(f,w,h,iD);
  add_tau_symbols_svg(f,w,h);
  add_job_arrivals_svg(f,w,h, iD, 1, 1);
  fprintf( f, "</svg>\n");
  fprintf( f, "</body>\n");
  fprintf( f, "</html>\n");
  fclose( f);
}

#if COMPILEMSVS
unsigned __int128 diff_us_timeval(struct timeval *x, struct timeval *y)
{
  unsigned __int128 amillion = 1000000;
  unsigned __int128 u = ((x->tv_sec * amillion) + x->tv_usec);
  unsigned __int128 v = ((y->tv_sec * amillion) + y->tv_usec);
  return u-v;
}
double diff_s_timeval(struct timeval *x, struct timeval *y)
{
  unsigned __int128 amillion = 1000000;
  unsigned __int128 t;
  unsigned __int128 tsec;
  unsigned __int128 tusec;
  double t_as_double_secondpart;
  double t_as_double_usecondpart;
  double t_as_double;
  t = diff_us_timeval( x, y);
  tsec = t / amillion;
  tusec =  t % amillion; 
  t_as_double_secondpart = tsec;
  t_as_double_usecondpart = tusec;
  t_as_double_usecondpart = t_as_double_usecondpart / amillion;
  t_as_double = t_as_double_secondpart + t_as_double_usecondpart; 
  return t_as_double;
}
#else
unsigned long long diff_ns_timespec(struct timespec *x, struct timespec *y) {
  unsigned long long abillion = 1000000000;
  unsigned long long u;
  u = x->tv_sec;
  u = u * abillion;
  u = u + x->tv_nsec;

  unsigned long long v;
  v = y->tv_sec;
  v = v * abillion;
  v = v + y->tv_nsec;
  return u-v;
}
double diff_s_timespec (struct timespec *x, struct timespec *y)
{
  unsigned long long abillion = 1000000000;
  unsigned long long t;
  unsigned long long tsec;
  unsigned long long tnsec;
  double t_as_double_secondpart;
  double t_as_double_usecondpart;
  double t_as_double;
  t = diff_ns_timespec( x, y);
  tsec = t / abillion;
  tnsec =  t % abillion; 
  t_as_double_secondpart = tsec;
  t_as_double_usecondpart = tnsec;
  t_as_double_usecondpart = t_as_double_usecondpart / abillion;
  t_as_double = t_as_double_secondpart + t_as_double_usecondpart; 
  return t_as_double;
}
#endif

#if COMPILEMSVS

#define CLOCK_REALTIME 0
LARGE_INTEGER getFILETIMEoffset()
{
    SYSTEMTIME s;
    FILETIME f;
    LARGE_INTEGER t;
    s.wYear = 1970;
    s.wMonth = 1;
    s.wDay = 1;
    s.wHour = 0;
    s.wMinute = 0;
    s.wSecond = 0;
    s.wMilliseconds = 0;
    SystemTimeToFileTime(&s, &f);
    t.QuadPart = f.dwHighDateTime;
    t.QuadPart <<= 32;
    t.QuadPart |= f.dwLowDateTime;
    return (t);
}
 
int my_clock_gettime(int X, struct timeval *tv)
{
  LARGE_INTEGER           t;
  FILETIME            f;
  double                  microseconds;
  static LARGE_INTEGER    offset;
  static double           frequencyToMicroseconds;
  static int              initialized = 0;
  static BOOL             usePerformanceCounter = 0;
  if (!initialized) {
    LARGE_INTEGER performanceFrequency;
    initialized = 1;
    usePerformanceCounter = QueryPerformanceFrequency(&performanceFrequency);
    if (usePerformanceCounter) {
      QueryPerformanceCounter(&offset);
      frequencyToMicroseconds = (double)performanceFrequency.QuadPart / 1000000.;
    } else {
      offset = getFILETIMEoffset();
      frequencyToMicroseconds = 10.;
    }
  }
  if (usePerformanceCounter) { QueryPerformanceCounter(&t); }
  else {
    GetSystemTimeAsFileTime(&f);
    t.QuadPart = f.dwHighDateTime;
    t.QuadPart <<= 32;
    t.QuadPart |= f.dwLowDateTime;
  }
  t.QuadPart -= offset.QuadPart;
  microseconds = (double)t.QuadPart / frequencyToMicroseconds;
  t.QuadPart = microseconds;
  tv->tv_sec = t.QuadPart / 1000000;
  tv->tv_usec = t.QuadPart % 1000000;
  return (0);
}
#endif


void parsearguments( int argc, char *argv[], char *envp[]) {
  int i;
  i = 1;
  while (i<=argc-1) {
    if (strcmp( argv[i], "-i")==0) {
      strcpy( inputfilename, argv[i+1] );
      i = i + 2;
    } else {
      if (strcmp( argv[i], "-o")==0) {
        strcpy( outputfilename, argv[i+1] );
        i = i + 2;
      } else {
        if (strcmp( argv[i], "-m")==0) {
          metathing = 1;
          i = i + 1;
        } else {
	  if (strcmp( argv[i], "-p")==0){
	    strcpy(plotfilename, argv[i+1]);
	    i = i + 2;
	  } else {
	    i++;
	  }
        }
      }
    }
  }
}

void add_line_verbose100()    { fprintf( z3throughcommandlinesmt2file, "(set-option :verbose 100)\n"); }
void add_line_logic_QF_LIRA() { fprintf( z3throughcommandlinesmt2file, "(set-logic QF_LIRA)\n"); }
void add_line_logic_QF_DIRA() { fprintf( z3throughcommandlinesmt2file, "(set-logic QF_DIRA)\n"); } // DIRA is not supported. So don't use it.
void add_line_logic_QF_LRA() { fprintf( z3throughcommandlinesmt2file, "(set-logic QF_LRA)\n"); }
void add_line_checksat()      { fprintf( z3throughcommandlinesmt2file, "(check-sat)\n"); }
void add_line_getmodel()   { fprintf( z3throughcommandlinesmt2file, "(get-model)\n"); }
void createcommandstring_for_is_cprsmtinstance_satisfiable() { fprintf(commandstringwithscriptfile,"z3 %s > %s", z3throughcommandlinesmt2filename, z3throughcommandline_result_filename); }

void addt(int iD) {
  int p;
  for (p=1;p<=getnpos(iD)+1;p++) {
    fprintf( z3throughcommandlinesmt2file, "(declare-const t^%d Real)\n", p);
  }
}
void addrealvariableforjob(char* tempstr, int iD) {
  int j; int q;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {   
        fprintf( z3throughcommandlinesmt2file, "(declare-const %s_%d_%d Real)\n", tempstr, j,q);
      }
    }
  }
}
void addA(int iD) { addrealvariableforjob("A", iD); }
void addc(int iD) { addrealvariableforjob("c", iD); }
void adde(int iD) { addrealvariableforjob("e", iD); }
void addrealvariableforjobforposition(char* tempstr, int iD) {
  int j; int q; int p;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {   
        for (p=1;p<=getnpos(iD)+1;p++) {
          fprintf( z3throughcommandlinesmt2file, "(declare-const %s_%d_%d^%d Real)\n", tempstr, j,q,p);
        }
      }
    }
  }
}
void addexecc(int iD)      { addrealvariableforjobforposition("execc", iD); }
void addexece(int iD)      { addrealvariableforjobforposition("exece", iD); }
void addintvariableforjob(char* tempstr, int iD) {
  int j; int q;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {   
        fprintf( z3throughcommandlinesmt2file, "(declare-const %s_%d_%d Int)\n", tempstr, j,q);
      }
    }
  }
}
void addarrivespos(int iD)  { addintvariableforjob("arrivespos", iD); }
void addZexpirespos(int iD) { addintvariableforjob("Zexpirespos", iD); }
void addDexpirespos(int iD) { addintvariableforjob("Dexpirespos", iD); }
void addintvariablefortaskpos_even_for_pos_zero(char* tempstr, int iD) {
  int j; int p;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (p=0;p<=getnpos(iD)+1;p++) {
        fprintf( z3throughcommandlinesmt2file, "(declare-const %s_%d^%d Int)\n", tempstr, j,p);
      }
    }
  }
}
void addcounters(int iD) { addintvariablefortaskpos_even_for_pos_zero("counter", iD); } 
void addboolvariableforjob(char* tempstr, int iD) {
  int j; int q;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {   
        fprintf( z3throughcommandlinesmt2file, "(declare-const %s_%d_%d Bool)\n", tempstr, j,q);
      }
    }
  }
}
void addrespectC(int iD) { addboolvariableforjob("respectC", iD); }
void addboolvariableforjobforpos(char* tempstr, int iD) {
  int j; int q; int p;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {   
        for (p=1;p<=getnpos(iD)+1;p++) {
          fprintf( z3throughcommandlinesmt2file, "(declare-const %s_%d_%d^%d Bool)\n", tempstr, j,q,p);
        }
      }
    }
  }
}
void addelig(int iD) { addboolvariableforjobforpos("elig", iD); }
void addx(int iD)    { addboolvariableforjobforpos("x", iD); }
void addoe(int iD) {
  int j; int q; int p;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
        for (p=1;p<=getnpos(iD)+1;p++) {
          fprintf( z3throughcommandlinesmt2file, "(declare-const oe_%d_%d^%d^%d Bool)\n", j,q,p,1);
          fprintf( z3throughcommandlinesmt2file, "(declare-const oe_%d_%d^%d^%d Bool)\n", j,q,p,2);
          fprintf( z3throughcommandlinesmt2file, "(declare-const oe_%d_%d^%d^%d Bool)\n", j,q,p,3);
          fprintf( z3throughcommandlinesmt2file, "(declare-const oe_%d_%d^%d^%d Bool)\n", j,q,p,4);
          fprintf( z3throughcommandlinesmt2file, "(declare-const oe_%d_%d^%d^%d Bool)\n", j,q,p,5);
        }
      }
    }
  }
}
void is_cprsmtinstance_satisfiable_declare_all_variables(int iD) {
  addt(iD);
  addA(iD);
  addc(iD);
  adde(iD);
  addexecc(iD);
  addexece(iD);
  addarrivespos(iD);
  addZexpirespos(iD);
  addDexpirespos(iD);
  addcounters(iD);
  addrespectC(iD);
  addelig(iD);
  addx(iD);
  addoe(iD);
}

void addconstraintposorder(int iD) {
  int p;
  for (p=1;p<=getnpos(iD);p++) {
    fprintf( z3throughcommandlinesmt2file, "(assert ( ");
    fprintf( z3throughcommandlinesmt2file, " <= t^%d t^%d ", p, p+1);
    fprintf( z3throughcommandlinesmt2file, "))\n");
  }
}
void addconstraintfirstposisattimezero() {
  fprintf( z3throughcommandlinesmt2file, "(assert ( ");
  fprintf( z3throughcommandlinesmt2file, " = t^1 0");
  fprintf( z3throughcommandlinesmt2file, "))\n");
}
void addconstraintcounterinpositionzero_is_nonnegative(int iD) {
  int j;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      fprintf( z3throughcommandlinesmt2file, "(assert ( ");
      fprintf( z3throughcommandlinesmt2file, " >= counter_%d^0 0", j);
      fprintf( z3throughcommandlinesmt2file, "))\n");
    }
  }
}
void print_lower_and_upper_bound_on_jobvariable(char* tempstr,int j,int q,int iD,int lo,int hi) {
  fprintf( z3throughcommandlinesmt2file, "( and (<= %d %s_%d_%d) (<= %s_%d_%d %d) )",lo,tempstr,j,q,tempstr,j,q,hi);
}

void addconstraintpositionsareinrange(int iD) {
  int j; int q;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
        fprintf( z3throughcommandlinesmt2file, "(assert ( and ");
        print_lower_and_upper_bound_on_jobvariable("arrivespos", j,q,iD,3*(q-1)+1,getnpos(iD)+1 - 2 - 3*(ceil(tasks[iD].D/tasks[j].T)-q) ); fprintf( z3throughcommandlinesmt2file, " ");
        print_lower_and_upper_bound_on_jobvariable("Zexpirespos",j,q,iD,3*(q-1)+2,getnpos(iD)+1 - 1 - 3*(ceil(tasks[iD].D/tasks[j].T)-q) ); fprintf( z3throughcommandlinesmt2file, " ");
        print_lower_and_upper_bound_on_jobvariable("Dexpirespos",j,q,iD,3*(q-1)+3,getnpos(iD)+1     - 3*(ceil(tasks[iD].D/tasks[j].T)-q) ); fprintf( z3throughcommandlinesmt2file, " ");
        fprintf( z3throughcommandlinesmt2file, "))\n");
      }
    }
  }
}
void addconstrainteventsimplytimes(int iD) {
  int j; int q; int p;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
        for (p=1;p<=getnpos(iD)+1;p++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( and ");
          fprintf( z3throughcommandlinesmt2file, "( => ( = arrivespos_%d_%d  %d ) ( =     A_%d_%d       t^%d ) ) ",j,q,p,j,q,p);
          fprintf( z3throughcommandlinesmt2file, "( => ( = Zexpirespos_%d_%d %d ) ( = ( + A_%d_%d %lf ) t^%d ) ) ",j,q,p,j,q,tasks[j].Z,p);
          fprintf( z3throughcommandlinesmt2file, "( => ( = Dexpirespos_%d_%d %d ) ( = ( + A_%d_%d %lf ) t^%d ) ) ",j,q,p,j,q,tasks[j].D,p);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
}
void addconstraint_Dexpiresprecedesnextarrival(int iD) {
  int j; int q;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        fprintf( z3throughcommandlinesmt2file, "(assert ( ");
        fprintf( z3throughcommandlinesmt2file, "  <= ( + Dexpirespos_%d_%d 1 ) arrivespos_%d_%d ",j,q,j,q+1);
        fprintf( z3throughcommandlinesmt2file, "))\n");
      }
    }
  }
}

void printconstrainte(int j,int q) {
  fprintf( z3throughcommandlinesmt2file, "( and ( <= 0 c_%d_%d ) ( => respectC_%d_%d ( <= c_%d_%d %lf ) ) ) ", j,q,j,q,j,q,tasks[j].C);
}
void printconstraintc(int j,int q) {
  fprintf( z3throughcommandlinesmt2file, "( and ( <= 0 e_%d_%d ) ( <= e_%d_%d %lf ) ) ", j,q,j,q,tasks[j].E);
}
void addconstraintcande(int iD) {
  int j; int q;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
        fprintf( z3throughcommandlinesmt2file, "(assert ( and ");
        printconstraintc(j,q); fprintf( z3throughcommandlinesmt2file, " ");
        printconstrainte(j,q); fprintf( z3throughcommandlinesmt2file, " ");
        fprintf( z3throughcommandlinesmt2file, "))\n");
      }
    }
  }
}
void addconstraintminimumarrivaltime(int iD) {
  int j; int q;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        fprintf( z3throughcommandlinesmt2file, "(assert ( ");
        fprintf( z3throughcommandlinesmt2file, " <= ( + A_%d_%d %lf) A_%d_%d  ",j,q,tasks[j].T,j,q+1);
        fprintf( z3throughcommandlinesmt2file, "))\n");
      }
    }
  }
}

void addconstraintatleastonerespectC(int iD) {
  int j; int q; int qprime;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-(tasks[j].RC-1);q++) {
        fprintf( z3throughcommandlinesmt2file, "(assert ( or ");
        for (qprime=q;qprime<=q+tasks[j].RC-1;qprime++) {
          fprintf( z3throughcommandlinesmt2file, "respectC_%d_%d ",j,qprime);
        }
        fprintf( z3throughcommandlinesmt2file, "))\n");
      }
    }
  }
}

void printnotyetfinished(int j,int q,int p) {
  int pprime;
  for (pprime=1;pprime<=p;pprime++) {
    fprintf( z3throughcommandlinesmt2file, "( not oe_%d_%d^%d^1 ) ", j,q,pprime);   
    fprintf( z3throughcommandlinesmt2file, "( not oe_%d_%d^%d^2 ) ", j,q,pprime);   
    fprintf( z3throughcommandlinesmt2file, "( not oe_%d_%d^%d^3 ) ", j,q,pprime);   
    fprintf( z3throughcommandlinesmt2file, "( not oe_%d_%d^%d^4 ) ", j,q,pprime);   
    fprintf( z3throughcommandlinesmt2file, "( not oe_%d_%d^%d^5 ) ", j,q,pprime);   
  }
}

void printeligdef(int j,int q,int p,int iD) {
  fprintf( z3throughcommandlinesmt2file, "( = elig_%d_%d^%d ",j,q,p);
  if (p>=2) {
    fprintf( z3throughcommandlinesmt2file, "( and ");
        fprintf( z3throughcommandlinesmt2file, "( <= arrivespos_%d_%d  %d ) ", j,q,p);
        printnotyetfinished( j,q,p);
    fprintf( z3throughcommandlinesmt2file, ") ");
  } else {
        fprintf( z3throughcommandlinesmt2file, "( <= arrivespos_%d_%d  %d ) ", j,q,p);
  }
  fprintf( z3throughcommandlinesmt2file, ")");
}

int getnhptasks(int j,int iD) {
  int temp; int jprime;
  temp = 0;
  for (jprime=1;jprime<=ntasks;jprime++) {
    if (is_in_hp(jprime,j)) {
      temp = temp + 1;
    }
  }
  return temp;
}
void printnohpelig(int j,int q,int p,int iD) {
  int jprime; int qprime;
  fprintf( z3throughcommandlinesmt2file, "( and ");
  for (jprime=1;jprime<=ntasks;jprime++) {
    if (is_in_hp(jprime,j)) {
      for (qprime=1;qprime<=ceil(tasks[iD].D/tasks[jprime].T);qprime++) {
        fprintf( z3throughcommandlinesmt2file, "( not elig_%d_%d^%d ) ", jprime,qprime,p);
      }
    }
  }
  fprintf( z3throughcommandlinesmt2file, ")");
}
void printxdef(int j,int q, int p,int iD) {
  fprintf( z3throughcommandlinesmt2file, "( = x_%d_%d^%d ",j,q,p);
    if (getnhptasks(j,iD)>0) {
      fprintf( z3throughcommandlinesmt2file, "( and ");
        fprintf( z3throughcommandlinesmt2file, "elig_%d_%d^%d ", j,q,p);
        printnohpelig(j,q,p,iD); fprintf( z3throughcommandlinesmt2file, " ");
      fprintf( z3throughcommandlinesmt2file, ")");
    } else {
        fprintf( z3throughcommandlinesmt2file, "elig_%d_%d^%d ", j,q,p);
    }
  fprintf( z3throughcommandlinesmt2file, ")");
}
void addconstraintdispatching(int iD) {
  int j; int q; int p;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
        for (p=1;p<=getnpos(iD);p++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( and ");
          printeligdef(j,q,p,iD); fprintf( z3throughcommandlinesmt2file, " ");
          printxdef(j,q,p,iD);    fprintf( z3throughcommandlinesmt2file, " ");
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
}

void addconstraintxandexeccexece(int iD) {
  int j; int q; int p;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
        for (p=1;p<=getnpos(iD);p++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( and ");
          fprintf( z3throughcommandlinesmt2file, "( =>       ( and          x_%d_%d^%d          ( < %d Zexpirespos_%d_%d )   ) ( = execc_%d_%d^%d ( - t^%d t^%d) ) ) ",j,q,p,p,j,q,j,q,p,p+1,p);
          fprintf( z3throughcommandlinesmt2file, "( =>       ( and   ( not  x_%d_%d^%d )        ( < %d Zexpirespos_%d_%d )   ) ( = execc_%d_%d^%d              0 ) ) ",j,q,p,p,j,q,j,q,p      );
          fprintf( z3throughcommandlinesmt2file, "( =>                                    ( not ( < %d Zexpirespos_%d_%d ) )   ( = execc_%d_%d^%d              0 ) ) ",      p,j,q,j,q,p      );
          fprintf( z3throughcommandlinesmt2file, "( =>       ( and          x_%d_%d^%d    ( not ( < %d Zexpirespos_%d_%d ) ) ) ( = exece_%d_%d^%d ( - t^%d t^%d) ) ) ",j,q,p,p,j,q,j,q,p,p+1,p);
          fprintf( z3throughcommandlinesmt2file, "( =>       ( and   ( not  x_%d_%d^%d )  ( not ( < %d Zexpirespos_%d_%d ) ) ) ( = exece_%d_%d^%d              0 ) ) ",j,q,p,p,j,q,j,q,p      );
          fprintf( z3throughcommandlinesmt2file, "( =>                                          ( <   %d Zexpirespos_%d_%d )   ( = exece_%d_%d^%d              0 ) ) ",      p,j,q,j,q,p      );
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
}

void print_atleastone_oe(int j, int q, int iD) {
  int p; int o;
  fprintf( z3throughcommandlinesmt2file, "( or ");
  for (p=1;p<=getnpos(iD)+1;p++) {
    for (o=1;o<=5;o++) {
      fprintf( z3throughcommandlinesmt2file, " oe_%d_%d^%d^%d ", j,q,p,o);
    }
  }
  fprintf( z3throughcommandlinesmt2file, ")");
}
void print_notwo_oe(int j, int q, int iD) {
  int pprime;      int oprime;
  int pprimeprime; int oprimeprime;
  fprintf( z3throughcommandlinesmt2file, "( and ");
  for (pprime=1;pprime<=getnpos(iD)+1;pprime++) {
    for (oprime=1;oprime<=5;oprime++) {
      for (pprimeprime=1;pprimeprime<=getnpos(iD)+1;pprimeprime++) {
        for (oprimeprime=1;oprimeprime<=5;oprimeprime++) {
          if ( ((pprime==pprimeprime) && (oprime<oprimeprime)) || (pprime<pprimeprime)) {
            fprintf( z3throughcommandlinesmt2file, " ( not ( and oe_%d_%d^%d^%d oe_%d_%d^%d^%d ) ) ", j,q,pprime,oprime, j,q,pprimeprime,oprimeprime);
          }
        }
      }
    }
  }
  fprintf( z3throughcommandlinesmt2file, ")");
}


void addconstraint_range_o_and_range_of_op(int iD) {
  int j; int q;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
        fprintf( z3throughcommandlinesmt2file, "(assert ( and ");
        print_atleastone_oe(j,q, iD);
        print_notwo_oe(j,q, iD);
        fprintf( z3throughcommandlinesmt2file, "))\n");
      }
    }
  }
}

void print_oe(int j,int q,int p,int o) { fprintf( z3throughcommandlinesmt2file, " oe_%d_%d^%d^%d ",j,q,p,o); }

void printsumexecrelatestosymbol(int j,int q,int pprime,int p,char* relopstring,char* tempsterm,char* temps) {
  int piterator;
  if (pprime+1>p) { printf("Error in printsumexecrelatestosymbol.\n"); exit(-1); }
  fprintf( z3throughcommandlinesmt2file, "( %s ", relopstring);
  if (pprime+1<p) {
    fprintf( z3throughcommandlinesmt2file, "( + ");
    for (piterator=pprime;piterator<=p-1;piterator++) { fprintf( z3throughcommandlinesmt2file, "%s_%d_%d^%d ",tempsterm,j,q,piterator); }
    fprintf( z3throughcommandlinesmt2file, ")");
  } else {
    fprintf( z3throughcommandlinesmt2file, "%s_%d_%d^%d ",tempsterm,j,q,p-1); 
  }
  fprintf( z3throughcommandlinesmt2file, " %s_%d_%d ", temps,j,q); 
  fprintf( z3throughcommandlinesmt2file, ")");
}
void printfsumexecequalsc(           int j,int q,int pprime,int p) { printsumexecrelatestosymbol(j,q,pprime,p,"=", "execc","c"); }
void printfsumexecstrictlylessthanc( int j,int q,int pprime,int p) { printsumexecrelatestosymbol(j,q,pprime,p,"<", "execc","c"); }
void printfsumexeclessthanorequaltoc(int j,int q,int pprime,int p) { printsumexecrelatestosymbol(j,q,pprime,p,"<=","execc","c"); }
void printfsumexecequalse(           int j,int q,int pprime,int p) { printsumexecrelatestosymbol(j,q,pprime,p,"=", "exece","e"); }
void printfsumexecstrictlylessthane( int j,int q,int pprime,int p) { printsumexecrelatestosymbol(j,q,pprime,p,"<", "exece","e"); }
void printfsumexeclessthanorequaltoe(int j,int q,int pprime,int p) { printsumexecrelatestosymbol(j,q,pprime,p,"<=","exece","e"); }

void addconstraint_oe_implications(int iD,int o) {
  int j; int q; int p;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
        for (p=1;p<=getnpos(iD)+1;p++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( => ");
          print_oe(j,q,p,o); fprintf( z3throughcommandlinesmt2file, " ");
          switch (o) {
            case 1 :
              fprintf( z3throughcommandlinesmt2file, "( and ");
              fprintf( z3throughcommandlinesmt2file, "( <= arrivespos_%d_%d %d ) ( <= %d Zexpirespos_%d_%d ) ",j,q,p,p,j,q);
              if (p>=2) { printfsumexeclessthanorequaltoc(j,q,1,p); fprintf( z3throughcommandlinesmt2file, " "); }
              fprintf( z3throughcommandlinesmt2file, "( >= counter_%d^%d 1 ) ",j,p-1);
              fprintf( z3throughcommandlinesmt2file, "( = counter_%d^%d ( - counter_%d^%d 1 ) ) ",j,p,j,p-1);
              fprintf( z3throughcommandlinesmt2file, ") ");
              break;
            case 2 :
              if (p==1) {
                fprintf( z3throughcommandlinesmt2file, "false ");
              } else {
                fprintf( z3throughcommandlinesmt2file, "( and ");
                fprintf( z3throughcommandlinesmt2file, "( < arrivespos_%d_%d %d ) ( <= %d Zexpirespos_%d_%d ) ",j,q,p,p,j,q);
                fprintf( z3throughcommandlinesmt2file, "x_%d_%d^%d ",j,q,p-1);
                printfsumexecequalsc(j,q,1,p); fprintf( z3throughcommandlinesmt2file, " ");
                fprintf( z3throughcommandlinesmt2file, "( < counter_%d^%d %d ) ",j,p-1,tasks[j].MAXCOUNT);
                fprintf( z3throughcommandlinesmt2file, "( = counter_%d^%d ( + counter_%d^%d 1 ) ) ",j,p,j,p-1);
                fprintf( z3throughcommandlinesmt2file, ") ");
              }
              break;
            case 3 :
              if (p==1) {
                fprintf( z3throughcommandlinesmt2file, "false ");
              } else {
                fprintf( z3throughcommandlinesmt2file, "( and ");
                fprintf( z3throughcommandlinesmt2file, "( < arrivespos_%d_%d %d ) ( <= %d Zexpirespos_%d_%d ) ",j,q,p,p,j,q);
                fprintf( z3throughcommandlinesmt2file, "x_%d_%d^%d ",j,q,p-1);
                printfsumexecequalsc(j,q,1,p); fprintf( z3throughcommandlinesmt2file, " ");
                fprintf( z3throughcommandlinesmt2file, "( not ( < counter_%d^%d %d ) ) ",j,p-1,tasks[j].MAXCOUNT);
                fprintf( z3throughcommandlinesmt2file, "( = counter_%d^%d counter_%d^%d ) ",j,p,j,p-1);
                fprintf( z3throughcommandlinesmt2file, " ) ");
              }
              break;
            case 4 :
              if (p==1) {
                fprintf( z3throughcommandlinesmt2file, "false ");
              } else {
                fprintf( z3throughcommandlinesmt2file, "( and ");
                fprintf( z3throughcommandlinesmt2file, "( < Zexpirespos_%d_%d %d ) ( < %d Dexpirespos_%d_%d ) ",j,q,p,p,j,q);
                fprintf( z3throughcommandlinesmt2file, "x_%d_%d^%d ",j,q,p-1);
                printfsumexecstrictlylessthanc(j,q,1,p); fprintf( z3throughcommandlinesmt2file, " ");
                printfsumexecequalse(j,q,1,p);           fprintf( z3throughcommandlinesmt2file, " "); 
                fprintf( z3throughcommandlinesmt2file, "( = counter_%d^%d counter_%d^%d ) ",j,p,j,p-1);
                fprintf( z3throughcommandlinesmt2file, ") ");
              }
              break;
            case 5 :
              if (p==1) {
                fprintf( z3throughcommandlinesmt2file, "false ");
              } else {
                fprintf( z3throughcommandlinesmt2file, "( and  ");
                fprintf( z3throughcommandlinesmt2file, "( = %d Dexpirespos_%d_%d ) ",p,j,q);
                printfsumexecstrictlylessthanc(j,q,1,p); fprintf( z3throughcommandlinesmt2file, " ");
                printfsumexecstrictlylessthane(j,q,1,p); fprintf( z3throughcommandlinesmt2file, " ");
                fprintf( z3throughcommandlinesmt2file, "( = counter_%d^%d ( - counter_%d^%d 1 ) ) ",j,p,j,p-1);
                fprintf( z3throughcommandlinesmt2file, ") ");
              }
              break;
            default :
              printf("This should not happen. We have an unexpeted value of o.\n");
              exit(-1);
          }
          fprintf( z3throughcommandlinesmt2file, " ))\n");
        }
      }
    }
  }
}

void addconstraint_oe_implications_not1to5(int iD) {
  int j; int q; int p;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
        for (p=1;p<=getnpos(iD)+1;p++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( => ");
          fprintf( z3throughcommandlinesmt2file, "( and ( not oe_%d_%d^%d^%d ) ( not oe_%d_%d^%d^%d ) ( not oe_%d_%d^%d^%d ) ( not oe_%d_%d^%d^%d ) ( not oe_%d_%d^%d^%d ) ) ",j,q,p,1,j,q,p,2,j,q,p,3,j,q,p,4,j,q,p,5  );
          fprintf( z3throughcommandlinesmt2file, "( = counter_%d^%d counter_%d^%d ) ",j,p,j,p-1);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
}

void addconstraint_forhptasks_counter_is_nonnegative(int iD) {
  int j; int p;
  for (j=1;j<=ntasks;j++) {
    if (is_in_hp(j,iD)) {
      for (p=1;p<=getnpos(iD)+1;p++) {
        fprintf( z3throughcommandlinesmt2file, "(assert ( >= counter_%d^%d 0 ))\n",j,p);
      }
    }
  }  
}

void addconstraint_iDjobiskilled(int iD) {
  int p; int o;
  for (p=1;p<=getnpos(iD)+1;p++) {
    for (o=1;o<=4;o++) {
      fprintf( z3throughcommandlinesmt2file, "(assert ( ");
      fprintf( z3throughcommandlinesmt2file, " not oe_%d_%d^%d^%d ",iD,1,p,o );     
      fprintf( z3throughcommandlinesmt2file, "))\n");
    }
  } 
  fprintf( z3throughcommandlinesmt2file, "(assert ( ");
  fprintf( z3throughcommandlinesmt2file, " or ");
  for (p=1;p<=getnpos(iD)+1;p++) {
    fprintf( z3throughcommandlinesmt2file, " oe_%d_%d^%d^%d ",iD,1,p,5 );     
  } 
  fprintf( z3throughcommandlinesmt2file, "))\n");
}

void addconstraint_iDjob_hascounter_initially_zero(int iD) {
  fprintf( z3throughcommandlinesmt2file, "(assert ( = counter_%d^0 0 ))\n", iD);
}

void addconstraint_busy_related_to_deadlineofiDjob(int iD) {
  int j; int q; int p;
  int temp;
  for (p=1;p<=getnpos(iD);p++) {
    fprintf( z3throughcommandlinesmt2file, "(assert ( = ");
    fprintf( z3throughcommandlinesmt2file, "( < %d Dexpirespos_%d_%d ) ",p,iD,1);

    temp = 0;
    for (j=1;j<=ntasks;j++) {
      if ((is_in_hp(j,iD)) || (j==iD)) {
        for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
          temp++;
        }
      }
    }

    if (temp==0) { printf("Error in addconstraint_busy_related_to_deadlineofiDjob\n"); exit(-1); }
    if (temp>1)  { fprintf( z3throughcommandlinesmt2file, "( or "); }
    for (j=1;j<=ntasks;j++) {
      if ((is_in_hp(j,iD)) || (j==iD)) {
        for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
          fprintf( z3throughcommandlinesmt2file, "x_%d_%d^%d ",j,q,p);
        }
      }
    }
    if (temp>1)  { fprintf( z3throughcommandlinesmt2file, " ) "); }

    fprintf( z3throughcommandlinesmt2file, " ))\n");
  }
}

void addconstraint_position_strictlylessthan_deadlineofiDjob_implies_busy(int iD) {
  int j; int q; int p;
  int temp;
  for (p=1;p<=getnpos(iD);p++) {
    fprintf( z3throughcommandlinesmt2file, "(assert ( => ");
    fprintf( z3throughcommandlinesmt2file, "( < %d Dexpirespos_%d_%d ) ",p,iD,1);

    temp = 0;
    for (j=1;j<=ntasks;j++) {
      if ((is_in_hp(j,iD)) || (j==iD)) {
        for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
          temp++;
        }
      }
    }

    if (temp==0) { printf("Error in addconstraint_busy_related_to_deadlineofiDjob\n"); exit(-1); }
    if (temp>1)  { fprintf( z3throughcommandlinesmt2file, "( or "); }
    for (j=1;j<=ntasks;j++) {
      if ((is_in_hp(j,iD)) || (j==iD)) {
        for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
          fprintf( z3throughcommandlinesmt2file, "x_%d_%d^%d ",j,q,p);
        }
      }
    }
    if (temp>1)  { fprintf( z3throughcommandlinesmt2file, " ) "); }

    fprintf( z3throughcommandlinesmt2file, " ))\n");
  }
}

void addconstraint_position_greaterthanorequalto_deadlineofiDjob_implies_execcandrexece_are_zero(int iD) {
  int j; int q; int p;
  int temp;
  for (p=1;p<=getnpos(iD);p++) {
    fprintf( z3throughcommandlinesmt2file, "(assert ( => ");
    fprintf( z3throughcommandlinesmt2file, "( not ( < %d Dexpirespos_%d_%d ) ) ",p,iD,1);

    temp = 0;
    for (j=1;j<=ntasks;j++) {
      if ((is_in_hp(j,iD)) || (j==iD)) {
        for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
          temp++;
        }
      }
    }

    if (temp==0) { printf("Error in addconstraint_busy_related_to_deadlineofiDjob\n"); exit(-1); }
    if (temp>1)  { fprintf( z3throughcommandlinesmt2file, "( and "); }
    for (j=1;j<=ntasks;j++) {
      if ((is_in_hp(j,iD)) || (j==iD)) {
        for (q=1;q<=ceil(tasks[iD].D/tasks[j].T);q++) {
          fprintf( z3throughcommandlinesmt2file, " ( and ");
          fprintf( z3throughcommandlinesmt2file, " ( = execc_%d_%d^%d 0 )",j,q,p);
          fprintf( z3throughcommandlinesmt2file, " ( = exece_%d_%d^%d 0 )",j,q,p);
          fprintf( z3throughcommandlinesmt2file, " ) ");
        }
      }
    }
    if (temp>1)  { fprintf( z3throughcommandlinesmt2file, " ) "); }

    fprintf( z3throughcommandlinesmt2file, " ))\n");
  }
}

void addconstraint_counterupperbounded(int iD) {
  int j; int p; int upperbound;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (p=1;p<=getnpos(iD)+1;p++) {
        fprintf( z3throughcommandlinesmt2file, "(assert ( ");
        upperbound = minint2( ceil(tasks[iD].D/tasks[j].T), tasks[j].MAXCOUNT);
        fprintf( z3throughcommandlinesmt2file, " <= counter_%d^%d %d ",j,p,upperbound);
        fprintf( z3throughcommandlinesmt2file, "))\n");
      }
    }
  }  
}

void addconstraint_victimjobarrivesattimezero(int iD) {
  fprintf( z3throughcommandlinesmt2file, "(assert ( ");
  fprintf( z3throughcommandlinesmt2file, " = A_%d_%d %lf ",iD,1, 0.0);
  fprintf( z3throughcommandlinesmt2file, "))\n");
}
void addconstraint_victimjobhasarrivesposequalsone(int iD) {
  fprintf( z3throughcommandlinesmt2file, "(assert ( ");
  fprintf( z3throughcommandlinesmt2file, " = arrivespos_%d_%d %d ",iD,1, 1);
  fprintf( z3throughcommandlinesmt2file, "))\n");
}  
void addconstraint_victimjobhascounterzerobeforedeadline_and_negative_after(int iD) {
  int p;
  for (p=1;p<=getnpos(iD)+1;p++) {
    fprintf( z3throughcommandlinesmt2file, "(assert ( => ");
    fprintf( z3throughcommandlinesmt2file, "( < %d Dexpirespos_%d_%d ) ",p,iD,1);
    fprintf( z3throughcommandlinesmt2file, "( = counter_%d^%d %d ) ",iD,p, 0);
    fprintf( z3throughcommandlinesmt2file, " ))\n");

    fprintf( z3throughcommandlinesmt2file, "(assert ( => ");
    fprintf( z3throughcommandlinesmt2file, "( not ( < %d Dexpirespos_%d_%d ) ) ",p,iD,1);
    fprintf( z3throughcommandlinesmt2file, "( = counter_%d^%d ( - 1 ) ) ",iD,p);
    fprintf( z3throughcommandlinesmt2file, " ))\n");
  }
}  

void addconstraint_atmostoneeventper_position_given_position(int p,int iD) {
  int jprime; int qprime; int jprimeprime; int qprimeprime;
  for (jprime=1;jprime<=ntasks;jprime++) {
    if ((is_in_hp(jprime,iD)) || (jprime==iD)) {
      for (qprime=1;qprime<=ceil(tasks[iD].D/tasks[jprime].T);qprime++) {
        for (jprimeprime=1;jprimeprime<=ntasks;jprimeprime++) {
          if ((is_in_hp(jprimeprime,iD)) || (jprimeprime==iD)) {
            for (qprimeprime=1;qprimeprime<=ceil(tasks[iD].D/tasks[jprimeprime].T);qprimeprime++) {
              if ((jprime!=jprimeprime) || (qprime!=qprimeprime)) {
                fprintf( z3throughcommandlinesmt2file, "(assert ( not ( and ( = arrivespos_%d_%d %d  ) ( = Zexpirespos_%d_%d %d ) ) ))\n",jprime,qprime,p,jprimeprime,qprimeprime,p);
                fprintf( z3throughcommandlinesmt2file, "(assert ( not ( and ( = arrivespos_%d_%d %d  ) ( = Dexpirespos_%d_%d %d ) ) ))\n",jprime,qprime,p,jprimeprime,qprimeprime,p);
                fprintf( z3throughcommandlinesmt2file, "(assert ( not ( and ( = Zexpirespos_%d_%d %d ) ( = Dexpirespos_%d_%d %d ) ) ))\n",jprime,qprime,p,jprimeprime,qprimeprime,p);
              }
            }
          }
        }
      }
    }
  }
}

void addconstraint_atmostoneeventper_position(int iD) {
  int p;
  for (p=1;p<=getnpos(iD)+1;p++) {
    addconstraint_atmostoneeventper_position_given_position(p,iD);
  }
}

void addconstraintseparationbetweenevents(int iD) {
  int j; int q; int le;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + arrivespos_%d_%d %d ) arrivespos_%d_%d ",j,q,3*le,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + arrivespos_%d_%d %d ) Zexpirespos_%d_%d ",j,q,3*le+1,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + arrivespos_%d_%d %d ) op_%d_%d ",j,q,3*le,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + arrivespos_%d_%d %d ) Dexpirespos_%d_%d ",j,q,3*le+2,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }

  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + Zexpirespos_%d_%d %d ) arrivespos_%d_%d ",j,q,3*le-1,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + Zexpirespos_%d_%d %d ) Zexpirespos_%d_%d ",j,q,3*le,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + Zexpirespos_%d_%d %d ) op_%d_%d ",j,q,3*le-1,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + Zexpirespos_%d_%d %d ) Dexpirespos_%d_%d ",j,q,3*le+1,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }

  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + op_%d_%d %d ) arrivespos_%d_%d ",j,q,3*le-2,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + op_%d_%d %d ) Zexpirespos_%d_%d ",j,q,3*le-1,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + op_%d_%d %d ) op_%d_%d ",j,q,3*le-2,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + op_%d_%d %d ) Dexpirespos_%d_%d ",j,q,3*le,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }

  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + Dexpirespos_%d_%d %d ) arrivespos_%d_%d ",j,q,3*le-2,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + Dexpirespos_%d_%d %d ) op_%d_%d ",j,q,3*le-2,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + Dexpirespos_%d_%d %d ) Zexpirespos_%d_%d ",j,q,3*le-1,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        for (le=1;le<=ceil(tasks[iD].D/tasks[j].T)-q;le++) {
          fprintf( z3throughcommandlinesmt2file, "(assert ( ");
          fprintf( z3throughcommandlinesmt2file, " <= ( + Dexpirespos_%d_%d %d ) Dexpirespos_%d_%d ",j,q,3*le,j,q+le);
          fprintf( z3throughcommandlinesmt2file, "))\n");
        }
      }
    }
  }

  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        fprintf( z3throughcommandlinesmt2file, "(assert ( ");
        fprintf( z3throughcommandlinesmt2file, " < arrivespos_%d_%d Zexpirespos_%d_%d ",j,q,j,q);
        fprintf( z3throughcommandlinesmt2file, "))\n");
        fprintf( z3throughcommandlinesmt2file, "(assert ( ");
        fprintf( z3throughcommandlinesmt2file, " <= arrivespos_%d_%d op_%d_%d ",j,q,j,q);
        fprintf( z3throughcommandlinesmt2file, "))\n");
        fprintf( z3throughcommandlinesmt2file, "(assert ( ");
        fprintf( z3throughcommandlinesmt2file, " < ( + arrivespos_%d_%d 1 ) Dexpirespos_%d_%d ",j,q,j,q);
        fprintf( z3throughcommandlinesmt2file, "))\n");
        fprintf( z3throughcommandlinesmt2file, "(assert ( ");
        fprintf( z3throughcommandlinesmt2file, " < Zexpirespos_%d_%d Dexpirespos_%d_%d ",j,q,j,q);
        fprintf( z3throughcommandlinesmt2file, "))\n");

        fprintf( z3throughcommandlinesmt2file, "(assert ( ");
        fprintf( z3throughcommandlinesmt2file, " <= op_%d_%d          Dexpirespos_%d_%d ",j,q,j,q);
        fprintf( z3throughcommandlinesmt2file, "))\n");

      }
    }
  }

}

void addconstraintjobarrivingaftervictimjobhaszeroexecution(int iD) {
  int j; int q;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      for (q=1;q<=ceil(tasks[iD].D/tasks[j].T)-1;q++) {
        fprintf( z3throughcommandlinesmt2file, "(assert ( => ");
        fprintf( z3throughcommandlinesmt2file, " ( >= arrivespos_%d_%d Dexpirespos_%d_%d ) ",j,q,iD,1);
        fprintf( z3throughcommandlinesmt2file, " (  = c_%d_%d          0                 ) ",j,q);
        fprintf( z3throughcommandlinesmt2file, "))\n");
        fprintf( z3throughcommandlinesmt2file, "(assert ( => ");
        fprintf( z3throughcommandlinesmt2file, " ( >= arrivespos_%d_%d Dexpirespos_%d_%d ) ",j,q,iD,1);
        fprintf( z3throughcommandlinesmt2file, " (  = e_%d_%d          0                 ) ",j,q);
        fprintf( z3throughcommandlinesmt2file, "))\n");
      }
    }
  }
}

double getmaxt(int iD) {
  int j; int q; double max_seen_sofar; double temp;
  max_seen_sofar = 0.0;
  for (j=1;j<=ntasks;j++) {
    if ((is_in_hp(j,iD)) || (j==iD)) {
      temp = tasks[iD].D + ceil(tasks[iD].D/tasks[j].T) * tasks[j].T;
      if (max_seen_sofar<temp) {
        max_seen_sofar = temp;
      } 
    }
  }
  return max_seen_sofar;
}

void addconstraint_t_is_atmost(int iD) {
  int p;
  for (p=1;p<=getnpos(iD);p++) {
    fprintf( z3throughcommandlinesmt2file, "(assert ( ");
    fprintf( z3throughcommandlinesmt2file, " <= t^%d %lf ", p, getmaxt(iD));
    fprintf( z3throughcommandlinesmt2file, "))\n");
  }
}

void is_cprsmtinstance_satisfiable_make_all_assertions(int iD) {
  addconstraintposorder(iD);
  addconstraintfirstposisattimezero();
  addconstraintcounterinpositionzero_is_nonnegative(iD);
  addconstraintpositionsareinrange(iD);
  addconstrainteventsimplytimes(iD);
  addconstraint_Dexpiresprecedesnextarrival(iD);
  addconstraintcande(iD);
  addconstraintminimumarrivaltime(iD);
  addconstraintatleastonerespectC(iD);
  addconstraintdispatching(iD);
  addconstraintxandexeccexece(iD);
  addconstraint_range_o_and_range_of_op(iD);  
  addconstraint_oe_implications(iD,1);
  addconstraint_oe_implications(iD,2);
  addconstraint_oe_implications(iD,3);
  addconstraint_oe_implications(iD,4);
  addconstraint_oe_implications(iD,5);
  addconstraint_oe_implications_not1to5(iD);
  addconstraint_forhptasks_counter_is_nonnegative(iD);
  addconstraint_iDjobiskilled(iD);
  addconstraint_iDjob_hascounter_initially_zero(iD);
  addconstraint_position_strictlylessthan_deadlineofiDjob_implies_busy(iD);
  addconstraint_position_greaterthanorequalto_deadlineofiDjob_implies_execcandrexece_are_zero(iD);
  addconstraint_counterupperbounded(iD);
  addconstraint_victimjobarrivesattimezero(iD);
  addconstraint_victimjobhasarrivesposequalsone(iD);  
  addconstraint_victimjobhascounterzerobeforedeadline_and_negative_after(iD);  
}

void setuserexecutablemode(char* fn) {
  char s[2000];
  sprintf(s,"chmod u+x %s", fn);
  system(s);
}

int is_the_result_satisfiable() {
  FILE* f; char s[200];
  f = fopen( z3throughcommandline_result_filename, "rt");
  if (f==NULL) {
    printf("In is_the_result_satisfiable. error when opening file. fn=%s\n", z3throughcommandline_result_filename); fflush(stdout);
    exit(0);
  }
  fgets( s, 200, f);
  fclose(f); 
  if (strncmp(s,"sat",3)==0) {
    return 1;
  } else {
    return 0;
  }
}

void create_plot_from_failure_doit_with_latex(int iD) {
  char failuretexfn[200];
  char failuredvifn[200];
  char failurepsfn[200];
  char failurepdffn[200];
  char commandstr[200];

  fill_in_variableandvaluestruct();
  fill_in_mint_and_maxt();

  sprintf(failuretexfn,"failure_%d.tex", counterforSMTsolver);
  sprintf(failuredvifn,"failure_%d.dvi", counterforSMTsolver);
  sprintf(failurepsfn, "failure_%d.ps",  counterforSMTsolver);
  sprintf(failurepdffn,"failure_%d.pdf", counterforSMTsolver);

  create_latex_file_with_visualization_of_failure(failuretexfn,iD);
  sprintf(commandstr,"latex %s", failuretexfn);                    system(commandstr);
  sprintf(commandstr,"dvips -o %s %s", failurepsfn, failuredvifn); system(commandstr);
  sprintf(commandstr,"ps2pdf %s %s", failurepsfn, failurepdffn);   system(commandstr);
}

void create_plot_from_failure_doit_with_svg(int iD) {
  FILE* fout; char failuresvgfn[200];

  fill_in_variableandvaluestruct();
  fill_in_mint_and_maxt();

  sprintf(failuresvgfn,"%s",plotfilename);

  create_svg_file_with_visualization_of_failure(failuresvgfn,iD);
}

void create_plot_from_failure(int iD) {
  if (enable_generate_latexpdf) {
    create_plot_from_failure_doit_with_latex(iD);
  }
  if (enable_generate_svg) {
    create_plot_from_failure_doit_with_svg(iD);
  }
}

int is_cprsmtinstance_satisfiable(int iD) {
  counterforSMTsolver = counterforSMTsolver + 1;
  sprintf( z3throughcommandlinesmt2filename, "z3throughcommandlinesmt2filename_%d.smt2", counterforSMTsolver);
  sprintf( commandstringwithscriptfilename,  "./commandstringwithscript_%d.cmd", counterforSMTsolver);
  sprintf( z3throughcommandline_result_filename, "z3throughcommandlinesmt2_result_filename_%d.txt", counterforSMTsolver);
  z3throughcommandlinesmt2file = fopen( z3throughcommandlinesmt2filename, "w");
  if (z3throughcommandlinesmt2file==NULL) {
    printf("In schedulable_bounded_time. error when opening file. fn=%s\n", z3throughcommandlinesmt2filename); fflush(stdout);
    exit(0);
  }
  commandstringwithscriptfile = fopen( commandstringwithscriptfilename, "w");
  if (commandstringwithscriptfile==NULL) {
    printf("In schedulable_bounded_time. error when opening file. fn=%s\n", commandstringwithscriptfilename); fflush(stdout);
    exit(0);
  }
  if (useanalysismethod!=1) {
    printf("In schedulable_bounded_time. error. bad method. fn=%s\n", z3throughcommandlinesmt2filename); fflush(stdout);
    exit(0);
  }
  add_line_verbose100();
  add_line_logic_QF_LIRA();
  is_cprsmtinstance_satisfiable_declare_all_variables(iD);
  is_cprsmtinstance_satisfiable_make_all_assertions(iD);
  add_line_checksat();
  add_line_getmodel();
  createcommandstring_for_is_cprsmtinstance_satisfiable();
  fclose( z3throughcommandlinesmt2file);
  fclose( commandstringwithscriptfile);
  setuserexecutablemode(commandstringwithscriptfilename);
  system(commandstringwithscriptfilename);
  if (is_the_result_satisfiable()) {
    if (enableplot) { create_plot_from_failure(iD); }
    return 1;
  } else {
    return 0;
  }
}

int perform_schedulability_analysis() {
  int flag; int iD;
  flag = 1;
  iD = 1;
  while ((iD<=ntasks) && (flag)) {
    if (is_cprsmtinstance_satisfiable(iD)) {
      flag = 0;
    }
    iD++;
  }
  return flag;
}

double getutil() {
  int j; double sum;
  sum = 0.0;
  for (j=1;j<=ntasks;j++) {
    sum = sum + tasks[j].C/tasks[j].T;
  }
  return sum;
}

void adjustCE_to_each_targetutil( double targetutil) {
  double scalefactor; int j;
  scalefactor = targetutil/getutil();
  for (j=1;j<=ntasks;j++) {
    tasks[j].C = tasks[j].C * scalefactor;
    tasks[j].E = tasks[j].E * scalefactor;
  }
}

void sort_tasks_so_that_smallest_has_lowest_index() {
  int j; int jprime;
  struct task temp;
  for (j=1;j<=ntasks;j++) {
    for (jprime=j+1;jprime<=ntasks;jprime++) {
      if (tasks[j].D>tasks[jprime].D) {
        temp = tasks[j];
        tasks[j] = tasks[jprime];
        tasks[jprime] = temp;
      }
    }
  }
}

double log2(double t) { return (log(t))/(log(2.0)); }

void generate_taskset_randomly(int nt,int TUTILINDEX,int TMAXEXP) {
  int j; double CTOT;
  useanalysismethod = 1;
  ntasks = nt;
  for (j=1;j<=ntasks;j++) {
    tasks[j].T = mypow( 2.0, my_double_random(0.0,log2(TMAXEXP)));  
    tasks[j].D = 0.8*tasks[j].T;
    tasks[j].Z = 0.8*tasks[j].D;
    tasks[j].C = 0.9*tasks[j].Z;
    tasks[j].E = 0.1*tasks[j].Z;
    tasks[j].RC = 1;
    tasks[j].MAXCOUNT = 1;
  }
  adjustCE_to_each_targetutil( TUTILINDEX/5.0);
  sort_tasks_so_that_smallest_has_lowest_index();
  for (j=1;j<=ntasks;j++) {
    tasks[j].id = j;
    tasks[j].prio = ntasks+1-j;
  }
}

void get_file_name_for_taskset(int nt,int TUTILINDEX,int TMAXEXP,char* fn_for_taskset) {
  sprintf(fn_for_taskset,"taskset_%d_%d_%d.txt", nt,TUTILINDEX,TMAXEXP);
}

void do_metathing() {
  struct timespec mybegin;
  struct timespec myend;
  int status_clock_gettime_begin;
  int status_clock_gettime_end;
  int nt; int TUTILINDEX; int TMAXEXP; int DTRATIOINDEX;
  int flag; double timerequired;
  char fn_for_taskset[2000];
  FILE* myfile;
  myfile = fopen("overallstatistics.txt","w");
  for (nt=2;nt<=5;nt++) {
    for (TUTILINDEX=1;TUTILINDEX<=10;TUTILINDEX++) {
      for (TMAXEXP=1;TMAXEXP<=128;TMAXEXP*=2) {
        generate_taskset_randomly(nt,TUTILINDEX,TMAXEXP);

        get_file_name_for_taskset(nt,TUTILINDEX,TMAXEXP,fn_for_taskset);
        writetasksettofile(fn_for_taskset);
        status_clock_gettime_begin = clock_gettime(CLOCK_MONOTONIC_RAW, &mybegin);

        flag = perform_schedulability_analysis();
        status_clock_gettime_end = clock_gettime(CLOCK_MONOTONIC_RAW, &myend);
        timerequired = diff_s_timespec(&myend,&mybegin);

        fprintf(myfile,"%d %d %d  %d %lf\n", nt,TUTILINDEX,TMAXEXP,   flag, timerequired ); fflush(myfile);
      }      
    }    
  }
  fclose( myfile);
}

int main( int argc, char *argv[], char *envp[]) {
  int flag;
  initialize_random_generator();
  parsearguments(argc, argv, envp);
  if (metathing) {
    do_metathing();
    exit(0);
  }

  readtasksetfromfile( inputfilename );
  flag = perform_schedulability_analysis();
  if (flag) {
    printf("Taskset is schedulable.\n");
    return 1;
  } else {
    printf("Taskset is unschedulable.\n");
    return 0;
  }
}