path: root/test/spass/tableau.c

/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *                  TABLEAU PROOF TREES                   * */
/* *                                                        * */
/* *  Copyright (C) 1998, 1999, 2000, 2001                  * */
/* *  MPI fuer Informatik                                   * */
/* *                                                        * */
/* *  This program is free software; you can redistribute   * */
/* *  it and/or modify it under the terms of the GNU        * */
/* *  General Public License as published by the Free       * */
/* *  Software Foundation; either version 2 of the License, * */
/* *  or (at your option) any later version.                * */
/* *                                                        * */
/* *  This program is distributed in the hope that it will  * */
/* *  be useful, but WITHOUT ANY WARRANTY; without even     * */
/* *  the implied warranty of MERCHANTABILITY or FITNESS    * */
/* *  FOR A PARTICULAR PURPOSE.  See the GNU General Public * */
/* *  License for more details.                             * */
/* *                                                        * */
/* *  You should have received a copy of the GNU General    * */
/* *  Public License along with this program; if not, write * */
/* *  to the Free Software Foundation, Inc., 59 Temple      * */
/* *  Place, Suite 330, Boston, MA  02111-1307  USA         * */
/* *                                                        * */
/* $Revision: 21527 $                                        * */
/* $State$                                            * */
/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $                             * */
/* $Author: duraid $                                       * */
/* *                                                        * */
/* *                                                        * */
/* *             Contact:                                   * */
/* *             Christoph Weidenbach                       * */
/* *             MPI fuer Informatik                        * */
/* *             Stuhlsatzenhausweg 85                      * */
/* *             66123 Saarbruecken                         * */
/* *             Email: weidenb@mpi-sb.mpg.de               * */
/* *             Germany                                    * */
/* *                                                        * */
/* ********************************************************** */

/* $RCSfile$ */

#include "tableau.h" 

/* for graph output */
extern BOOL        pcheck_ClauseCg;
extern GRAPHFORMAT pcheck_GraphFormat;

TABPATH tab_PathCreate(int MaxLevel, TABLEAU Tab)
/**************************************************************
  INPUT:   A tableau, its maximum expected depth
  RETURNS: A path consisting of the root  node of the tableau
           which can have a max length of <MaxLevel>
***************************************************************/
{
  TABPATH TabPath;

  TabPath            = (TABPATH)memory_Malloc(sizeof(TABPATH_NODE));
  TabPath->Path      = (TABLEAU*)memory_Malloc(sizeof(TABLEAU)*(MaxLevel+1));
  TabPath->Path[0]   = Tab;
  TabPath->MaxLength = MaxLevel;
  TabPath->Length    = 0;
  
  return TabPath;
}

void tab_PathDelete(TABPATH TabPath)
/**************************************************************
  INPUT:   A tableau path.
  RETURNS: Nothing.
  EFFECTS: The path is deleted.
***************************************************************/
{
  memory_Free(TabPath->Path, (TabPath->MaxLength+1)*sizeof(TABLEAU));
  memory_Free(TabPath, sizeof(TABPATH_NODE));
}


BOOL tab_PathContainsClause(TABPATH Path, CLAUSE Clause)
/**************************************************************
  INPUT:   A tableau path, a clause
  RETURNS: TRUE iff the clause exists on its level (wrt. the
           path) in the tableau
***************************************************************/
{
  LIST Scan;

  if (clause_SplitLevel(Clause) > tab_PathLength(Path))
    return FALSE;

  for (Scan = tab_Clauses(tab_PathNthNode(Path, clause_SplitLevel(Clause))); 
       !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    if (list_Car(Scan) == Clause)
      return TRUE;
  }
  return FALSE;
}

static BOOL tab_PathContainsClauseSoft(TABPATH Path, CLAUSE Clause)
/**************************************************************
  INPUT:   A tableau path, a clause
  RETURNS: TRUE iff the clause is on one of the levels
           in the tableau traversed by the path. Different
	   from tab_PathContainsClauseSoft, since it does
           not expect the clause on its split level.
***************************************************************/
{
  LIST Scan;
  int Level;

  if (clause_SplitLevel(Clause) > tab_PathLength(Path))
    return FALSE;
  
  for (Level = 0; Level <= tab_PathLength(Path); Level++) {
    for (Scan = tab_Clauses(tab_PathNthNode(Path, Level));  
	 !list_Empty(Scan); Scan = list_Cdr(Scan)) {
      if (list_Car(Scan) == Clause)
	return TRUE;
    }
  }
  return FALSE;
}

