/*-----------------------------------------------------------------------

  File  : che_to_precgen.c

  Author: Stephan Schulz

  Contents

  Functions implementing several precedence generation schemes for
  term orderings.

  Copyright 1998-2020 by the author.
  This code is released under the GNU General Public Licence and
  the GNU Lesser General Public License.
  See the file COPYING in the main E directory for details..
  Run "eprover -h" for contact information.

  Changes

  Created: Fri Sep 25 02:49:11 MET DST 1998

  -----------------------------------------------------------------------*/

#include "che_to_precgen.h"



/*---------------------------------------------------------------------*/
/*                        Global Variables                             */
/*---------------------------------------------------------------------*/

/*---------------------------------------------------------------------*/
/*                      Forward Declarations                           */
/*---------------------------------------------------------------------*/

/*---------------------------------------------------------------------*/
/*                         Internal Functions                          */
/*---------------------------------------------------------------------*/

/* #define PRINT_PRECEDENCE */

#ifdef PRINT_PRECEDENCE
/*-----------------------------------------------------------------------
//
// Function: print_prec_array()
//
//   Print the precedence described by the array. Hacked to enable
//   Waldmeister to use the same orderings as generated by E.
//
// Global Variables: -
//
// Side Effects    : Output
//
/----------------------------------------------------------------------*/

void print_prec_array(FILE* out, Sig_p sig, FCodeFeatureArray_p array)
{
   FunCode i;
   char *del = "";

   fprintf(out, "# Ordering precedence: ");
   for(i = sig->f_count; i > 0; i--)
   {
      if(!SigIsSpecial(sig, array->array[i].symbol))
      {
         fprintf(out, "%s%s", del, SigFindName(sig,array->array[i].symbol));
         del = " > ";
      }
   }
   fprintf(out, "\n");
}
#endif


