Using an internal index

In order to make use of an index, certain member functions have to defined by the user. Given an internal index named foo, the rewriter invokes two functions named

int get_foo_state() const;
void set_foo_state(int);

within the generated code. The user should provide the implementations for these functions within the datatypes.

For example, reusing the well-formed formulas example (see section 4.1.2), an internal index on the datatype Wff can be implemented as follows:

#include <AD/rewrite/burs.h>
class WffIndex {
   int state;
public:
   WffIndex() : state(BURS::undefined_state) {}
   int get_wff_state() const { return state; }
   void set_wff_state(int s) { state = s; }
};

datatype Wff : public WffIndex
   = F
   | T
   | Var     (const char *)
   | And     (Wff, Wff)
   | Or      (Wff, Wff)
   | Not     (Wff)
   | Implies (Wff, Wff)
   ;

...

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

Here, the class WffIndex provides the internal index interface functions get_wff_state and set_wff_state expected by the rewriter. Note that each term must be initialized with the state BURS::undefined_state. This constant is defined within the library include file <AD/rewrite/burs.h>.

To enable the index, in the rewriter we specify that datatype Wff should make use of the index named wff, using the index: declaration.