<?php

require("login.php");

// Início da transacção - para já para poder simular tudo sem
// consequência na base de dados (não faço o commit

//@ mysql_query("BEGIN");



// Alterações

// o userId é um número e não um nome (isso é o username), o userId do
// gpreda1 é o 70 (no hilbert e no gentzen)

// As bibrefs estão em tabelas separadas "bibfigure", "bibtheorem", e
// "bibproofs". No caso de não haver uma referência bibliográfica não há
// razão para fazer a inserção, só no caso em que há é que isso é feito.


/*
 Processamento dos diferentes "objectos"

 Figuras

  Formato "PIC" - gclc figure0073.code figure0073.pic 

  Formato "SVG" - gclc figure0073.code figure0073.svg -svg

  Formato "XML" - gclc figure0073.code figure0073.xml -xml 

 Demonstrações - Pode não ser possível

  Area Method

  Formato "LaTeX" - gclc proof0073.code proof0073.pic -a
    proof0073.pic - figura em formato "PIC"
    proof0074_proof.tex - demonstração em formato "LaTeX"

  Formato "XML" -  gclc proof0073.code proof0073.svg -svg
    proof0073.svg - figura em formato "SVG"
    proof0074_proof.xml - demonstração em formato "XML"

  Medidas de Performance

    gclc.log

  Wu's Method

    gclc proof0073.code proof0073.pic -w
    gclc proof0073.code proof0073.svg -w -svg
    

  Gröbner basis Method

    gclc proof0073.code proof0073.pic -g
    gclc proof0073.code proof0073.svg -g -svg

    


*/

//Initialize the XML parser
$parser=xml_parser_create();

//Function to use at the start of an element
function start($parser,$element_name,$element_attrs) {

  global $i,$elementos;

  switch($element_name) {
//   case "RESULTS":
//     echo "-- Lista de Teoremas --<br />";
//     break; 
//   case "RESULT":
//     echo "Teorema<br/>";
//     break; 
  case "USERID":
    $elementos[$i] = "";
    break; 
  case "THEONAME":
    $elementos[$i] = "";
    break; 
  case "DESCRIPTION":
    $elementos[$i] = "\begin{geothm}";
    break; 
  case "SHORTDESCRIPTION":
    $elementos[$i] = "";
    break; 
  case "OBSERVATIONS":
    $elementos[$i] = "";
    break; 
  case "FIGCODE":
    $elementos[$i] = "";
    break; 
  case "PROOFSCODE":
    $elementos[$i] = "";
    break; 
  case "BIBTEXENTRY":
    $elementos[$i] = "";
    break; 
  }
}

//Function to use at the end of an element
function stop($parser,$element_name) {

  global $i,$elementos;

  switch($element_name)    {
//   case "RESULT":
//     echo "<br/> - - - - - - - - <br/></br>";
//    break; 
  case "USERID":
    $elementos[$i] .= "\n";
    $i++;
    break; 
  case "THEONAME":
    $elementos[$i] .= "\n";
    $i++;
    break; 
  case "DESCRIPTION":
    $elementos[$i].="\end{geothm}";
    $i++;
    break; 
  case "SHORTDESCRIPTION":
    $elementos[$i] .= "\n";
    $i++;
    break; 
  case "OBSERVATIONS":
    $elementos[$i] .= "\n";
    $i++;
    break; 
  case "FIGCODE":
    $elementos[$i] .= "\n";
    $i++;
    break; 
  case "PROOFSCODE":
    $elementos[$i] .= "\n";
    $i++;
    break; 
  case "BIBTEXENTRY":
    $elementos[$i] .= "";
    $i++;
    break; 
  }
}

//Function to use when finding character data
function char($parser,$data)  {
  global $elementos,$i;

  //  echo $data;
  $elementos[$i] .= $data;
}

//Specify element handler
xml_set_element_handler($parser,"start","stop");

//Specify data handler
xml_set_character_data_handler($parser,"char");

//Open XML file
$fpElementos=fopen("geothms0301.xml","r");