/* unused */
/*static*/ BOOL tab_PathContainsClauseRobust(TABPATH P, CLAUSE C)
/**************************************************************
  INPUT:   A tableau path, a clause
  RETURNS: TRUE if clause can be find on the path (not
           necessarily on its level)
  EFFECTS: Prints a note if clause cannot be found on
           its level. Intended for debugging.
***************************************************************/
{
  if (tab_PathContainsClause(P,C)) 
    return TRUE;

  if (tab_PathContainsClauseSoft(P,C)) {
    fputs("NOTE: Clause is found on path, but not indexed by level.\n", stderr);
    clause_PParentsFPrint(stderr,C);
    fflush(stderr);
    return TRUE;
  }
  return FALSE;
}


void tab_AddSplitAtCursor(TABPATH Path, BOOL LeftSide)
/**************************************************************
  INPUT:   A tableau path, a flag
  RETURNS: Nothing.
  EFFECTS: Extends the tableau containing the path <Path> to
           the left if <LeftSide> is TRUE, to the right 
	   otherwise
***************************************************************/
{
  TABLEAU Tab, NewBranch;

  Tab = tab_PathTop(Path);
  NewBranch = tab_CreateNode();
  if (LeftSide) {

#ifdef CHECK
    if (!tab_LeftBranchIsEmpty(Tab)) {
      misc_StartErrorReport();
      misc_ErrorReport("\n In tab_AddSplitAtCursor: Recreating existing");
      misc_ErrorReport(" left branch in tableau.\n");
      misc_FinishErrorReport();
    }
#endif

    tab_SetLeftBranch(Tab,NewBranch);
  } else {

#ifdef CHECK    
    if (!tab_RightBranchIsEmpty(Tab)) {
      misc_StartErrorReport();
      misc_ErrorReport("\n In tab_AddSplitAtCursor: Recreating existing");
      misc_ErrorReport(" right branch in tableau.\n");
      misc_FinishErrorReport();
    }
#endif
    tab_SetRightBranch(Tab, NewBranch);
  }
  tab_PathPush(NewBranch, Path);
}

void tab_AddClauseOnItsLevel(CLAUSE C, TABPATH Path)
/**************************************************************
  INPUT:   A clause, a tableau path 
  RETURNS: Nothing
  EFFECTS: Adds the clause on its split level which
           must belong to <Path>
***************************************************************/
{
  int Level; 

  Level = clause_SplitLevel(C);
  if (Level > tab_PathLength(Path)) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("\nError: Split level of some clause ");
    misc_UserErrorReport("\nis higher than existing level."); 
    misc_UserErrorReport("\nThis may be a bug in the proof file."); 
    misc_FinishUserErrorReport();  
  }
  
  tab_AddClause(C, tab_PathNthNode(Path, clause_SplitLevel(C)));
}


int tab_Depth(TABLEAU T)
/**************************************************************
  INPUT:   A tableau
  RETURNS: The depth of the tableau
***************************************************************/
{
  if (tab_IsEmpty(T))
    return 0;
  if (tab_IsLeaf(T))
    return 0;
  else 
    return (misc_Max(tab_Depth(tab_RightBranch(T))+1, tab_Depth(tab_LeftBranch(T)))+1);
}

static BOOL tab_HasEmptyClause(TABLEAU T)
/**************************************************************
  INPUT:   A tableau                                                     
  RETURNS: TRUE iff an empty clause is among the clauses
           on this level
***************************************************************/
{
  LIST Scan;
  
  for (Scan = tab_Clauses(T); !list_Empty(Scan); Scan = list_Cdr(Scan)) 
    if (clause_IsEmptyClause(list_Car(Scan)))
      return TRUE;

  return FALSE;
}


