<?php

// Versão GCLCprover - Gröbner Bases Method

// Vai criar o ficheiro pdf com a demonstração para guardar na base de
// dados.  

// Os nomes dos ficheiros tem apenso o identificador de utilizador
// para desta forma permitir a escrita de ficheiros por mais do que um
// utilizador ao mesmo tempo.


$vNameProofCode = 'proof'.$pUserId.'.code';
$vNameProofCodeXML = 'proofCode'.$pUserId.'.xml';  // contêm o código do ATP formato XML
$vNameProofProof = 'proof'.$pUserId.'_proof.tex';
$vNameProofErr = 'proof'.$pUserId.'.err';
$vNameProofErrors = 'proof'.$pUserId.'.errors';
$vNameProofLog = 'proof'.$pUserId.'.gclclog';
$vNameProofPIC = 'proof'.$pUserId.'.pic';
$vNameProofTeX = 'proof'.$pUserId.'.tex';
$vNameProofDVI = 'proof'.$pUserId.'.dvi';
$vNameProofPS = 'proof'.$pUserId.'.ps';
$vNameProofPDF = 'proof'.$pUserId.'.pdf';
$vNameProofProofXML = 'proof'.$pUserId.'_proof.xml';
$vNameProofXML = 'proof'.$pUserId.'.xml';  // contêm a demonstração em formato XML
$vNameProofBZ2 = $vNameProofXML.'.bz2';

$vNameProofAux = 'proof'.$pUserId.'_aux.txt';
$vNameProofCodeConv = 'proof'.$pUserId.'.codeconv';
$vNameErrorsConv = 'proof'.$pUserId.'.errorsconv';

$commandLineATP = "gclc $vNameProofCode $vNameProofPIC -g > $vNameProofErrors";
$timeLimit = "0"; // 0 significa que não foi estabelecido o limite do tempo de execução


// Escreve o ficheiro ".code" referente ao código
ob_start();
print $auxCode."\n";
$prooffile=fopen($vNameProofCode,"w");
fwrite($prooffile,ob_get_contents()); 
fclose($prooffile); 
ob_end_clean(); 

// Vai processar o código com o programa de prova
ob_start();
// aplica o  provador GCLCprover Area Method
system($commandLineATP);
// salvaguarda o ficheiro gclc.log em <nome>.gclclog
system("cp gclc.log $vNameProofLog");
// verifica se há erros de sintaxe
system("grep Syntax $vNameProofErrors > $vNameProofErr");
// ou se há erros na conjectura (ou construções não suportadas)
system("grep ill-formed $vNameProofErrors >> $vNameProofErr");
ob_end_clean(); 

$filename = $vNameProofErr;