//Read data
$i=0;
while ($data=fread($fpElementos,4096))  {
  xml_parse($parser,$data,feof($fpElementos)) or 
     die (sprintf("XML Error: %s at line %d", 
		  xml_error_string(xml_get_error_code($parser)),
		  xml_get_current_line_number($parser)));
 }

// tratamento dos dados

require('formata_num.inc');

echo "Elementos";

// Abre o Ficheiro aonde vão ser guardados todos os comandos MySQL
$fpMySQL=fopen("comandosMySQL.sql","w");


/*
 Vai obter o número de teorema como sendo o último + 1
*/ 
$sqlMaxTeo = "SELECT max(teoId) 
                FROM theorems
            ORDER BY teoId";
 
$resultadoMaxTeo = mysql_query($sqlMaxTeo,$ligacao);
 
$linhaMaxTeo = mysql_fetch_assoc($resultadoMaxTeo);
$maxTeoId=trim($linhaMaxTeo['max(teoId)']);
 
// retirar a componente númerica do identificador
preg_match("§GEO([0-9]+)§",$maxTeoId,$matches);
 
// O números máximo para o identificador de "theorems"
$maxTeoId = $matches[1];

$aux=0;
// para já é Um
$nteo=$maxTeoId+1;

$today = date("Y/m/d"); 
  
