Class RewriteCache

To make it easy for the users to implement their own external indices, two sample external index implementation are provided. The first is the class RewriteCache defined in the library file <AD/rewrite/cache.h>.

The class RewriteCache implements a simple fixed capacity cache with the following member functions.

   RewriteCache();
   RewriteCache(int capacity);
  ~RewriteCache();

   void clear();                   // after rewriting
   void initialize();              // before rewriting
   void initialize(int capacity);  // before rewriting/also set capacity

   int capacity() const;

   void set_state(const void * t, int s);
   int get_state(const void * t) const;

   void invalidate(const void * t);

The user should call the function initialize before rewriting in order to setup the cache and/or clear out previously cached result. The functions set_state and get_state can be used to implement the necessary state caching functions expected by the rewriter.

Returning to our Wff example, we have the following possible implementation of the external index:

   rewrite class Simplify (Wff)
   {  RewriteCache cache;
   public:
      int get_wff_state(Wff t) const { return cache.get_state(t); }
      void set_wff_state(Wff t, int s) { cache.set_state(t,s); }
   };

   rewrite Simplify
   {  index: Wff = extern wff;
      ...
   };

Tips: manual memory management is used, a term should not be deallocated from memory if a cache contains a handle to it. The method invalidate can be used to make sure the entry associated with a term is removed from the cache.