/**CFile***********************************************************************

  FileName    [ltlSet.c]

  PackageName [ltl]

  Synopsis    [Set/Pair/Cover Manipulation functions used in the ltl package.]

  Author      [Chao Wang<chao.wang@colorado.EDU>]

  Copyright   [This file was created at the University of Colorado at Boulder.
  The University of Colorado at Boulder makes no warranty about the suitability
  of this software for any purpose.  It is presented on an AS IS basis.]

******************************************************************************/

#include "ltlInt.h"

static char rcsid[] UNUSED = "$Id: ltlSet.c,v 1.25 2005/04/28 08:45:27 bli Exp $";

/* Set manipulation functions.
 *  
 * Set is a term -- the conjunction of literals. In the Ltl->Aut process, a
 * literal can be an propositional formula, a X-formula and its negation.
 * In order to interpret a Set, we need to corresponding arrays: Table and
 * Negate. An '1' in the i-th position of the Set means "Table[i] is contained
 * in the Set", and the negation of "Table[i]" is "Negate[i]".
 * 
 * Cover is a lsList of terms -- the "union" of all the items (product terms).
 *
 * Pair is a data structure to hold a 'ordered pair of items': (First, Second).
 */

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Allocate the set data structure.]

  Description []

  SideEffects [The result should be freed by the caller.]

******************************************************************************/
LtlSet_t *
LtlSetNew(
  int size)
{
  LtlSet_t *set = ALLOC(LtlSet_t, 1);
    
  set->e = var_set_new(size);

  return set;
}

/**Function********************************************************************

  Synopsis    [Free the data structure associated with 'set'.]

  Description []

  SideEffects []

******************************************************************************/
void
LtlSetFree(
  LtlSet_t *set)
{
  var_set_free(set->e);
  FREE(set);
}

/**Function********************************************************************

  Synopsis    [Allocate the new set and copy the content of the given set.]

  Description []

  SideEffects [The result should be freed by the caller.]

******************************************************************************/
LtlSet_t *
LtlSetCopy(
  LtlSet_t *from)
{
  LtlSet_t *set = ALLOC(LtlSet_t, 1);
  
  set->e = var_set_copy(from->e);
  
  return set;
}

/**Function********************************************************************

  Synopsis    [Assign the content of 'from' to set 'to'.]

  Description []

  SideEffects [set 'to' is changed.]

******************************************************************************/
void
LtlSetAssign(
  LtlSet_t *to,
  LtlSet_t *from)
{
  var_set_assign(to->e, from->e);
}

/**Function********************************************************************

  Synopsis    [Return 1 if the two sets have the same content.]

  Description []

  SideEffects []

******************************************************************************/
int
LtlSetEqual(
  LtlSet_t *s1,
  LtlSet_t *s2)
{
  return var_set_equal(s1->e, s2->e);
}


/**Function********************************************************************

  Synopsis    [Return how many bit is set to 1 in the given set.]

  Description []

  SideEffects []

******************************************************************************/
int
LtlSetCardinality(
  LtlSet_t *set)
{
  return (var_set_n_elts(set->e));
}

/**Function********************************************************************

  Synopsis    [Return -1/0/+1 when 's1' has more/equal/less cardinality than
  's2'.]

  Description []

  SideEffects []

******************************************************************************/
int
LtlSetCompareCardinality(
  const void *p1,
  const void *p2)
{
  LtlSet_t **s1 = (LtlSet_t **) p1;
  LtlSet_t **s2 = (LtlSet_t **) p2;
  int c1;
  int c2;
  
  c1 = LtlSetCardinality(*s1);
  c2 = LtlSetCardinality(*s2);
  
  if (c1 < c2)
    return -1;
  else if (c1 == c2)
    return 0;
  else
    return +1;
}

/**Function********************************************************************

  Synopsis    [Return 1 iff the set contains both 'F' and '!F'.]

  Description []

  SideEffects []

******************************************************************************/
int
LtlSetIsContradictory(
  LtlSet_t *set,
  array_t *Negate)
{
  int i, negi;
  int flag = 0;

  for (i=0; i<array_n(Negate); i++) {
    if (LtlSetGetElt(set, i)) {
      negi = array_fetch(int, Negate, i);
      if (LtlSetGetElt(set, negi)) {
	flag = 1;
	break;
      }
    }
  }
  
  return flag;
}