BOOL tab_IsClosed(TABLEAU T)
/**************************************************************
  INPUT:   A Tableau   
  RETURNS: TRUE iff the tableau is closed. (NOTE: FALSE
           if the tableau is empty)
***************************************************************/
{
  if (tab_IsEmpty(T))
    return FALSE;

  if (tab_HasEmptyClause(T))
      return TRUE;
  /* 
   *  now tableau can only be closed
   *  if there has been a split, and
   *  both subtableaus are closed 
   */
  
  if (tab_RightBranchIsEmpty(T) || tab_LeftBranchIsEmpty(T)) {
    printf("\nopen node label: %d", T->Label);
    fflush(stdout);

    return FALSE;
  }
  return tab_IsClosed(tab_RightBranch(T)) && tab_IsClosed(tab_LeftBranch(T));
}

static LIST tab_DeleteFlat(TABLEAU T)
/**************************************************************
  INPUT:   A tableau
  RETURNS: The list of its clauses on the first level of
          the tableau
  EFFECTS: Frees the root tableau node.
***************************************************************/
{
  LIST Clauses;

  Clauses = tab_Clauses(T);
  memory_Free(T, sizeof(TABLEAU_NODE));
  
  return Clauses;
}


static void tab_DeleteGen(TABLEAU T, LIST* Clauses, BOOL DeleteClauses)
/**************************************************************
  INPUT:   A tableau, a list of clauses by reference, a flag 
  RETURNS: Nothing
  EFFECTS: Depending on <DeleteClauses>, all clauses in the
           tableau are added to <Clauses> or just deleted.
 	   The memory for the tableau and its clause lists is
	   freed.
***************************************************************/
{
  if (tab_IsEmpty(T))
    return;
  
  tab_DeleteGen(tab_RightBranch(T), Clauses, DeleteClauses);
  tab_DeleteGen(tab_LeftBranch(T),  Clauses, DeleteClauses);

  list_Delete(tab_RightSplitClauses(T));
  if (DeleteClauses) 
    list_Delete(tab_Clauses(T)); 
  else
    *Clauses = list_Nconc(tab_Clauses(T), *Clauses);
  
  tab_DeleteFlat(T);
  
}

static void tab_DeleteCollectClauses(TABLEAU T, LIST* Clauses)
/**************************************************************
  INPUT:   A tableau, a list of clauses by reference
  RETURNS: Nothing
  EFFECTS: Frees the memory of the tableau, but collects
           its clauses
***************************************************************/
{
  tab_DeleteGen(T, Clauses, FALSE);
}

void tab_Delete(TABLEAU T)
/**************************************************************
  INPUT:   A tableau
  RETURNS: Nothing
  EFFECTS: Frees the memory of the tableau
***************************************************************/
{
  LIST Redundant;
  
  Redundant = list_Nil();
  tab_DeleteGen(T, &Redundant, TRUE);
}

static void tab_SetSplitLevelsRec(TABLEAU T, int Level)
/**************************************************************
  INPUT:   A tableau
  RETURNS: Nothing                                                     
  EFFECTS: The split levels of the clauses in the
           tableau are set to the level of the
	   tableau level they are contained in.
***************************************************************/
{
  LIST Scan;

  if (tab_IsEmpty(T))
    return;
  
  for (Scan = tab_Clauses(T); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    clause_SetSplitLevel(list_Car(Scan), Level); 
    if (Level >0) {
      clause_ClearSplitField(list_Car(Scan));
      clause_SetSplitFieldBit(list_Car(Scan), Level);
    }
    else 
      clause_SetSplitField(list_Car(Scan), (SPLITFIELD)NULL,0);
  }
  
  tab_SetSplitLevelsRec(tab_RightBranch(T), Level+1);
  tab_SetSplitLevelsRec(tab_LeftBranch(T), Level+1);
}

void tab_SetSplitLevels(TABLEAU T)
/**************************************************************
  INPUT:   A tableau                                                     
  RETURNS: Nothing                                                     
  EFFECTS: The split levels of the clauses in the
           tableau are set to the level of the
	   tableau they belong to.
***************************************************************/
{
  tab_SetSplitLevelsRec(T,0);
}