/*-----------------------------------------------------------------------
//
// Function: compute_precedence_from_array()
//
//   Given an ocb and a sorted array of type featuresortcell[], set
//   the precedence in the ocb.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

static void compute_precedence_from_array(OCB_p ocb, FCodeFeatureArray_p
                                          array)
{
   FunCode i, last;

   assert(ocb->sig_size == array->size-1);
   if(ocb->prec_weights)
   {
      for(i = SIG_TRUE_CODE+1; i<=ocb->sig_size; i++)
      {
         if((SigFindArity(ocb->sig, i)==0) &&
            !SigIsPredicate(ocb->sig, i) &&
            !SigQueryFuncProp(ocb->sig, i, FPSpecial))
         {
            OCBCondSetMinConst(ocb, SigGetType(ocb->sig, i), i);
         }
         ocb->prec_weights[array->array[i].symbol] = i;
      }
      ocb->prec_weights[SIG_TRUE_CODE] = (LONG_MIN/2);
   }
   else
   {
      last = SIG_TRUE_CODE;
      for(i = SIG_TRUE_CODE+1; i<=ocb->sig_size; i++)
      {
         OCBPrecedenceAddTuple(ocb, last, array->array[i].symbol, to_lesser);
         last = array->array[i].symbol;
      }
   }
#ifdef PRINT_PRECEDENCE
   print_prec_array(GlobalOut, ocb->sig, array);
#endif
}



/*-----------------------------------------------------------------------
//
// Function: generate_unary_first_precedence()
//
//   Generate a precence in which symbols with higher arity are
//   larger, but unary symbols are larger still. Order of occurence in
//   the signature is used as a tie-breaker.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_unary_first_precedence(OCB_p ocb,
                                            FCodeFeatureArray_p array,
                                            ClauseSet_p axioms)
{
   FunCode i;
   long    arity;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      arity = SigFindArity(ocb->sig, i);
      if(arity == 1)
      {
         array->array[i].key1 = INT_MAX;
      }
      else
      {
         array->array[i].key1 = arity;
      }
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}


/*-----------------------------------------------------------------------
//
// Function: generate_unary_first_freq_precedence()
//
//   Generate a precence in which rarer symbols are
//   larger, but unary symbols are larger still (and constants are
//   minimal).
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_unary_first_freq_precedence(OCB_p ocb,
                                                 FCodeFeatureArray_p array,
                                                 ClauseSet_p axioms)
{
   FunCode i;
   long    arity;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      arity = SigFindArity(ocb->sig, i);
      if(arity == 1)
      {
         array->array[i].key1 = 2;
      }
      else if(arity == 0)
      {
         array->array[i].key1 = 0;
      }
      else
      {
         array->array[i].key1 = 1;
      }
      array->array[i].key2 = array->array[i].freq;
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}


/*-----------------------------------------------------------------------
//
// Function: generate_arity_precedence()
//
//   Generate a precende in which symbols with higher arity are
//   larger. Order of occurence in the signature is used as a
//   tie-breaker.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_arity_precedence(OCB_p ocb,
                                      FCodeFeatureArray_p array,
                                      ClauseSet_p axioms)
{
   FunCode i;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      array->array[i].key1 = SigFindArity(ocb->sig, i);
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}


/*-----------------------------------------------------------------------
//
// Function: generate_invarity_precedence()
//
//   Generate a precende in which symbols with higher arity are
//   smaller. Order of occurence in the signature is used as a
//   tie-breaker.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_invarity_precedence(OCB_p ocb,
                                         FCodeFeatureArray_p array,
                                         ClauseSet_p axioms)
{
   FunCode i;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      array->array[i].key1 = -SigFindArity(ocb->sig, i);
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}


/*-----------------------------------------------------------------------
//
// Function: generate_const_max_precedence()
//
//   Generate a precedence in which symbols with higher arity are
//   larger, but constants are the largest symbols. Order of occurence
//   in the signature is used as a tie-breaker.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_const_max_precedence(OCB_p ocb,
                                          FCodeFeatureArray_p array,
                                          ClauseSet_p axioms)
{
   FunCode i;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      array->array[i].key1 = SigFindArity(ocb->sig, i);
      if(!array->array[i].key1)
      {
         array->array[i].key1 = INT_MAX;
      }
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}


/*-----------------------------------------------------------------------
//
// Function: generate_const_min_precedence()
//
//   Generate a precedence in which symbols with higher arity are
//   smaller, but constants are the smallest symbols. Order of
//   occurence in the signature is used as a tie-breaker.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_const_min_precedence(OCB_p ocb,
                                          FCodeFeatureArray_p array,
                                          ClauseSet_p axioms)
{
   FunCode i;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      array->array[i].key1 = -SigFindArity(ocb->sig, i);
      if(!array->array[i].key1)
      {
         array->array[i].key1 = -FREQ_SEMI_INFTY;
      }
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}



/*-----------------------------------------------------------------------
//
// Function: generate_freq_precedence()
//
//   Generate a precedence in which symbols which occur more often in
//   the specification are bigger. Arity is used as a tie-breaker,
//   then order of occurence in the signature.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_freq_precedence(OCB_p ocb,
                                            FCodeFeatureArray_p array,
                                     ClauseSet_p axioms)
{
   FunCode       i;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      array->array[i].key1 = array->array[i].freq;
      array->array[i].key2 = SigFindArity(ocb->sig, i);
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}


#ifdef ENABLE_LFHO

/*-----------------------------------------------------------------------
//
// Function: generate_type_freq_precedence()
//
//   Generate a precedence in which symbols whose types occur more often in
//   the specification are bigger. Occurrence of symbol is used as a tie-breaker,
//   then order of occurence in the signature.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_type_freq_precedence(OCB_p ocb,
                                          FCodeFeatureArray_p array,
                                          ClauseSet_p axioms)
{
   FunCode       i;

   long max_types = ocb->sig->type_bank->types_count+1;
   long* type_counts = SizeMalloc(max_types*sizeof(long));
   for(long i=0; i<max_types; i++)
   {
      type_counts[i] = 0;
   }

   ClauseSetAddTypeDistribution(axioms, type_counts);

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      long sym_type_id = SigGetType(ocb->sig, i) ? SigGetType(ocb->sig, i)->type_uid : 0;
      array->array[i].key1 = type_counts[sym_type_id];
      array->array[i].key2 = array->array[i].freq;
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);

   SizeFree(type_counts, max_types*sizeof(long));
}


/*-----------------------------------------------------------------------
//
// Function: generate_comb_freq_precedence()
//
//   Generate a precedence in which symbols whose types occur more often in
//   the specification are bigger. Furthemore, add the occurence of symbol to
//   this value. Occurrence of symbol is used as a tie-breaker,
//   then order of occurence in the signature.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_comb_freq_precedence(OCB_p ocb,
                                          FCodeFeatureArray_p array,
                                          ClauseSet_p axioms)
{
   FunCode       i;

   long max_types =  ocb->sig->type_bank->types_count +1;
   long* type_counts = SizeMalloc(max_types*sizeof(long));
   for(long i=0; i<max_types; i++)
   {
      type_counts[i] = 0;
   }

   ClauseSetAddTypeDistribution(axioms, type_counts);

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      long sym_type_id = SigGetType(ocb->sig, i) ? SigGetType(ocb->sig, i)->type_uid : 0;
      array->array[i].key1 = type_counts[sym_type_id] + 2*array->array[i].freq;
      array->array[i].key2 = array->array[i].freq;
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);

   SizeFree(type_counts, max_types*sizeof(long));
}
#endif

/*-----------------------------------------------------------------------
//
// Function: generate_invfreq_precedence()
//
//   Generate a precedence in which symbols which occur more often in
//   the specification are smaller. Arity is used as a tie-breaker,
//   then order of occurence in the signature. .
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_invfreq_precedence(OCB_p ocb,
                                        FCodeFeatureArray_p array,
                                        ClauseSet_p axioms)
{
   FunCode       i;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      array->array[i].key1 = -array->array[i].freq;
      array->array[i].key2 = SigFindArity(ocb->sig, i);
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}


#ifdef ENABLE_LFHO

/*-----------------------------------------------------------------------
//
// Function: generate_inv_type_freq_precedence()
//
//   Generate a precedence in which symbols whose types occur more often in
//   the specification are smaller. Occurrence of symbol is used as a tie-breaker,
//   then order of occurence in the signature.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_inv_type_freq_precedence(OCB_p ocb,
                                              FCodeFeatureArray_p array,
                                              ClauseSet_p axioms)
{
   FunCode       i;

   long max_types = ocb->sig->type_bank->types_count+1;

   long* type_counts = SizeMalloc(max_types*sizeof(long));
   for(long i=0; i<max_types; i++)
   {
      type_counts[i] = 0;
   }

   ClauseSetAddTypeDistribution(axioms, type_counts);

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      long sym_type_id = SigGetType(ocb->sig, i) ? SigGetType(ocb->sig, i)->type_uid : 0;
      array->array[i].key1 = -type_counts[sym_type_id];
      array->array[i].key2 = array->array[i].freq;
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);

   SizeFree(type_counts, max_types*sizeof(long));
}

/*-----------------------------------------------------------------------
//
// Function: generate_inv_comb_freq_precedence()
//
//   Generate a precedence in which symbols whose types occur more often
//   and that occur often themselves in
//   the specification are smaller. Occurrence of symbol is used as a tie-breaker,
//   then order of occurence in the signature.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_inv_comb_freq_precedence(OCB_p ocb,
                                              FCodeFeatureArray_p array,
                                              ClauseSet_p axioms)
{
   FunCode       i;

   long max_types =  ocb->sig->type_bank->types_count+1;
   long* type_counts = SizeMalloc(max_types*sizeof(long));
   for(long i=0; i<max_types; i++)
   {
      type_counts[i] = 0;
   }

   ClauseSetAddTypeDistribution(axioms, type_counts);

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      long sym_type_id = SigGetType(ocb->sig, i) ? SigGetType(ocb->sig, i)->type_uid : 0;
      array->array[i].key1 = -(type_counts[sym_type_id] + 2*array->array[i].freq);
      array->array[i].key2 = array->array[i].freq;
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);

   SizeFree(type_counts, max_types*sizeof(long));
}

#endif

/*-----------------------------------------------------------------------
//
// Function: generate_invconjfreq_precedence()
//
//   Generate a precedence in which symbols which occur in conjectures
//   are larger, ordered by inverse frequency in conjectures. Ties are
//   broken by inverse overall frequency. Arity is used as a
//   tie-breaker, then order of occurence in the signature. .
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_invconjfreq_precedence(OCB_p ocb,
                                            FCodeFeatureArray_p array,
                                            ClauseSet_p axioms)
{
   FunCode       i;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      array->array[i].key1 = array->array[i].conjfreq?
         (INT_MAX-array->array[i].conjfreq):0;
      array->array[i].key2 = -array->array[i].freq;
      array->array[i].key3 = SigFindArity(ocb->sig, i);
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}


/*-----------------------------------------------------------------------
//
// Function: generate_invfreq_conjmax_precedence()
//
//   Generate a precedence in which conjecture symbols are larger than
//   other symbols. Inverse frequency is used within the classes,
//   arity is used as a tie-breaker, then order of occurence in the
//   signature.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_invfreq_conjmax_precedence(OCB_p ocb,
                                                FCodeFeatureArray_p array,
                                                ClauseSet_p axioms)
{
   FunCode       i;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      array->array[i].key1 = array->array[i].conjfreq?1:0;
      array->array[i].key2 = -array->array[i].freq;
      array->array[i].key3 = SigFindArity(ocb->sig, i);
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}

/*-----------------------------------------------------------------------
//
// Function: generate_invfreq_conjmin_precedence()
//
//   Generate a precedence in which conjecture symbols are larger than
//   other symbols. Inverse frequency is used within the classes,
//   arity is used as a tie-breaker, then order of occurence in the
//   signature.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_invfreq_conjmin_precedence(OCB_p ocb,
                                                FCodeFeatureArray_p array,
                                                ClauseSet_p axioms)
{
   FunCode       i;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      array->array[i].key1 = array->array[i].conjfreq?0:1;
      array->array[i].key2 = -array->array[i].freq;
      array->array[i].key3 = SigFindArity(ocb->sig, i);
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}


/*-----------------------------------------------------------------------
//
// Function: generate_invfreq_constmin_precedence()
//
//   Generate a precedence in which symbols which occur more often in
//   the specification are smaller, but constants are smaller
//   still. Arity is used as an additional tie-breaker, then order of
//   occurence in the signature.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_invfreq_constmin_precedence(OCB_p ocb,
                                            FCodeFeatureArray_p array,
                                                 ClauseSet_p axioms)
{
   FunCode       i;
   int arity;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      arity = SigFindArity(ocb->sig, i);
      if(arity == 0)
      {
         array->array[i].key1 = -FREQ_SEMI_INFTY;
         array->array[i].key2 = array->array[i].freq;
      }
      else
      {
         array->array[i].key1 = -array->array[i].freq;
         array->array[i].key2 = SigFindArity(ocb->sig, i);
      }
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}


/*-----------------------------------------------------------------------
//
// Function: generate_invfreq_hack_precedence()
//
//   Generate a precedence in which symbols which occur more often in
//   the specification are smaller, but constants are smaller
//   still. All unary function symbols that occur with the maximal
//   frequency are largest. Arity is used as an additional
//   tie-breaker, then order of occurence in the signature.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_invfreq_hack_precedence(OCB_p ocb,
                                             FCodeFeatureArray_p array,
                                             ClauseSet_p axioms)
{
   FunCode       i;
   int arity, max_freq=-1;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      arity = SigFindArity(ocb->sig, i);
      if(arity == 1)
      {
         max_freq = MAX(max_freq, array->array[i].freq);
      }
   }
   for(i=1; i<= ocb->sig->f_count; i++)
   {
      arity = SigFindArity(ocb->sig, i);
      if(arity == 0)
      {
         array->array[i].key1 = -FREQ_SEMI_INFTY;
         array->array[i].key2 = -array->array[i].freq;
      }
      else if((arity == 1) && (array->array[i].freq == max_freq))
      {
         array->array[i].key1 = FREQ_SEMI_INFTY;
         array->array[i].key2 = 0;
      }
      else
      {
         array->array[i].key1 = -array->array[i].freq;
         array->array[i].key2 = SigFindArity(ocb->sig, i);
      }
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}



/*-----------------------------------------------------------------------
//
// Function: generate_arrayopt_precedence()
//
//   Generate a precedence for array problems with store > select >
//   a* > e* > whatever > i*.
//
//   Inverse frequency is the tie breaker.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

static void generate_arrayopt_precedence(OCB_p ocb,
                                         FCodeFeatureArray_p array,
                                         ClauseSet_p axioms)
{
   FunCode       i;
   char* id;

   for(i=1; i<= ocb->sig->f_count; i++)
   {
      id = SigFindName(ocb->sig, i);
      if(strcmp(id, "store") == 0)
      {
         array->array[i].key1 = 30;
      }
      else if(strcmp(id, "select") == 0)
      {
         array->array[i].key1 = 25;
      }
      else if(strcmp(id, "sk") == 0)
      {
         array->array[i].key1 = 20;
      }
      else if((strncmp(id, "a_",2) == 0) || (strncmp(id, "b_",2) == 0))
      {
         array->array[i].key1 = 10;
      }
      else if((strncmp(id, "a",1) == 0) || (strncmp(id, "b",1) == 0))
      {
         array->array[i].key1 = 15;
      }
      else if(strncmp(id, "e_",2) == 0)
      {
         array->array[i].key1 = 5;
      }
      else if(strncmp(id, "e",1) == 0)
      {
         array->array[i].key1 = 7;
      }
      else if(strncmp(id, "i_",2) == 0)
      {
         array->array[i].key1 = 0;
      }
      else if(strncmp(id, "i",1) == 0)
      {
         array->array[i].key1 = 2;
      }
      else
      {
         array->array[i].key1 = 5;
      }
      array->array[i].key2 = -array->array[i].freq;
   }
   FCodeFeatureArraySort(array);
   compute_precedence_from_array(ocb, array);
}





/*---------------------------------------------------------------------*/
/*                         Exported Functions                          */
/*---------------------------------------------------------------------*/