/**Function********************************************************************

  Synopsis    [Return 1 iff 'large' includes 'small'.]

  Description []

  SideEffects []

******************************************************************************/
int
LtlSetInclude(
  LtlSet_t *large,
  LtlSet_t *small)
{
  var_set_t *neg_large = var_set_not(var_set_copy(large->e),large->e);
  int result = ! var_set_intersect(small->e, neg_large);
  var_set_free(neg_large);
  
  return result;
}

/**Function********************************************************************

  Synopsis    [Union the two sets 'from1' and 'from2', and assign to set 'to'.]

  Description []

  SideEffects [set 'to' is changed.]

******************************************************************************/
void
LtlSetOR(
  LtlSet_t *to,
  LtlSet_t *from1,
  LtlSet_t *from2)
{
  var_set_or(to->e, from1->e, from2->e);
}

/**Function********************************************************************

  Synopsis    [Clear all bits in the set.]

  Description []

  SideEffects [The set is changed.]

******************************************************************************/
void
LtlSetClear(
  LtlSet_t *set)
{
  var_set_clear(set->e);
}

/**Function********************************************************************

  Synopsis    [Set the bit indicated by 'index'.]

  Description []

  SideEffects [The set is changed.]

******************************************************************************/
void
LtlSetSetElt(
  LtlSet_t *set,
  int index)
{
  var_set_set_elt(set->e, index);
}

/**Function********************************************************************

  Synopsis    [Clear the bit indicated by 'index'.]

  Description []

  SideEffects [The set is changed.]

******************************************************************************/
void
LtlSetClearElt(
  LtlSet_t *set,
  int index)
{
  var_set_clear_elt(set->e, index);
}

/**Function********************************************************************

  Synopsis    [Return the value of the bit indicated by 'index'.]

  Description []

  SideEffects [The set is changed.]

******************************************************************************/
int
LtlSetGetElt(
  LtlSet_t *set,
  int index)
{
  return var_set_get_elt(set->e,index);
}

/**Function********************************************************************

  Synopsis    [Return 1 if the set is empty.]

  Description []

  SideEffects []

******************************************************************************/
int
LtlSetIsEmpty(
  LtlSet_t *set)
{
  return var_set_is_empty(set->e);
}

/**Function********************************************************************

  Synopsis    [Return the set in the list that matches the given set.]

  Description [Null will be return if there does not exist a match set.]

  SideEffects []

******************************************************************************/
LtlSet_t *
LtlSetIsInList(
  LtlSet_t *set,
  lsList list)
{
  lsGen gen;
  lsGeneric data;
  LtlSet_t *s = NIL(LtlSet_t);
  int flag = 0;
  
  lsForEachItem(list, gen, data) {
    s = (LtlSet_t *) data;
    if ( var_set_equal(s->e, set->e) ) {
      flag = 1;
      lsFinish(gen);
      break;
    }
  }
  
  return flag? s: NIL(LtlSet_t);
}
    
/**Function********************************************************************

  Synopsis    [Transform the given set to the label set and return it.]

  Description [The given set may contain all the 'elementary formulae'. Its
  table and negation are 'tableau->abTable' and 'tableau->abTableNegate'.
  
  The label set contain only the propositional formulae and their
  negations. Its table and negation array are 'labelTable' and 'labelNegate'.

  The above two table could have been the same, but we choose to implement
  them differently: Since labelTable might be smaller than abTable, it will
  make the boolean minimization based on it faster.]

  SideEffects [The result should be freed by the caller.]

******************************************************************************/
LtlSet_t *
LtlSetToLabelSet(
  LtlTableau_t *tableau,
  LtlSet_t *set)
{
  int i;
  LtlSet_t *vset = LtlSetNew(tableau->labelIndex);
  Ctlsp_Formula_t *F;
  
  for (i=0; i<tableau->abIndex; i++) {
    if (var_set_get_elt(set->e, i)) {
      F = tableau->abTable[i].F;
      if (Ctlsp_LtlFormulaIsPropositional(F)&&
	  Ctlsp_FormulaReadType(F) != Ctlsp_TRUE_c &&
	  Ctlsp_FormulaReadType(F) != Ctlsp_FALSE_c)
	var_set_set_elt(vset->e, 
			Ctlsp_FormulaReadLabelIndex(tableau->abTable[i].F));
    }
  }
  
  return vset;
}

