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

File  : che_hcbadmin.c

Author: Stephan Schulz

Contents
 
  Functions for administrating sets of predefined HCBs.

  Copyright 1998, 1999 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

<1> Wed Dec  9 02:44:26 MET 1998
    New

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

#include "che_hcbadmin.h"



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



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


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


/*-----------------------------------------------------------------------
//
// Function: parse_single_wfcb_item()
//
//   Parse a single wfcb-item "name(steps)" and insert it into the
//   HCB.
//
// Global Variables: -
//
// Side Effects    : Input, changes HCB (of course)
//
/----------------------------------------------------------------------*/

static void parse_single_wfcb_item(HCB_p hcb, Scanner_p in,
				   WFCBAdmin_p wfcbs, OCB_p ocb,
				   ProofState_p state)
{
   WFCB_p wfcb;
   long   steps;
   char   *name;

   steps = AktToken(in)->numval;
   if(steps<=0)
   {
      AktTokenError(in, 
		    "Value >0 expected in heuristic evaluation"
		    " function description",
		    false);
   }
   AcceptInpTok(in, PosInt);
   AcceptInpTok(in, Mult|Fullstop);
   
   CheckInpTok(in, Identifier);

   if(TestTok(LookToken(in,1), OpenBracket|EqualSign))
   {
      name = WeightFunDefParse(wfcbs, in, ocb, state);
      wfcb = WFCBAdminFindWFCB(wfcbs, name);
   }
   else
   {
      name = DStrView(AktToken(in)->literal);
      wfcb = WFCBAdminFindWFCB(wfcbs, name);
      NextToken(in);
   }
   if(!wfcb)
   {
      AktTokenError(in, "Not a valid evaluation function specifier",
		    false);
   } 
   HCBAddWFCB(hcb, wfcb, steps);
}


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

/*-----------------------------------------------------------------------
//
// Function: HCBAdminAlloc()
//
//   Allocate an empty initialized HCBAdminCell.
//
// Global Variables: -
//
// Side Effects    : Memory operations
//
/----------------------------------------------------------------------*/

HCBAdmin_p HCBAdminAlloc(void)
{
   HCBAdmin_p handle = HCBAdminCellAlloc();

   handle->names   = PStackAlloc();
   handle->hcb_set = PStackAlloc();

   return handle;
}


/*-----------------------------------------------------------------------
//
// Function: HCBAdminFree()
//
//   Free a HCBAdminCell. Will also free stored hcb's and names.
//
// Global Variables: -
//
// Side Effects    : Memory operations.
//
/----------------------------------------------------------------------*/

void HCBAdminFree(HCBAdmin_p junk)
{
   char* name;

   assert(junk);
   assert(junk->names);
   assert(junk->hcb_set);
   
   while(!PStackEmpty(junk->names))
   {
      name = PStackPopP(junk->names);
      FREE(name);      
   }
   PStackFree(junk->names);
   
   while(!PStackEmpty(junk->hcb_set))
   {
      HCBFree(PStackPopP(junk->hcb_set));      
   }
   PStackFree(junk->hcb_set);

   HCBAdminCellFree(junk);
}


/*-----------------------------------------------------------------------
//
// Function: HCBAdminAddHCB()
//
//   Add a HCB under a given name to the HCB-Set. Return index.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

long HCBAdminAddHCB(HCBAdmin_p set, char* name, HCB_p hcb)
{
   assert(set);
   assert(set->names);
   assert(set->hcb_set);
   assert(name);
   assert(hcb);

   VERBOSE2(fprintf(stderr, "%s: Adding heuristic '%s'.\n",
		   ProgName, name););
   PStackPushP(set->names, SecureStrdup(name));
   PStackPushP(set->hcb_set, hcb);

   return PStackGetSP(set->hcb_set)-1;
}


/*-----------------------------------------------------------------------
//
// Function: HCBAdminFindHCB()
//
//   Given a name and a HCB-Set, return the matching HCB (or
//   NULL). Always returns the last HCB with the same name, so you
//   can redefine predefined heuristics!
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

HCB_p HCBAdminFindHCB(HCBAdmin_p set, char* name)
{
   PStackPointer i;
   HCB_p res = NULL;
   
   assert(set);
   assert(set->names);
   assert(set->hcb_set);
   assert(name);
   

   for(i = PStackGetSP(set->names)-1; i>=0; i--)
   {
      if(strcmp(name, PStackElementP(set->names, i))==0)
      {
	 res = PStackElementP(set->hcb_set, i);
	 break;
      }
   }
   return res;
}


/*-----------------------------------------------------------------------
//
// Function: HeuristicParse()
//
//   Parse a heuristic.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

HCB_p HeuristicParse(Scanner_p in, WFCBAdmin_p wfcbs, OCB_p ocb,
		     ProofState_p state)
{
   HCB_p  hcb = HCBAlloc();

   AcceptInpTok(in, OpenBracket);
   
   parse_single_wfcb_item(hcb, in, wfcbs, ocb, state);

   while(TestInpTok(in, Comma))
   {
      AcceptInpTok(in, Comma);   
      parse_single_wfcb_item(hcb, in, wfcbs, ocb, state);
   }
   AcceptInpTok(in, CloseBracket);   
   return hcb;
}


/*-----------------------------------------------------------------------
//
// Function: HeuristicDefParse()
//
//   Parse a heuristics definition and add it to the set.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

long HeuristicDefParse(HCBAdmin_p set, Scanner_p in, WFCBAdmin_p
		       wfcbs, OCB_p ocb, ProofState_p state)
{
   char* name;
   HCB_p hcb;
   long   res;
   
   if(TestInpTok(in, OpenBracket))
   {
      name = SecureStrdup("Default");
   }
   else
   {
      CheckInpTok(in, Identifier);
      name = SecureStrdup(DStrView(AktToken(in)->literal)); 
      /* All this strdup'ing is inefficient, but uncritical */
      NextToken(in);
      AcceptInpTok(in, EqualSign);
   }
   hcb = HeuristicParse(in, wfcbs, ocb, state);
   res = HCBAdminAddHCB(set, name, hcb);
   FREE(name);
   
   return res;   
}


/*-----------------------------------------------------------------------
//
// Function: HeuristicDefListParse()
//
//   Parse a list of heuristics_definitions definitions.
//
// Global Variables: -
//
// Side Effects    : -
//
/----------------------------------------------------------------------*/

long HeuristicDefListParse(HCBAdmin_p set, Scanner_p in, WFCBAdmin_p
			   wfcbs, OCB_p ocb, ProofState_p state)
{
   long res = PStackGetSP(set->names);

   while((TestInpTok(in, Identifier)&&TestTok(LookToken(in,1), EqualSign))
	 ||TestInpTok(in, OpenBracket))
   {
      res = HeuristicDefParse(set, in, wfcbs, ocb, state);
   }
   return res;
}




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