Maude-help mailing list

[Ozan Kahramanogullari <ozan.kah AT gmail.com>]

Hi,

I am experimenting with some of my system modules and I could not find a simple solution to the following problem. I was wondering if someone could help.

Consider the following module.

mod S is
  sorts Atom Structure .
  subsort Atom < Structure .
  ops a b : -> Atom .

  op -_ : Atom -> Atom [ prec 50 ].
  op [_,_] : Structure Structure -> Structure [assoc comm ] .
  op {_,_} : Structure Structure -> Structure [assoc comm ] .

 var R T U : Structure . var A : Atom .

  rl [rls] : [ { R , T } , U ] => { [ R , U ] , T } .
endm

I do a one-step search as follows, which behaves as expected.

search in S : [[{a,b},{a,b}],{[- a,- b],[- a,- b]}] =>1 X .

Solution 1 (state 1)

states: 2  rewrites: 1 in 0ms cpu (0ms real) (11764 rewrites/second)

X --> {[- a,- b],[- a,[- b,[{a,b},{a,b}]]]}

Solution 2 (state 2)

states: 3  rewrites: 2 in 0ms cpu (0ms real) (17391 rewrites/second)

X --> [{a,b},{[- a,- b],[- a,[- b,{a,b}]]}]

Solution 3 (state 3)

states: 4  rewrites: 3 in 0ms cpu (0ms real) (20689 rewrites/second)

X --> {b,[a,[{[- a,- b],[- a,- b]},{a,b}]]}

Solution 4 (state 4)

states: 5  rewrites: 4 in 0ms cpu (0ms real) (23529 rewrites/second)

X --> [{[- a,- b],[- a,- b]},{b,[a,{a,b}]}]

Solution 5 (state 5)

states: 6  rewrites: 5 in 0ms cpu (0ms real) (25510 rewrites/second)

X --> [{a,b},{b,[a,{[- a,- b],[- a,- b]}]}]

Solution 6 (state 6)

states: 7  rewrites: 6 in 0ms cpu (0ms real) (27027 rewrites/second)

X --> {a,[b,[{[- a,- b],[- a,- b]},{a,b}]]}

Solution 7 (state 7)

states: 8  rewrites: 7 in 0ms cpu (0ms real) (28340 rewrites/second)

X --> [{[- a,- b],[- a,- b]},{a,[b,{a,b}]}]

Solution 8 (state 8)

states: 9  rewrites: 8 in 0ms cpu (0ms real) (29520 rewrites/second)

X --> [{a,b},{a,[b,{[- a,- b],[- a,- b]}]}]

No more solutions.

states: 9  rewrites: 8 in 0ms cpu (0ms real) (26755 rewrites/second)

The question is how can I get the information on the substitution in each solution? What I am looking for is not the X's substitution, but the subterms with which R, T, and U of the rule are matched. How can I get this information?

Thanks in advance!

Ozan

=======================

 Ozan Kahramanoğulları, PhD

              ozan-k.com       

=======================