/**Function********************************************************************

  Synopsis    [Print all the 'elementary formulae' contained in the set.]

  Description [Assume the set is based on the index table 'tableau->abTable'.]

  SideEffects []

******************************************************************************/
void
LtlSetPrint(
  LtlTableau_t *tableau,
  LtlSet_t *set)
{
  int i;
  
  fprintf(vis_stdout, "{ ");
  for (i=0; i<tableau->abIndex; i++) {
    if (LtlSetGetElt(set, i)) {
      Ctlsp_FormulaPrint(vis_stdout, tableau->abTable[i].F);
      fprintf(vis_stdout, "; ");
    }
  }
  fprintf(vis_stdout, " }");
}

/**Function********************************************************************

  Synopsis    [Print all index that are set in the set.]

  Description [The length of the set should be provided.]
  
  SideEffects []

******************************************************************************/
void
LtlSetPrintIndex(
  int length,
  LtlSet_t *set)
{
  int i;
  
  fprintf(vis_stdout, "{ ");
  for (i=0; i<length; i++) {
    if (LtlSetGetElt(set, i)) {
      fprintf(vis_stdout, " %d ", i);
    }
  }
  fprintf(vis_stdout, " }\n");
}


/**Function********************************************************************

  Synopsis    [Allocate the data struture for 'pair'.]

  Description []
  
  SideEffects []

******************************************************************************/
LtlPair_t *
LtlPairNew(
  char *First,
  char *Second)
{
  LtlPair_t *pair = ALLOC(LtlPair_t, 1);

  pair->First = First;
  pair->Second= Second;
  return pair;
}

/**Function********************************************************************

  Synopsis    [Free the LtlPair_t data struture.]

  Description []
  
  SideEffects []

******************************************************************************/
void
LtlPairFree(
  LtlPair_t *pair)
{
  FREE(pair);
}

/**Function********************************************************************

  Synopsis    [Return a hash key for the given pair.]

  Description [The key is based on the content. Thus two pair with the same
  content (not necessarily the same pointer) have the same hash key.]
  
  SideEffects []

******************************************************************************/
int
LtlPairHash(
  char *key,
  int modulus)
{
  LtlPair_t *pair = (LtlPair_t *) key;
  
  return (int) ((((unsigned long) pair->First >>2) +
		 ((unsigned long) pair->Second>>4)) % modulus);
}

/**Function********************************************************************

  Synopsis    [Return -1/0/+1 when the key1 is greater/equal/less than key2.]

  Description [For two keys with the same content, they are equal.]
  
  SideEffects []

******************************************************************************/
int 
LtlPairCompare(
  const char *key1,
  const char *key2)
{
  LtlPair_t *pair1 = (LtlPair_t *) key1;
  LtlPair_t *pair2 = (LtlPair_t *) key2;
  
  assert(key1 != NIL(char));
  assert(key2 != NIL(char));

  if ((pair1->First == pair2->First) && (pair1->Second == pair2->Second))
    return 0;
  else if (pair1->First >= pair2->First && pair1->Second >= pair2->Second)
    return 1;
  else
    return -1;
}

/**Function********************************************************************

  Synopsis    [Print the pair as index pair.]

  Description []
  
  SideEffects []

******************************************************************************/
void
LtlPairPrint(
  LtlPair_t *pair)
{
  vertex_t *first = (vertex_t *) pair->First;
  vertex_t *second= (vertex_t *) pair->Second;
  Ltl_AutomatonNode_t *node1 = (Ltl_AutomatonNode_t *) first->user_data;
  Ltl_AutomatonNode_t *node2 = (Ltl_AutomatonNode_t *) second->user_data;

  fprintf(vis_stdout, " (n%d, n%d) ", node1->index, node2->index);
}

/**Function********************************************************************

  Synopsis    [Print the cover as a set of index.]

  Description []
  
  SideEffects []

******************************************************************************/
void
LtlCoverPrintIndex(
  int length,
  lsList cover)
{
  int first = 1;
  lsGen gen;
  LtlSet_t *set;

  fprintf(vis_stdout, "{ ");
  lsForEachItem(cover, gen, set) {
    if (first)	  first = 0;
    else          	  fprintf(vis_stdout, " + ");
    LtlSetPrintIndex(length, set);
  }
  fprintf(vis_stdout, " }");
}


