[metis-users] rewrite structure in Metis

[Joe Hurd]

Hi James,

[This is just the kind of technical information that I'm trying to
archive on the metis-users list, so I'll take up your offer to cc: my
reply to the list.]

The Rewrite structure is pretty complex inside, but it seems for your
task you only need to use its API, which is a little easier to
explain.

In fact, if you're maintaining a backtracking tree then you might just
be able to store the Rewrite structure that is in effect at the
splitting point, and then use this as the starting point when you
return from one branch and go down the other. Since the Rewrite
structure is purely functional, the version you store is guaranteed
not to change while you explore.

Does this address your needs, or is there a reason why you can't use
this technique?

Also, if the obscure bug you discovered lives in the Metis code, I'd
appreciate knowing more details.

Cheers,

Joe

On Thu, Apr 7, 2011 at 6:29 AM, James Bridge <jpb65 at cam.ac.uk> wrote:
> Hi Joe,
>
> As you know, I am implementing splitting with backtracking in MetiTarski and
> to do this properly I need to be able to remove equations from the rewrite
> structure as well as adding them (i.e. when backtracking).
>
> I initially did this by creating a new rewrite structure and passing
> equations from one to the other, filtering out any that had been made
> redundant by the backtracking. Unfortunately this seems to lead to an
> obscure bug by which an axiom equational clause is repeatedly returned by
> extract_rewritable.
>
> It would be very useful if you could explain the various parts of the
> rewrite structure.
>
> I didn't copy in the Metis-Users group on this e-mail as I didn't know if it
> was of general interest, but I am of course quite happy for you to do so in
> your reply.
>
> Best Regards,
>
> James
>