// Vai verificar se houve erros ou não
if  (file_exists($filename) and filesize($filename)>0) { // há erros 
  $file = fopen ($filename, "r");
  $contents = fread ($file, filesize ($filename));
  echo $contents;
  //system("rm proof.err");
  echo "<center>\n";
  echo "<br>There are errors in the proof's code. ";
  echo "The proof was not inserted in the database</b>\n";
  echo "</center>\n";
  // TRANSAÇÕES - ROLLBACK
  @ mysql_query("ROLLBACK"); 
  echo "<meta http-equiv=\"refresh\" content=\"2; url=../Geothms/updateGeoThm.php?argumento=$pTeoId\" />";
 }
 else { 
   // Caso não haja erros vai processar a prova
   // Vai produzir o texto LaTeX referente à Prova
   // Pré-processa o ficheiro proof_proof.tex gerado pelo gclc 
   // pelo sed para substituir o estilo por omissão do gclc pelo estilo
   // landscape
   ob_start();
   system("sed -e 's/{gclc_proof}/\[landscape\]{gclcproof}/g' $vNameProofProof > $vNameProofTeX");  
   echo "<p>Processing the PDF file, please wait</p>\n";
   system("latex $vNameProofTeX"); 
   system("latex $vNameProofTeX"); 
   system("dvipdf $vNameProofDVI"); 
   
   ob_end_clean(); 
   
   /*
     Vai agora criar os ficheiros XML referente ao código e à prova

     Formato "XML" -  gclc proof.code proof.xml -xml
     proof.xml -  codigo em formato "XML"
     proof_proof.xml - demonstração em formato "XML"

   */

   echo "<p>Processing the XML file, please wait</p>\n";
   system("gclc  $vNameProofCode $vNameProofCodeXML -g -xml > $vNameProofErrors");
   
   // modifica o estilo de saída (código) para "Natural Language"
   // É o conteúdo do ficheiro modificado que é inserido na BD
   system("sed -e 's/GeoConsHTML.xsl/GeoConsNL.xsl/g' $vNameProofCodeXML > $vNameProofAux");

   // e agora  inserção do ficheiro referente à demonstração
   system("cp $vNameProofProofXML $vNameProofXML");
   // vai conprimir o ficheiro com o bzip2, é necessário apagar o
   // ficheiro comprimido, caso exista.
   system("rm $vNameProofBZ2");
   system("bzip2 $vNameProofXML");
   
   // Agora a inserção do código em formato XML
   $fpCodeXML      = fopen($vNameProofAux, 'r');
   $contentCodeXML = fread($fpCodeXML, filesize($vNameProofAux));
   $contentCodeXML = addslashes($contentCodeXML);
   fclose($fpCodeXML);
  
   // e agora a inserção da prova em formato PDF
   $fpPDF      = fopen($vNameProofPDF, 'r');
   $contentPDF = fread($fpPDF, filesize($vNameProofPDF));
   $contentPDF = addslashes($contentPDF);
   fclose($fpPDF);
   
   // Agora a inserção da prova em formato XML comprimido
   $fpBZ2      = fopen($vNameProofBZ2, 'r');
   $contentBZ2 = fread($fpBZ2, filesize($vNameProofBZ2));
   $contentBZ2 = addslashes($contentBZ2);
   fclose($fpBZ2);

   // Agora a inserção da LogFile
   $fpLF      = fopen($vNameProofLog, 'r');
   $contentLF = fread($fpLF, filesize($vNameProofLog));
   $contentLF = addslashes($contentLF);
   fclose($fpLF);


   $sqlproof = "UPDATE demonstrations
                   SET commandLine = '$commandLineATP',
                       timeLimit = $timeLimit,
                       proof    = '$contentPDF',
                       proofXML = '$contentBZ2',
                       logfile = '$contentLF'
                 WHERE demId = $auxDemId";

   $resultadoproof = mysql_query($sqlproof,$ligacao);
   
   //   echo $sqlproof."<br />";

   if (!$resultadoproof) {
     echo "Error - proof not inserted (GCLC L122)";
     // TRANSAÇÕES - ROLLBACK
     @ mysql_query("ROLLBACK"); 
     echo "<meta http-equiv=\"refresh\" content=\"2; url=../Geothms/updateGeoThm.php?argumento=$pTeoId\" />";
     exit;
   }
   
   
   // Fim - inserção da prova
   
   // Preenchimento do campo "status"
   
   // vai obter o resultado da tentativa de prova
     ob_start();
    $vResult=system("provedDisproved < $vNameProofLog");
    ob_end_clean();
    /*
     1 = The conjecture successfully proved.
     2 = The conjecture disproved.
     3 = The conjecture not proved.
     4 - The conjecture not proved - timeout.
     5 - The conjecture not proved - maximal number of proof steps reached.
     6 - The conjecture not proved - out of the scope
    */
    if ($vResult==1) 
      $vStatus="Proved";
    elseif ($vResult==2)
      $vStatus="Disproved";
    elseif ($vResult==3)
      $vStatus="Failed to prove the conjecture";
    elseif ($vResult==4)
      $vStatus="Time-out: Failed to prove the conjecture";
    elseif ($vResult==5)
      $vStatus="Maximal number of proof steps reached: Failed to prove the conjecture";
    elseif ($vResult==6)
      $vStatus="The conjecture out of scope of the prover";
    else {// Vai-se assumir que em todos os outros casos (ainda por tratar!?) houve falha.
      $vResult=3;
      $vStatus="Failed to prove the conjecture";
    }
   
   $sqlProofStatus = "UPDATE demonstrations
                         SET status = '$vStatus',
                             statusN = $vResult
                       WHERE demId = $auxDemId";
   
   $resultadoProofStatus = mysql_query($sqlProofStatus,$ligacao);
   
   if (!$resultadoProofStatus) {
     echo "Error - proof not inserted (L155)";
     // TRANSAÇÕES - ROLLBACK
     @ mysql_query("ROLLBACK"); 
     echo "<meta http-equiv=\"refresh\" content=\"2; url=../Geothms/updateGeoThm.php?argumento=$pTeoId\" />";
     exit;
   }
   
   // E agora os resultados das medidas de eficiência
   
   ob_start();
   $elimSteps=0; // no método de Wu não tem significado
   $geoSteps=0; // no método de Wu não tem significado
   $algSteps=0; // no método de Wu não tem significado
   $totalSteps=0; // no método de Wu não tem significado
   $nLargestPolynomial = system("nLargestPolynomial < $vNameProofTeX");
   $sTime=system("sTime < $vNameProofTeX");
   ob_end_clean();
   
    // Vai obter a identificação do Computador de serviço 
   // isto é o computador aonde os programas estão a ser executados.
   
   require_once("../servidor.php");

   $pComputerId = $servidorCPU; // valor fixado no ficheiro servidor.php

   $sqlProofMeasures = "UPDATE measures
                           SET elimSteps     = $elimSteps,
                               geoSteps      = $geoSteps,
                               algSteps      = $algSteps,
                               timeCPU       = $sTime,
                               numberTerms   = $nLargestPolynomial,
                               computerId    = $pComputerId
                         WHERE measuresId = $auxDemId";
   
   $resultadoProofMeasures = mysql_query($sqlProofMeasures,$ligacao);


   //   echo $sqlProofMeasures;

   if (!$resultadoProofMeasures) {
     echo "Error - proof not updated - Measures (L201)";
     // TRANSAÇÕES - ROLLBACK
     @ mysql_query("ROLLBACK"); 
     echo "<meta http-equiv='refresh' content='0; url=../Geothms/updateGeoThm.php?argumento=$pTeoId' />";
     exit;
   }
 } // fim da actualização da prova + status + medidas de eficiência

// Está tudo bem - Termina a transação.
@mysql_query("COMMIT");

?>