[metis-users] rewrite structure in Metis

[James Bridge]

Hi Joe,

Sadly it is not a simple backtracking tree - a split doesn't freeze 
conditions at the split point because heavier clauses coming out of 
waiting, that don't depend on the split, may combine with other clauses 
that don't depend on the split and thus it may be possible that new 
equations are written to the rewrite structure that need to be retained 
even after backtracking.

Each clause carries a label indicating which splits it depends on so it is 
possible to determine which should be deleted on backtracking (and in some 
cases which should be restored). So what I want to be able to do is run 
through the rewrite structure and remove any equations, and related data 
items, which have redundant labels.

I had a similar problem with the waiting clause set which, as you know, is 
stored as a functional heap. To avoid destroying the heap and reforming it 
I use a lazy approach and check each clause as it is removed from the heap. 
(I would like to improve on this at some stage but it is not an urgent 
priority.)

As far as the bug is concerned, I don't think this is in the Metis code per 
se, rather it arises because of my attempt to filter the rewrite structure. 
What happens is that an equational axiom is placed in the original 
structure and stays there quite happily (i.e. it is not removed as a 
potentially simplyfiable clause by extract_rewritable). Then after I have 
done my filtering process as part of backtracking it is extracted from the 
new rewrite structure. So the problem arises in my attempt at reproducing 
the rewrite structure.

I can think of work-arounds, such as keeping a list copy of everything 
added to the rewrite structure and then filter this list and recreate the 
rewrite structure on backtracking but this seems to be a bit extravagant on 
storage space. (Though I think that the rewrite structure is probably small 
compared to other storage structures such as waiting.)

In general, the problem with backtracking is that most Metis structures are 
well set up to accept new clauses but are much less happy about giving them 
back again! (This is not a criticism of Metis, I think most theorem provers 
are written in the same way.)

James

On Apr 7 2011, Joe Hurd wrote:

>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
>>
>