while ($aux<800) { // deve ser 800

  echo "<h1>$nteo</h1>";
  fwrite($fpMySQL,"--- $nteo ---\n\n"); 

//   print("Observações: ".$elementos[$aux+4]."\n\n");
//   print("Código GCLC: ".$elementos[$aux+5]."\n\n");
//   print("Código GCLCprover: ".$elementos[$aux+6]."\n\n");

  // coloca-o no formato apropriado
  $nteo=leading_zero($nteo,4);
  $pTeoId             = 'GEO'.$nteo;
  $pTeoName           = addslashes($elementos[$aux+1]);
  $pBibRef            = addslashes($elementos[$aux+7]);
  $pCategory          = 'Geometry';
  $pDateSubmission    = $today;
  $pDescription       = addslashes($elementos[$aux+2]);
  $pShortDescription  = addslashes($elementos[$aux+3]);
  $pUserId            = addslashes($elementos[$aux]);

  /*
   Faz a inserção da informação referente ao teorema
  */
   
  $sqlInsertGeoTheorem = 
    "INSERT INTO theorems
       (teoId,userId,category,description,shortDescription,teoName,dateSubmission)
      VALUES 
       ('$pTeoId','$pUserId','$pCategory','$pDescription','$pShortDescription',
        '$pTeoName','$pDateSubmission')";


  
  $resultadoInsertGeoTheorem = mysql_query($sqlInsertGeoTheorem,$ligacao);
  
  if (!$resultadoInsertGeoTheorem) {
    echo 'Error - InsertGeoTheorem!';
    // TRANSAÇÕES - ROLLBACK
    //    @ mysql_query("ROLLBACK");
    //echo "<meta http-equiv=\"refresh\" content=\"2; url=updateGeoThm.php?argumento=$pTeoId\" />";
    exit;
  }
  else {
    echo "<p>sqlInsertGeoTheorem - $pTeoName/$pTeoId</p>";
    fwrite($fpMySQL,$sqlInsertGeoTheorem."\n\n"); 
  }


  // a inserção de referências bibliográficas só faz sentido se houver
  // algo para inserir

  if ($pBibRef!="") {
    $sqlInsertTheoremBibRef = 
      "INSERT INTO bibtheorem
       (teoId,bibrefId)
      VALUES 
       ('$pTeoId','$pBibRef')";


    $resultadoInsertTheoremBibRef = mysql_query($sqlInsertTheoremBibRef,$ligacao);
  
    if (!$resultadoInsertTheoremBibRef) {
      echo 'Error - InsertTheoremBibRef!';
      // TRANSAÇÕES - ROLLBACK
      //      @ mysql_query("ROLLBACK");
      //echo "<meta http-equiv=\"refresh\" content=\"2; url=updateGeoThm.php?argumento=$pTeoId\" />";
      exit;
    }
    else {
      echo "<p>sqlInsertTheoremBibRef - $pTeoId</p>";
      fwrite($fpMySQL,$sqlInsertTheoremBibRef."\n\n"); 
    }
  }
    
  /*
   Faz a inserção da informação referente à figura
  */


  // Formata os valores para posterior inserção na Tabela
  // GCLC = 3
  
  $pDrawerId        = 3;
  $pBibrefDrw       = $pBibRef;
  $pCodeDrw         = addslashes($elementos[$aux+5]);

  $sqlInsertFigure = 
    "INSERT INTO figures
       (teoId,drawerId,code,dateSubmission,userId)
      VALUES 
       ('$pTeoId','$pDrawerId','$pCodeDrw','$pDateSubmission','$pUserId')";



  $resultadoInsertFigure = mysql_query($sqlInsertFigure,$ligacao);
  
  if (!$resultadoInsertFigure) {
    echo 'Error - InsertFigure!';
    // TRANSAÇÕES - ROLLBACK
    //    @ mysql_query("ROLLBACK");
    //echo "<meta http-equiv=\"refresh\" content=\"2; url=updateGeoThm.php?argumento=$pTeoId\" />";
    exit;
  }
  else {
    echo "<p>sqlInsertFigure - $pTeoId</p>";
    fwrite($fpMySQL,$sqlInsertFigure."\n\n"); 
  }
  

  // É necessário obter a identificação da figura que se acabou de
  // inserir.  
  
  $pFigureIdLast = mysql_insert_id();

  //  $sqlLastInsertIdFig = "SELECT LAST_INSERT_ID()";
  //  $resultadoLastInsertIdFig = mysql_query($sqlLastInsertIdFig,$ligacao);
  //  $linhaLastInsertIdFig = mysql_fetch_assoc($resultadoLastInsertIdFig);
  //  $pFigureIdLast = $linhaLastInsertIdFig['LAST_INSERT_ID()'];


  // a inserção de referências bibliográficas só faz sentido se houver
  // algo para inserir

  if ($pBibRefDrw!="") {

    $sqlInsertFigureBibRef = 
      "INSERT INTO bibfigure
       (figureId,bibrefId)
      VALUES 
       ('$pFigureIdLast','$pBibRefDrw')";

    $resultadoInsertFigureBibRef = mysql_query($sqlInsertFigureBibRef,$ligacao);
    
    if (!$resultadoInsertFigureBibRef) {
      echo 'Error - InsertFigureBibRef!';
      // TRANSAÇÕES - ROLLBACK
      //      @ mysql_query("ROLLBACK");
      //echo "<meta http-equiv=\"refresh\" content=\"2; url=updateGeoThm.php?argumento=$pTeoId\" />";
      exit;
    }
    else {
      echo "<p>sqlInsertFigureBibRef - $pFigureIdLast</p>";
      fwrite($fpMySQL,$sqlInsertFigureBibRef."\n\n"); 
    }
  }
    
  // e agora as componentes jpg,svg,xml

  $vNameCode = 'figure'.$nteo.'.code';
  $vNameErr = 'figure'.$nteo.'.err';
  $vNameErrors = 'figure'.$nteo.'.errors';
  $vNamePIC = 'figure'.$nteo.'.pic';
  $vNameTeX = 'figure'.$nteo.'.tex';
  $vNameDVI = 'figure'.$nteo.'.dvi';
  $vNamePS = 'figure'.$nteo.'.ps';
  $vNameEPSI = 'figure'.$nteo.'.epsi';
  $vNameJPG = 'figure'.$nteo.'.jpg';


  ob_start();
  print $elementos[$aux+5]."\n";
  $texfile=fopen($vNameCode,"w");
  fwrite($texfile,ob_get_contents()); 
  fclose($texfile); 
  ob_end_clean(); 

  //print("gclc7 $vNameCode $vNamePIC > $vNameErrors");

  ob_start();

  system("gclc $vNameCode $vNamePIC > $vNameErrors");
  system("grep Syntax $vNameErrors > $vNameErr");
  
  ob_end_clean(); 
  
  $filename = $vNameErr;
  
  // 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 figure.err");
    echo "<center>\n";
    echo "<br>There are errors in the figure's code.</b>\n";
    echo "</center>\n";
  }
  else { // Caso não haja erros vai processar a figura

    /* 
     Vai produzir o texto LaTeX referente à Figura, produzindo
     depois a versão JPEG
    */
    ob_start(); 
    print "\documentclass[11pt]{article}\n"; 
    print "\usepackage{gclc}\n"; 
    print "\pagestyle{empty}\n"; 
    print "\begin{document}\n"; 
    print "\input{ $vNamePIC }\n"; 
    print "\end{document}\n"; 
    
    $texfile=fopen($vNameTeX,"w");
    fwrite($texfile,ob_get_contents()); 
    fclose($texfile); 
    
    system("latex $vNameTeX"); 
    system("dvips -E $vNameDVI -o $vNamePS"); 
    system("ps2epsi $vNamePS $vNameEPSI");
    system("convert $vNameEPSI $vNameJPG");
    ob_end_clean(); 
    
    // Agora vai produzir os ficheiros XML e SVG  - para já só para o GCLC
    
    // -----------
    $vNameXML = 'figure'.$nteo.'.xml'; 
    $vNameXMLaux = 'figure'.$nteo.'.auxxml'; 
    // -----------

    // -----------
    $vNameXML = "figureEmpty.xml";
    // -----------

    // -----------
    $vNameSVGaux = 'figure'.$nteo.'.auxsvg';
    $vNameSVG = 'figure'.$nteo.'.svg';
    // -----------
    
    ob_start();   
    // primeiro cria o XML correspondente ao GCLC
    // -----------
    system("gclc $vNameCode $vNameXMLaux -xml");
    system("gclc $vNameCode $vNamePIC > $vNameErrors");
    // depois faz o "rendering" do XML em linguagem natural
    // modifica o estilo de saída para a Natural Language
    system("sed -e 's/GeoConsHTML.xsl/GeoConsNL.xsl/g' $vNameXMLaux > $vNameXML"); 
    // -----------
    // agora cria o SVG correspondente ao GCLC
    system("gclc $vNameCode $vNameSVGaux -svg");

  }
  ob_end_clean(); 
  
  
  // e agora a escrita do ficheiro referente à imagem
  $fpJPG   = fopen($vNameJPG, 'r');
  $contentJPG = fread($fpJPG, filesize($vNameJPG));
  $contentJPG = addslashes($contentJPG);
  fclose($fpJPG);
  
  // e do ficheiro XML
  $fpXML = fopen($vNameXML,'r');
  $contentXML = fread($fpXML,filesize($vNameXML));
  $contentXML = addslashes($contentXML);
  fclose($fpXML);
  
  // e do ficheiro SVG
  $fpSVG = fopen($vNameSVG,'r');
  $contentSVG = fread($fpSVG,filesize($vNameSVG));
  $contentSVG = addslashes($contentSVG);
  fclose($fpSVG);
  