/**Function********************************************************************

  Synopsis    [Return the 'Complete Sum' of the cover by iterated consensus.]

  Description [The cover is represented by a list of sets (product terms).]
  
  SideEffects [The result should be freed by the caller. The given cover is
  NOT changed.]

******************************************************************************/
lsList 
LtlCoverCompleteSum(
  lsList Cover,
  array_t *Negate)
{
  lsList cs = lsCreate();
  lsGen lsgen;
  array_t *products = array_alloc(LtlSet_t *, 0);
  LtlSet_t *term, *term1, *term2, *consensus;
  long i, j, k, flag;
  st_table *removed, *consList;  /* removed, and consensus generated */
  
  /* Check and remove contraditory terms -- containing both F and !F */
  lsForEachItem(Cover, lsgen, term) {
    if (!LtlSetIsContradictory(term, Negate))
      array_insert_last(LtlSet_t *, products, term);
  }
  
  /* Sort terms by increasing number of literals */
  array_sort(products, LtlSetCompareCardinality);

  /* Check tautologous term */
  term = array_fetch(LtlSet_t *, products, 0);
  if (LtlSetCardinality(term) == 0) {
    lsNewEnd(cs, (lsGeneric) LtlSetCopy(term), (lsHandle *)0);
    array_free(products);
    return cs;
  }

  /* In the following, we won't change 'products'. Instead, if a term need to
   * be removed, we will store it (its index number) in the hash table
   */
  removed = st_init_table(st_ptrcmp, st_ptrhash);
  /* In the following, we might generate some new consensus terms, and we will
   * store them (LtlSet_t) in the list 
   */
  consList = st_init_table(st_ptrcmp, st_ptrhash);
  
  /* Check terms for single-cube containment. Rely on ordering for efficiency.
   * A term can only be contained by another term with fewer literals 
   */
  for (i=array_n(products)-1; i>0; i--) {
    term = array_fetch(LtlSet_t *, products, i);
    for (j=0; j<i; j++) {
      term1 = array_fetch(LtlSet_t *, products, j);
      if (LtlSetCardinality(term1) == LtlSetCardinality(term)) break;
      if (LtlSetInclude(term, term1)) {
	/* remember the removed term */
	st_insert(removed, (char *)i, (char *)i);
	break;
      }
    }
  }
  
  /* Now do iterated consensus */
  for (i=1; i<array_n(products); i++) {
    if (st_is_member(removed, (char *)i)) continue;
    term = array_fetch(LtlSet_t *, products, i);
      
    for (j=0; j<i; j++) {
      if (st_is_member(removed, (char *)j)) continue;	  
      term1 = array_fetch(LtlSet_t *, products, j);
      
      consensus = LtlSetConsensus(term, term1, Negate);
	  
      if (consensus) {
	/* should store consensus ? */
	flag = 1;  
	for(k=0; k<array_n(products); k++) {
	  if (st_is_member(removed, (char *)k)) continue;
	  term2 = array_fetch(LtlSet_t *, products, k);
	  
	  if (LtlSetInclude(consensus, term2)) {
	    /* redudant new term */
	    flag = 0;  
	    break;
	  } 
	  if (LtlSetInclude(term2, consensus)) {
	    /* remember the removed term2 (k)  */
	    st_insert(removed, (char *)k, (char *)k);
	  }
	}
	if (flag) {
	  array_insert_last(LtlSet_t *, products, consensus);
	  st_insert(consList, consensus, (char *)0);
	}else
	  LtlSetFree(consensus);
      }
    }
  }

#if 0
  if (0) {
    fprintf(vis_stdout, "\nLtlCompleteSum: products = {  ");
    for(i=0; i<array_n(products); i++) {
      term = array_fetch(LtlSet_t *, products, i);
      LtlSetPrintIndex(array_n(Negate), term);
    }
    fprintf(vis_stdout, "}\nLtlCompleteSum: removed = {  ");
    st_foreach_item(removed, stgen, &i, NIL(char *)) {
      term = array_fetch(LtlSet_t *, products, i);
      LtlSetPrintIndex(array_n(Negate), term);
    }
    fprintf(vis_stdout, "}\nLtlCompleteSum: consList = {  ");
    st_foreach_item(consList, stgen, &term, NIL(char *)) {
      LtlSetPrintIndex(array_n(Negate), term);
    }
    fprintf(vis_stdout, "}\n");
    
    fflush(vis_stdout);
  }
#endif      
  
  arrayForEachItem(LtlSet_t *, products, i, term) {
    if (!st_is_member(removed, (char *)i)) {
      /* put it into the complete sum list */
      if (!st_is_member(consList, term))
	term1 = LtlSetCopy(term);
      else
	term1 = term;
      lsNewEnd(cs, (lsGeneric) term1, NIL(lsHandle));
    }else {
      /* it has been removed. If it was allocated locally, free it */
      if (st_is_member(consList, term))
	LtlSetFree(term);
    }
  }

  array_free(products);
  st_free_table(removed);
  st_free_table(consList);

  return cs;
}