/*-----------------------------------------------------------------------
//
// Function: TOTranslatePrecGenMethod()
//
//   Given a string, return the corresponding TOPrecGenMethod
//   token.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

TOPrecGenMethod TOTranslatePrecGenMethod(char* name)
{
   TOPrecGenMethod method;

   method = StringIndex(name, TOPrecGenNames);

   if(method == -1)
   {
      method = PNoMethod;
   }
   return method;
}


/*-----------------------------------------------------------------------
//
// Function: TOGeneratePrecedence()
//
//   Given a pre-initialized OCB, compute a good precedence for a term
//   ordering.
//
// Global Variables: -
//
// Side Effects    : Sets weights in ocb.
//
/----------------------------------------------------------------------*/

void TOGeneratePrecedence(OCB_p ocb, ClauseSet_p axioms,
                          char* predefined, OrderParms_p oparms)
{
   FCodeFeatureArray_p array = FCodeFeatureArrayAlloc(ocb->sig, axioms);
   FCodeFeatureArrayUpdateOccKey(array, oparms);
   FCodeFeatureArrayUpdateSymbKey(array, ocb->sig, oparms);
   assert(ocb);
   assert(ocb->precedence||ocb->prec_weights);
   assert(ocb->sig);

   if(predefined)
   {
      Scanner_p in = CreateScanner(StreamTypeUserString, predefined,
                                   true, NULL, true);

      TOPrecedenceParse(in, ocb);

      DestroyScanner(in);
   }

   VERBOUTARG("Generating ordering precedence with ",
              TOPrecGenNames[oparms->to_prec_gen]);
   switch(oparms->to_prec_gen)
   {
   case POrientAxioms:
         Error("Not yet implemented", OTHER_ERROR);
         break;
   case PNoMethod:
         if(predefined) /* User should know what he does now! */
         {
            break;
         } /* else: Fall through */
         VERBOUT("Fall-through to unary_first\n");
   case PUnaryFirst:
         generate_unary_first_precedence(ocb, array, axioms);
         break;
   case PUnaryFirstFreq:
         generate_unary_first_freq_precedence(ocb, array, axioms);
         break;
   case PArity:
         generate_arity_precedence(ocb, array, axioms);
         break;
   case PInvArity:
         generate_invarity_precedence(ocb, array, axioms);
         break;
   case PConstMax:
         generate_const_max_precedence(ocb, array, axioms);
         break;
   case PInvArConstMin:
         generate_const_min_precedence(ocb, array, axioms);
         break;
   case PByFrequency:
         generate_freq_precedence(ocb, array, axioms);
         break;
   case PByInvFrequency:
         generate_invfreq_precedence(ocb, array, axioms);
         break;
   case PByInvConjFrequency:
         generate_invconjfreq_precedence(ocb, array, axioms);
         break;
   case PByInvFreqConjMax:
         generate_invfreq_conjmax_precedence(ocb, array, axioms);
         break;
   case PByInvFreqConjMin:
         generate_invfreq_conjmin_precedence(ocb, array, axioms);
         break;
   case PByInvFreqConstMin:
         generate_invfreq_constmin_precedence(ocb, array, axioms);
         break;
   case PByInvFreqHack:
         generate_invfreq_hack_precedence(ocb, array, axioms);
         break;
#ifdef ENABLE_LFHO
   case PByTypeFreq:
         generate_type_freq_precedence(ocb, array, axioms);
         break;
   case PByInvTypeFreq:
         generate_inv_type_freq_precedence(ocb, array, axioms);
         break;
   case PByCombFreq:
         generate_comb_freq_precedence(ocb, array, axioms);
         break;
   case PByInvCombFreq:
         generate_inv_comb_freq_precedence(ocb, array, axioms);
         break;

#endif
   case PArrayOpt:
         generate_arrayopt_precedence(ocb, array, axioms);
         break;
   default:
         assert(false && "Precedence generation method unimplemented");
         break;
   }
   FCodeFeatureArrayFree(array);
}


/*---------------------------------------------------------------------*/
/*                        End of File                                  */
/*---------------------------------------------------------------------*/