TABLEAU tab_PruneClosedBranches(TABLEAU T, LIST* Clauses) 
/**************************************************************
  INPUT:   A tableau, a list of clauses by reference.
  RETURNS: The (destructively) reduced tableau: Descendants of
           nodes that have an empty clause are deleted.
  EFFECTS: The tableau is modified.
***************************************************************/
{
  if (tab_IsEmpty(T))
    return T;

  /* if there is an empty clause on this level, delete subtrees */

  if (tab_HasEmptyClause(T)) {

    tab_DeleteCollectClauses(tab_RightBranch(T), Clauses); 
    tab_DeleteCollectClauses(tab_LeftBranch(T), Clauses); 
    tab_SetRightBranch(T, tab_EmptyTableau());
    tab_SetLeftBranch(T, tab_EmptyTableau()); 
    list_Delete(tab_RightSplitClauses(T));
    tab_SetRightSplitClauses(T, list_Nil());
    tab_SetSplitClause(T,clause_Null());
    tab_SetLeftSplitClause(T, clause_Null());
  }
  /* else recursively prune subtrees */
  else {
    tab_SetRightBranch(T, tab_PruneClosedBranches(tab_RightBranch(T), Clauses));
    tab_SetLeftBranch(T, tab_PruneClosedBranches(tab_LeftBranch(T), Clauses));
  }
  
  return T;
}


TABLEAU tab_RemoveIncompleteSplits(TABLEAU T, LIST* Clauses)
/**************************************************************
  INPUT:   A Tableau, a list of clauses by reference
  RETURNS: The reduced tableau: If a node has exactly one
           successor (that is, the corresponding split was
           not completed), delete the successor and move
	   its subtrees to <T>.
  EFFECTS: The successor node is deleted, and its clauses added
           to <Clauses>
***************************************************************/
{
  LIST    NewClauses;
  TABLEAU Child;

  if (tab_IsEmpty(T))
    return T;

  if (tab_IsLeaf(T))
    return T;

  if (!tab_IsEmpty(tab_RightBranch(T)) &&
      !tab_IsEmpty(tab_LeftBranch(T))) {	   
    tab_SetRightBranch(T, tab_RemoveIncompleteSplits(tab_RightBranch(T), Clauses));
    tab_SetLeftBranch(T, tab_RemoveIncompleteSplits(tab_LeftBranch(T), Clauses));
    return T;
  }
  if (tab_IsEmpty(tab_RightBranch(T))) 
    Child = tab_LeftBranch(T);
  else 
    Child = tab_RightBranch(T);

  Child = tab_RemoveIncompleteSplits(Child, Clauses);

  tab_SetLeftBranch(T, tab_LeftBranch(Child));   
  tab_SetRightBranch(T, tab_RightBranch(Child));

  /* copy split data */

  tab_SetSplitClause(T, tab_SplitClause(Child));
  tab_SetLeftSplitClause(T, tab_LeftSplitClause(Child));
  tab_SetRightSplitClauses(T, tab_RightSplitClauses(Child));

  /* delete ancestors of deleted clauses and remember */

  NewClauses = tab_DeleteFlat(Child);
  (*Clauses) = list_Nconc(NewClauses, *Clauses);

  return T;
}


void tab_CheckEmpties(TABLEAU T)
/**************************************************************
  INPUT:   A tableau 
  RETURNS: Nothing.
  EFFECTS: Prints warnings if non-leaf nodes contain
           empty clauses (which should not be the case
           after pruning any more), of if leaf nodes
	   contain more than one empty clause
***************************************************************/
{
  LIST Scan, Empties;
  BOOL Printem;

  if (tab_IsEmpty(T))
    return;

  /* get all empty clauses in this node */ 
  Empties = list_Nil();
  for (Scan = tab_Clauses(T); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
    if (clause_IsEmptyClause(list_Car(Scan)))
      Empties = list_Cons(list_Car(Scan), Empties);
  }
  Printem = FALSE;
  if (!list_Empty(Empties) && !tab_IsLeaf(T)) {
    puts("\nNOTE: non-leaf node contains empty clauses.");
    Printem = TRUE;
  }
  
  if (tab_IsLeaf(T) && list_Length(Empties) > 1) {
    puts("\nNOTE: Leaf contains more than one empty clauses.");
    Printem = TRUE;
  }
  if (Printem) {
    puts("Clauses:");
    clause_PParentsListPrint(tab_Clauses(T));
  }
  list_Delete(Empties);
  tab_CheckEmpties(tab_LeftBranch(T));
  tab_CheckEmpties(tab_RightBranch(T));
}