/**Function********************************************************************

  Synopsis    [Return the consensus of two given set (product terms).]

  Description [If the consesus does not exist, return a null pointer.]
  
  SideEffects [The result should be freed by the caller.]

******************************************************************************/
LtlSet_t *
LtlSetConsensus(
  LtlSet_t *first,
  LtlSet_t *second,
  array_t *Negate)
{
  LtlSet_t *consensus = LtlSetNew(array_n(Negate));
  int pivot = -1;
  int literal, complement;
  
  for (literal=0; literal<array_n(Negate); literal++) {
    if (LtlSetGetElt(first, literal)) {
      complement = array_fetch(int, Negate, literal);
      if (LtlSetGetElt(second, complement)) {
	if (pivot != -1) {
	  LtlSetFree(consensus);
	  return NIL(LtlSet_t);
	}else {
	  pivot = complement;
	}
      }else {
	LtlSetSetElt(consensus, literal);
      }
    }
  }
  /* if pivot has never been defined, return NIL */
  if (pivot == -1) {
    LtlSetFree(consensus);
    return NIL(LtlSet_t);
  }

  for (literal=0; literal<array_n(Negate); literal++) {
    if (LtlSetGetElt(second, literal)) {
      if (literal != pivot)
	LtlSetSetElt(consensus, literal);
    }
  }

  return consensus;
}

/**Function********************************************************************

  Synopsis    [Return the cofactor of the cover with respect to the set.]

  Description [We need the Negate method for each item in the set.]
  
  SideEffects [The result need to be freed by the caller. The input is left
  unchanged.]

******************************************************************************/
lsList
LtlCoverCofactor(
  lsList Cover,
  LtlSet_t *c,
  array_t *Negate)
{
  lsList cofactor = lsCopy(Cover, (lsGeneric (*)(lsGeneric))LtlSetCopy);
  lsList list;
  lsGen  lsgen;
  st_table *removed = st_init_table(st_ptrcmp, st_ptrhash);
  int literal, complement;
  LtlSet_t *term;
  
  for (literal=0; literal<array_n(Negate); literal++) {
    if (!LtlSetGetElt(c, literal))  continue;
    complement = array_fetch(int, Negate, literal);
    lsForEachItem(cofactor, lsgen, term) {
      if (st_is_member(removed, term)) continue;
      if (LtlSetGetElt(term, complement)) 
	st_insert(removed, term, term);
      else if (LtlSetGetElt(term, literal))
	LtlSetClearElt(term, literal);
    }
  }

  list = cofactor;
  cofactor = lsCreate();
  lsForEachItem(list, lsgen, term) {
    if (st_is_member(removed, term)) 
      LtlSetFree(term);
    else
      lsNewEnd(cofactor, (lsGeneric) term, (lsHandle *) 0);
  }
  lsDestroy(list, (void (*)(lsGeneric))0);

  st_free_table(removed);

  return cofactor;
}
      
/**Function********************************************************************

  Synopsis    [Return 1 if the given cover is tautology.]

  Description [The test is not fast: the compute sum of the cover should be
  computed.]
  
  SideEffects []

******************************************************************************/
int
LtlCoverIsTautology(
  lsList Cover,
  array_t *Negate)
{
  lsList complete = LtlCoverCompleteSum(Cover, Negate);
  LtlSet_t *term;
  int result;

  if (lsLength(complete) !=1)
    result = 0;
  else {
    lsFirstItem(complete, &term, (lsHandle *)0);
    result = (LtlSetCardinality(term) == 0);
  }

  lsDestroy(complete, (void (*)(lsGeneric))LtlSetFree);
  return result;
}

/**Function********************************************************************

  Synopsis    [Return 1 if the given cover is implied BY the set.]

  Description []
  
  SideEffects []

******************************************************************************/
int
LtlCoverIsImpliedBy(
  lsList Cover,
  LtlSet_t *term,
  array_t *Negate)
{
  lsList cofactor = LtlCoverCofactor(Cover, term, Negate);
  int result = LtlCoverIsTautology(Cover, Negate);
  lsDestroy(cofactor, (void (*)(lsGeneric))LtlSetFree);
  
  return result;
}
    

