[antlr-interest] simplification of logic formula

[Ric Klaren]

Michel Metzger wrote:
> I have a logic formula: logic operators (&&, ||, !), atomic proposition 
> (a, b, c, d, ...), and litterals (true, false)
> What I want is to simplify those formulae : for instance translate (a && 
> !a) into false
> I also want to push the not operator in front of atomic propositions 
> only. ie, transform !(a && b) in !a || !b
> 
> To do that, I thought that using tree parser to transform my syntax tree 
> would be a good idea. I wrote the following tree transformation rules:
> 
>     |! (#(OP_NOT OP_OR)) => #(OP_NOT #(OP_OR leftNO:expr rightNO:expr))
>        {
>            #expr = #([OP_AND, "&&"], #([12, "!"], leftNO), #([12, "!"], 
> rightNO));
>        }
>     |!    (#(OP_NOT OP_AND)) => #(OP_NOT #(OP_AND leftNA:expr 
> rightNA:expr))
>        {
>            #expr = #([OP_OR, "||"], #([12, "!"], leftNA), #([12, "!"], 
> rightNA));
>        }
> 
> But I have a problem :
> take the formula !((a && b) || c). The result should be : ((!a || !b) && 
> !c). But with the rules I wrote, the result is :
> (!(a && b) && !c. I understand why, but is there a way to call again my 
> transformation rule on the subtree that I build in my action bloc ?

I guess you have to wrap the call to the treeparser and add a attribute 
to it that gets set when a modification gets done to the tree (e.g. when 
you rewrite a bit). Then keep on calling the treeparser on the new tree 
untill no change is done. Depends a bit on the the transformations you 
do and if they're 'stable' if this simple scheme will work.

Another approach could be to call your tree parser recursively from 
itself. Probably a bit more efficient but could get hairier, I have 
little experience with transforming treewalkers but in simple 
'walk-only' treewalkers this strategy works pretty well. Just see rules 
as method calls. Read the generated code to get a feel for it.

Hope this helps, cryptic as it may be :/

Ric