void tab_GetAllEmptyClauses(TABLEAU T, LIST* L)
/**************************************************************
  INPUT:   A tableau, a list by reference
  RETURNS: All empty clauses in the tableau prepended to <L>.
***************************************************************/
{
  if (tab_IsEmpty(T))
    return;
  
  tab_GetAllEmptyClauses(tab_LeftBranch(T), L);
  tab_GetAllEmptyClauses(tab_RightBranch(T), L);
}


void tab_GetEarliestEmptyClauses(TABLEAU T, LIST* L)
/**************************************************************
  INPUT  : A tableau, a list of clauses by reference
  RETURNS: Nothing. 
  EFFECTS: For each leaf node, adds empty clauses in
           leaf nodes to <L>. If the leaf node contains only one
	   empty clause, it is added to <L> anyway.
           If the leaf node contains more than one empty clause,
	   the earliest derived empty clause is added to <L>.
***************************************************************/
{
  CLAUSE FirstEmpty;
  LIST   Scan;

  if (tab_IsEmpty(T))
    return;

  if (tab_IsLeaf(T)) {  
    FirstEmpty = clause_Null();
  
    for (Scan = tab_Clauses(T); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
      if (clause_IsEmptyClause(list_Car(Scan))) {
	if (FirstEmpty == clause_Null()) 
	  FirstEmpty = list_Car(Scan);
	else if (clause_Number(FirstEmpty) > clause_Number(list_Car(Scan)))
	  FirstEmpty = list_Car(Scan);
      }
    }
    
    if (FirstEmpty != clause_Null())
      (*L) = list_Cons(FirstEmpty, *L);
  }
  tab_GetEarliestEmptyClauses(tab_LeftBranch(T), L);
  tab_GetEarliestEmptyClauses(tab_RightBranch(T), L);

}

void tab_ToClauseList(TABLEAU T, LIST* Proof)
/**************************************************************
  INPUT:   A tableau <T>, a list of clauses 
  RETURNS: Nothing.
  EFFECTS: All clauses in T are added to <Proof>
***************************************************************/
{
  if (tab_IsEmpty(T))
    return;
  
  (*Proof) = list_Nconc(list_Copy(tab_Clauses(T)), *Proof);

  tab_ToClauseList(tab_LeftBranch(T),Proof);
  tab_ToClauseList(tab_RightBranch(T),Proof);
}


static void tab_ToSeqProofOrdered(TABLEAU T, LIST* Proof)
/**************************************************************
  INPUT:   A tableau <T>, a list of clauses <Proof> representing a 
           proof by reference
  RETURNS: The sequential proof corresponding to the tableau.
***************************************************************/
{
  LIST Scan;
  BOOL RightSplitRead, LeftSplitRead;
  
  if (tab_IsEmpty(T))
    return;

  Scan = tab_Clauses(T); 
  RightSplitRead = LeftSplitRead = FALSE;

  while (!list_Empty(Scan)) {
    /* insert left and right splits and descendants controlled by clause number */

    if (!RightSplitRead && !tab_RightBranchIsEmpty(T) &&
	clause_Number(list_Car(Scan)) <
	clause_Number(list_Car(tab_RightSplitClauses(T)))) {
      tab_ToSeqProofOrdered(tab_RightBranch(T), Proof);
      RightSplitRead = TRUE;
    }
    if (!LeftSplitRead && !tab_LeftBranchIsEmpty(T) &&
	clause_Number(list_Car(Scan)) < 
	clause_Number(tab_LeftSplitClause(T))) {
      tab_ToSeqProofOrdered(tab_LeftBranch(T), Proof);
      LeftSplitRead  = TRUE;
    }
    (*Proof) = list_Cons(list_Car(Scan), *Proof); 
    Scan  = list_Cdr(Scan);
  }
  /* if a split clause with descendants has not been inserted yet, 
     it been generated after all other clauses */

  if (!RightSplitRead)
    tab_ToSeqProofOrdered(tab_RightBranch(T), Proof);
  if (!LeftSplitRead)
    tab_ToSeqProofOrdered(tab_LeftBranch(T), Proof);
}


/****************************************************************/
/*  SPECIALS FOR GRAPHS                                         */
/****************************************************************/

static void tab_LabelNodesRec(TABLEAU T, int* Num)
/**************************************************************
  INPUT:   A Tableau, a number by reference
  RETURNS: Nothing.
  EFFECTS: Labels the tableau nodes dflr, starting with <Num>
***************************************************************/
{
  if (tab_IsEmpty(T))
    return;
  T->Label = *Num;
  (*Num)++;
  tab_LabelNodesRec(tab_LeftBranch(T), Num);
  tab_LabelNodesRec(tab_RightBranch(T), Num);
}