/**Function********************************************************************

  Synopsis    [Boolean minimization of the given cover.]

  Description [First, compute a prime and irredundant version of the Cover;
  Then try to drop each item iff it is implied by the remaining items.
  
  Notice: there might be a bug in the algorithm. Need to be fixed.
  Need to talke to Fabio/Roderick
  ]
  
  SideEffects []

******************************************************************************/
lsList
LtlCoverPrimeAndIrredundant(
  LtlTableau_t *tableau,
  lsList Cover,
  array_t *Negate)
{
  lsList pai = LtlCoverCompleteSum(Cover, Negate);
  int totalnum;   /* total num of terms in current lsList pai */
  int procnum;    /* how many are already processed so far ? */
  LtlSet_t *term;
  
  totalnum = lsLength(pai);
  procnum = 0;
  /* Try to drop each term in turn */
  while(lsDelBegin(pai, &term) != LS_NOMORE) {
    if ( (lsLength(pai) != 0) &&
	 /* !LtlAutomatonSetIsFair(tableau, term) && */
	 LtlCoverIsImpliedBy(pai, term, Negate) ) {
      LtlSetFree(term);
      totalnum--;
    }else 
      lsNewEnd(pai, (lsGeneric) term, (lsHandle *)0);
    
    procnum++;
    if (procnum >= totalnum)
      break;
  }
  
  return pai;
}


/**Function********************************************************************

  Synopsis    [Return the supercube of a cover.]

  Description []
  
  SideEffects [The result should be freed by the caller.]

******************************************************************************/
LtlSet_t *
LtlCoverGetSuperCube(
  lsList Cover,
  array_t *Negate)
{
  LtlSet_t *unate = LtlSetNew(array_n(Negate));
  LtlSet_t *binate = LtlSetNew(array_n(Negate));
  lsGen  lsgen;
  LtlSet_t *term;
  int literal, neg;

  lsForEachItem( Cover, lsgen, term ) {
    for (literal=0; literal<array_n(Negate); literal++) {
      if (!LtlSetGetElt(term, literal))  continue;
      if (LtlSetGetElt(binate, literal) || LtlSetGetElt(unate, literal))
	continue;
      neg = array_fetch(int, Negate, literal);
      if (LtlSetGetElt(unate, neg)) {
	LtlSetClearElt(unate, neg);
	LtlSetSetElt(binate, literal);
	LtlSetSetElt(binate, neg);
      }else
	LtlSetSetElt(unate, literal);
    }
  }

  LtlSetFree(binate);
  
  return unate;
}



/**Function********************************************************************

  Synopsis    [Return the supercube of a cover.]

  Description []
  
  SideEffects [The result should be freed by the caller.]

******************************************************************************/
mdd_t *
LtlSetModelCheckFormulae(
  LtlSet_t *set,
  array_t *labelTable,
  Fsm_Fsm_t *fsm)
{
  mdd_t *minterm, *mdd1, *mdd2;
  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
  mdd_t *mddOne = mdd_one(mddManager);
  array_t *careStatesArray = array_alloc(mdd_t *, 0);
  int i;

  array_insert(mdd_t *, careStatesArray, 0, mddOne);

  minterm = mdd_dup(mddOne);
  for (i=0; i<array_n(labelTable); i++) {
    if (LtlSetGetElt(set, i)) {
      Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *, labelTable, i);
      Ctlp_Formula_t *ctlF = Ctlsp_PropositionalFormulaToCTL(F);
      mdd1 = Mc_FsmEvaluateFormula(fsm, ctlF, mddOne, 
				   NIL(Fsm_Fairness_t),
				   careStatesArray, 
				   MC_NO_EARLY_TERMINATION,
				   NIL(Fsm_HintsArray_t), Mc_None_c,
				   McVerbosityNone_c, McDcLevelNone_c, 0,
				   McGSH_EL_c);
      mdd2 = minterm;
      minterm = mdd_and(minterm, mdd1, 1, 1);
      mdd_free(mdd2);
      mdd_free(mdd1);
      Ctlp_FormulaFree(ctlF);
    }
  }

  mdd_array_free(careStatesArray);

  return minterm;
}