//   echo "<center><h3>Figura $nteo</h3></center>";
//   echo "<ul>";
//   echo "<li>
//          <span class='ficha'>Figure (JPEG format)</span>
//          - <a href='$vNameJPG'>$vNameJPG</a>
//         </li>";
//   echo "<li>
//          <span class='ficha'>
//           Description of the construction in natural language
//          </span>
//          - <a href='$vNameXML'>$vNameXML</a>
//         </li>";
//   echo "<li>
//          <span class='ficha'>Figure in SVG format</span>
//          - <a href='$vNameSVG'>$vNameSVG</a>
//         </li>\n";
//   echo "</ul>";

  // o valor de da última figura a ser inserida já foi obtido, está
  // guardado em $pFigId

  $sqlUpdatefigure = "UPDATE figures
                         SET codeXML   = '$contentXML',
                              figure    = '$contentJPG',
                           figureSVG = '$contentSVG'
                       WHERE figureId = $pFigureIdLast";


  $resultadoUpdatefigure = mysql_query($sqlUpdatefigure,$ligacao);
  
  if (!$resultadoUpdatefigure) {
    echo 'Error - Updatefigure!';
    // TRANSAÇÕES - ROLLBACK
    //    @ mysql_query("ROLLBACK");
    //echo "<meta http-equiv=\"refresh\" content=\"2; url=updateGeoThm.php?argumento=$pTeoId\" />";
    exit;
  }
  else {
    echo "<p>sqlUpdatefigure - $pFigureIdLast</p>";
    fwrite($fpMySQL,sqlUpdatefigure."\n\n"); 
  }


  /*
   =======================================================  
   Faz a inserção da informação referente às demonstrações
   =======================================================
  */


  /*
    A inserção de dados só é feita após validação do código da
    demonstração - podem ocorrer erros sintáticos assim como erros na
    construção devidos a operadores não suportados
  */

  // GCLCprover=2
  $pPrvId     = 2;
  $pBibrefPrv = $pBibRef;
  $pCodePrv   = addslashes($elementos[$aux+6]);

  
  //$vNameParaApagar     = 'proof*.*';
  //system("rm $vNameParaApagar");
  
  
  $vNameProofCode = 'proof'.$nteo.'.code';
  $vNameProofCodeXML = 'proofCode'.$nteo.'.xml';
  $vNameProofProof = 'proof'.$nteo.'_proof.tex';
  $vNameProofErr = 'proof'.$nteo.'.err';
  //  $vNameProofErrIllFormed = 'proof'.$nteo.'.errIllFormed';
  $vNameProofErrors = 'proof'.$nteo.'.errors';
  $vNameProofPIC = 'proof'.$nteo.'.pic';
  $vNameProofTeX = 'proof'.$nteo.'.tex';
  $vNameProofDVI = 'proof'.$nteo.'.dvi';
  $vNameProofPS = 'proof'.$nteo.'.ps';
  $vNameProofPDF = 'proof'.$nteo.'.pdf';
  $vNameProofProofXML = 'proof'.$nteo.'_proof.xml';

  $vNameProofXML = 'proof'.$nteo.'.xml';
  $vNameProofBZ2 = $vNameProofXML.'.bz2';
  
  $vNameProofAux = 'proofAux'.$nteo.'.aux';
  $vNameProofCodeConv = 'proof'.$nteo.'.codeconv';
  $vNameErrorsConv = 'proof'.$nteo.'.errorsconv';
  
  // Escreve o ficheiro ".code" referente ao código
  ob_start();
  print $elementos[$aux+6]."\n";
  $prooffile=fopen($vNameProofCode,"w");
  fwrite($prooffile,ob_get_contents()); 
  fclose($prooffile); 
  ob_end_clean(); 
  
  ob_start();
  // aplica o  provador GCLCprover v9.0 - Area Method

  // !!! Tenho de ver como acrescentar os Metodos de Wu e das bases de Gröbner !!!

  system("gclc $vNameProofCode $vNameProofPIC  > $vNameProofErrors");
  // 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) { 
    /* 
      No caso em que há erros não é feito mais nenhum processamento
      para este caso, isto dado que tudo o resto é ligado à produção
      da demonstração 
    */
    $file = fopen ($filename, "r");
    $contents = fread ($file, filesize ($filename));
    echo $contents."<p>";
    //system("rm proof.err");
    echo "<b>There are errors in the proof's $nteo code.</b>\n";
    echo "<br/>\n";
  } 
  else { 
    /*
      O ramo "senão" (caso não haja erros) tem de abraguer tudo o
      resto 
    */
    echo "<b>The Proof's code $nteo is correct.</b>\n";
    echo "<br/>\n";

    // Inserção dos dados gerais
    
    
    $sqlInsertProof = 
      "INSERT INTO demonstrations
                   (teoId,proverId,code,dateSubmission,userId)
            VALUES ('$pTeoId','$pPrvId','$pCodePrv','$pDateSubmission','$pUserId')";


    
    $resultadoInsertProof = mysql_query($sqlInsertProof,$ligacao);
    
    if (!$resultadoInsertProof) {
      echo 'Error - InsertProof!';
      // TRANSACÇÕES - ROLLBACK
      //    @ mysql_query("ROLLBACK");
      //echo "<meta http-equiv=\"refresh\" content=\"2; url=updateGeoThm.php?argumento=$pTeoId\" />";
      exit;
    }
    else {
      echo "<p>sqlInsertProof - $pTeoId</p>";
      fwrite($fpMySQL,$sqlInsertProof."\n\n"); 
    }
    
    
    
    // É necessário, para o que se segue, obter a identificação da
    // demonstração que se acabou de inserir.
    $pDemId=mysql_insert_id();
    
    
    // a inserção de referências bibliográficas só faz sentido se houver
    // algo para inserir
    if ($pBibRefPrv!="") {
      
      $sqlInsertProofBibRef = 
	"INSERT INTO bibproofs
                     (demId,bibrefId)
              VALUES ('$pDemId','$pBibRefPrv')";
      
    
      $resultadoInsertProofBibRef = mysql_query($sqlInsertProofBibRef,$ligacao);
      
      if (!$resultadoInsertProofBibRef) {
	echo 'Error - InsertProofBibRef!';
	// TRANSACÇÕES - ROLLBACK
	//@ mysql_query("ROLLBACK");
	//echo "<meta http-equiv=\"refresh\" content=\"2; url=updateGeoThm.php?argumento=$pTeoId\" />";
	exit;
      }
      else {
	echo "<p>sqlInsertProofBibRef - $pDemId</p>";
	fwrite($fpMySQL,$sqlInsertProofBibRef."\n\n"); 
      }
      
    }
    
    // Vai agora produzir os resultados da demonstração
    
    
    // Processa o ficheiro LaTeX com a demonstração
    ob_start();
    system("sed -e 's/{gclc_proof}/\[landscape\]{gclcproof}/g' $vNameProofProof > $vNameProofTeX");  
    
    system("latex $vNameProofTeX"); 
    system("latex $vNameProofTeX"); 
    system("dvips $vNameProofDVI"); 
    system("ps2pdf $vNameProofPS"); 
    
    ob_end_clean(); 
  
  
  
    // Vai agora criar os ficheiros XML referente ao código e à prova
    //echo "<p>Processing the XML file, please wait</p>\n";

    system("gclc  $vNameProofCode $vNameProofCodeXML -svg > $vNameProofErrors");
    
    //    echo "gclc7  $vNameProofCode $vNameProofCodeXML -svg > $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 à prova
    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);
    
    $sqlUpdateProof = 
                "UPDATE demonstrations
                    SET codeXML  = '$contentCodeXML',
                        proof    = '$contentPDF',
                        proofXML = '$contentBZ2'    
                 WHERE demId = $pDemId";

    
  
    $resultadoUpdateProof = mysql_query($sqlUpdateProof,$ligacao);
  
    if (!$resultadoUpdateProof) {
      echo 'Error - UpdateProof!';
      // TRANSA~~ES - ROLLBACK
      //      @ mysql_query("ROLLBACK");
      //echo "<meta http-equiv=\"refresh\" content=\"2; url=updateGeoThm.php?argumento=$pTeoId\" />";
      exit;
    }
    else {
      echo "<p>sqlUpdateProof - $pDemId</p>";
      fwrite($fpMySQL,sqlUpdateProof."\n\n"); 
    }
  
    // Fim - inserção da prova
    
    // Preenchimento do campo "status"
    
    // vai obter o resultado da tentativa de prova
    ob_start();
    $vResult=system("./provedDisproved < $vNameProofTeX");
    ob_end_clean();
    //   1 = proved (if the conjecture was proved valid)
    //   0 = disproved (if the conjecture was proved invalid)
    //   2 = Failed to prove the conjecture (if neither of above two)
    if ($vResult==1) 
      $vStatus="Proved";
    elseif ($vResult==2)
      $vStatus="Disproved";
    else
      $vStatus="Failed to prove the conjecture";
    
    $sqlProofStatus = "UPDATE demonstrations
                          SET status = '$vStatus'
                        WHERE demId = $pDemId";
  

    $resultadoProofStatus = mysql_query($sqlProofStatus,$ligacao);
    
    if (!$resultadoProofStatus) {
      echo 'Error - ProofStatus!';
      // TRANSAÇÕES - ROLLBACK
      //      @ mysql_query("ROLLBACK");
      //echo "<meta http-equiv=\"refresh\" content=\"2; url=updateGeoThm.php?argumento=$pTeoId\" />";
      exit;
    }
    else {
      echo "<p>sqlProofStatus - $vStatus</p>";
      fwrite($fpMySQL,$sqlProofStatus."\n\n"); 
    }

    // E agora os resultados das medidas de eficiência
    
    if ($pPrvId==2 || $pPrvId==3) {
      // para o  provador GCLCprover 1.0
      // ou
      // para o provador GCLCprover 1.0 após o conversor euktogclcprover 1.0
      ob_start();
      $elimSteps=system("nEliminationSteps < $vNameProofTeX");
      $geoSteps=system("nGeometricSteps < $vNameProofTeX");
      $algSteps=system("nAlgebraicSteps < $vNameProofTeX");
      $totalSteps=system("nTotalSteps < $vNameProofTeX");
      $sTime=system("sTime < $vNameProofTeX");
      ob_end_clean();
    }
    
    // Vai obter os dados do Computador de serviço 
    // isto é na tabela "computador" estão os dados do meu computador
    // actual, aquele aonde os programas estão a ser executados.
    
    $sqlComputer = "SELECT CPUBrand,CPUType,speed,RAM
                      FROM computer";
  

    $resultadoComputer = mysql_query($sqlComputer,$ligacao);
    
    if (!$resultadoComputer) {
      echo 'Error - Computer!';
      // TRANSAçõES - ROLLBACK
      //@ mysql_query("ROLLBACK");
      //echo "<meta http-equiv=\"refresh\" content=\"2; url=updateGeoThm.php?argumento=$pTeoId\" />";
      exit;
    }
    else {

      $linhaComputer = mysql_fetch_assoc($resultadoComputer);

      $pCPUBrand = trim($linhaComputer['CPUBrand']);
      $pCPUType  = trim($linhaComputer['CPUType']);
      $pSpeed    = trim($linhaComputer['speed']);
      $pRAM      = trim($linhaComputer['RAM']);
      
      $computerSpecs = $pCPUBrand." ".$pCPUType.", ".$pSpeed."GHz, ".$pRAM."GB";
      
      echo "<p>sqlComputer - $computerSpecs</p>";
    }

    
    $sqlProofMeasures = 
      "INSERT INTO measures
                   (measuresId,elimSteps,geoSteps,algSteps,timeCPU,
                    computerSpecs)
             VALUES
                   ('$pDemId','$elimSteps','$geoSteps','$algSteps',
                    '$sTime','$computerSpecs')";


    $resultadoProofMeasures = mysql_query($sqlProofMeasures,$ligacao);
    
    if (!$resultadoProofMeasures) {
      echo 'Error - Computer!';
      // TRANSAçõES - ROLLBACK
      //      @ mysql_query("ROLLBACK");
      //echo "<meta http-equiv=\"refresh\" content=\"2; url=updateGeoThm.php?argumento=$pTeoId\" />";
      exit;
    }
    else {
      echo "<p>sqlProofMeasures - $pDemId</p>";
      fwrite($fpMySQL,$sqlProofMeasures."\n\n"); 
    }          
    
    
  } // fim da actualização da prova + status


  $aux+=8;
  $nteo++;
 }

//$resultadoInsertGeoTheorem    = mysql_query($sqlInsertGeoTheorem,$ligacao);
//$resultadoInsertTheoremBibRef = mysql_query($sqlInsertTheoremBibRef,$ligacao);



//$texfile=fopen("descriptions.tex","w");
//fwrite($texfile,ob_get_contents()); 
//fclose($texfile); 
//ob_end_clean(); 

fclose($fpElementos);
fclose($fpMySQL);

// Faz o rollback da transacção.
//@ mysql_query("ROLLBACK");


//Free the XML parser
xml_parser_free($parser);

?>