void tab_LabelNodes(TABLEAU T)
/**************************************************************
  INPUT:   A Tableau, a number by reference
  RETURNS: Nothing.
  EFFECTS: Labels the tableau nodes dflr, starting with 0
***************************************************************/
{
  int Num;

  Num = 0;
  tab_LabelNodesRec(T, &Num);
}


static void tab_FPrintNodeLabel(FILE *File, TABLEAU T)
/**************************************************************
  INPUT:   A file handle, a tableau 
  RETURNS: Nothing.
  EFFECTS: Prints the root node information to <File>:
           clauses, split information
***************************************************************/
{
  LIST Scan;

  /* start printing of node label string */
  
  fprintf(File, "\"label: %d\\n", T->Label);
  
  /* print left and right parts of split */
  fputs("SplitClause : ", File); 
  clause_PParentsFPrint(File, tab_SplitClause(T));
  fputs("\\nLeft Clause : ", File);
  clause_PParentsFPrint(File, tab_LeftSplitClause(T));
  fputs("\\nRightClauses: ", File);
  if (list_Empty(tab_RightSplitClauses(T)))
    fputs("[]\\n", File);
  else {
    clause_PParentsFPrint(File, list_Car(tab_RightSplitClauses(T)));
    fputs("\\n", File);
    for (Scan = list_Cdr(tab_RightSplitClauses(T)); !list_Empty(Scan); Scan = list_Cdr(Scan)) {
      fputs("              ", File);
      clause_PParentsFPrint(File, list_Car(Scan));
      fputs("\\n", File);
    }
  }
  /* print clause at this level */
  if (pcheck_ClauseCg) {
    if (list_Empty(tab_Clauses(T)))
      fputs("[]", File);
    else {
      for (Scan = tab_Clauses(T); !list_Empty(Scan); Scan = list_Cdr(Scan)){
	clause_PParentsFPrint(File, list_Car(Scan)); 
	fputs("\\n", File);
      }
    }
  }
  putc('"', File); /* close string */
}


static void tab_FPrintEdgeCgFormat(FILE* File, int Source, int Target, BOOL Left)
/**************************************************************
  INPUT:   A file handle, two node labels, a flag
  RETURNS: Nothing.
  EFFECTS: Prints the edge denoted by <Source> and <Target>
           to <File>, with an edge label (0/1) according to <Left>.
	   The edge label is added since xvcg cannot handle
           ordered edges.
***************************************************************/
{
  fputs("\nedge: {", File);
  fprintf(File, "\nsourcename: \"%d\"", Source);
  fprintf(File, "\ntargetname: \"%d\"\n", Target);
  fputs("\nlabel: \"", File);
  if (Left) 
    putc('0', File);
  else
    putc('1', File);
  fputs("\"  }\n", File);
} 


static void tab_FPrintEdgesCgFormat(FILE* File, TABLEAU T)
/**************************************************************
  INPUT:   A file handle, a tableau
  RETURNS: Nothing.
  EFFECTS: Prints edge information of <T> in xvcg graph format
           to <File>.
***************************************************************/
{
  if (tab_IsEmpty(T))
    return;

  if (!tab_LeftBranchIsEmpty(T))
    tab_FPrintEdgeCgFormat(File, T->Label, tab_LeftBranch(T)->Label, TRUE);
  if (!tab_RightBranchIsEmpty(T))
    tab_FPrintEdgeCgFormat(File, T->Label, tab_RightBranch(T)->Label, FALSE);
  
  tab_FPrintEdgesCgFormat(File, tab_LeftBranch(T));
  tab_FPrintEdgesCgFormat(File, tab_RightBranch(T));
}


static void tab_FPrintNodesCgFormat(FILE* File, TABLEAU T)
/**************************************************************
  INPUT:   A file handle, a tableau
  RETURNS: Nothing
  EFFECTS: Prints egde information of <T> in xvcg graph format
           to <File>.                                            
***************************************************************/
{
  if (tab_IsEmpty(T))
    return;

  fputs("\nnode: {\n\nlabel: ", File);
  tab_FPrintNodeLabel(File, T);
  putc('\n', File); /* end label section */
  
  fprintf(File, "title: \"%d\"\n", T->Label);
  fputs("  }\n", File);
  
  /* recursion */
  tab_FPrintNodesCgFormat(File, tab_LeftBranch(T));
  tab_FPrintNodesCgFormat(File, tab_RightBranch(T));
  
} 

static void tab_FPrintCgFormat(FILE* File, TABLEAU T)
/**************************************************************
  INPUT:   A file handle, a tableau
  RETURNS: Nothing.
  EFFECTS: Prints tableau as a graph in xvcg format to <File>
***************************************************************/
{
  fputs("graph: \n{\ndisplay_edge_labels: yes\n", File);
  
  tab_FPrintNodesCgFormat(File, T);
  tab_FPrintEdgesCgFormat(File, T); 
  fputs("}\n", File);
}

/* unused */
/*static*/ void tab_PrintCgFormat(TABLEAU T)
/**************************************************************
  INPUT:   A tableau. 
  RETURNS: Nothing.                                                     
  EFFECTS: Print tableau in xvcg format to stdout
***************************************************************/
{
  tab_FPrintCgFormat(stdout, T);
}


/**************************************************************/
/* procedures for printing graph in da Vinci format           */
/**************************************************************/

static void tab_FPrintDaVinciEdge(FILE* File, int L1, int L2)
/**************************************************************
  INPUT:   A file handle, two numbers 
  RETURNS: Nothing 
  EFFECTS: Print an edge in daVinci format
***************************************************************/
{
  fprintf(File, "l(\"%d->%d\","   ,L1,L2);
  fputs("e(\"\",[],\n", File);
  /* print child node as reference */
  fprintf(File, "r(\"%d\")))\n", L2);
}


static void tab_FPrintDaVinciFormatRec(FILE* File, TABLEAU T)
/**************************************************************
  INPUT:   A file handle, a tableau
  RETURNS: Nothing
  EFFECTS: Prints tableau to <File> in daVinci format
***************************************************************/
{
  /* print node label */
  fprintf(File, "l(\"%d\",", T->Label);
  /* print node attributes */
  fputs("n(\"\", [a(\"OBJECT\",", File); 
  tab_FPrintNodeLabel(File, T);
  fputs(")],\n", File);
  
  /* print egde list  */
  putc('[', File);
  if (!tab_LeftBranchIsEmpty(T)) 
    tab_FPrintDaVinciEdge(File, T->Label, tab_LeftBranch(T)->Label); 

  if (!tab_RightBranchIsEmpty(T)) {
    if (!tab_LeftBranchIsEmpty(T))
      putc(',', File);
    tab_FPrintDaVinciEdge(File, T->Label, tab_RightBranch(T)->Label);
  }
  fputs("]))", File); /* this ends the node description */

  if (!tab_LeftBranchIsEmpty(T)) {
    putc(',', File);
    tab_FPrintDaVinciFormatRec(File, tab_LeftBranch(T));
  }
  if (!tab_RightBranchIsEmpty(T)) {
    putc(',', File);
    tab_FPrintDaVinciFormatRec(File, tab_RightBranch(T));
  }
}


static void tab_FPrintDaVinciFormat(FILE* File, TABLEAU T)
/**************************************************************
  INPUT:   A file handle <File>, a tableau
  RETURNS: Nothing
  EFFECTS: Print tableau in daVinci format to <File>
***************************************************************/
{
  fputs("[\n", File);
  tab_FPrintDaVinciFormatRec(File,T);
  fputs("]\n", File);
}


void tab_WriteTableau(TABLEAU T, const char* Filename, GRAPHFORMAT Format)
/**************************************************************
  INPUT:   A tableau, a filename 
  RETURNS: Nothing.
***************************************************************/
{
  FILE*  File;
  
  if (Format != DAVINCI && Format != XVCG) {
    misc_StartUserErrorReport();
    misc_UserErrorReport("\nError: unknown output format for tableau.\n");
    misc_FinishUserErrorReport();
  }

  File = misc_OpenFile(Filename, "w");

  if (Format == DAVINCI)
    tab_FPrintDaVinciFormat(File, T);
  else 
    if (Format == XVCG)
      tab_FPrintCgFormat(File, T);

  misc_CloseFile(File, Filename);
}