Maude-help mailing list

["Guoqiang Li" <li.g AT agusa.i.is.nagoya-u.ac.jp>]

Hi,

 

I met a problem when using the Linear Diophantine Equation Solver in the linear.maude file predefined by Maude.

 

I constructed a file, using load command to import the linear.maude,

 

load linear.maude .

 

and defined a module TRACE which imports DIOPHANTINE by protecting(including)

 

fmod TRACE is

   protecting DIOPHANTINE .

  ...

 

endfm

 

Then, when I tested the function natSystemSolve as follows,

 

reduce in TRACE : natSystemSolve( 0,0 |-> 1 ; 0,1 |-> 2 ; 0,3 |-> -3,  zeroVector, "gcd") .

 

it does not work:

 

rewrites: 0 in 2262221ms cpu (0ms real) (0 rewrites/second)

result IntVectorSetPair: natSystemSolve(0,0 |-> 1 ; 0,1 |-> 2 ; 0,3 |-> -3,  zeroVector, "gcd")

 

while the fuction is performed well in the DIOPHANTINE module,

 

reduce in DIOPHANTINE : natSystemSolve(0,0 |-> 1 ; 0,1 |-> 2 ; 0,3 |-> -3,
    zeroVector, "gcd") .

rewrites: 1 in -3336089716ms cpu (0ms real) (~ rewrites/second)
result IntVectorSetPair: [
  zeroVector
|
  2 |-> 1,
  0 |-> 3 ; 3 |-> 1,
  1 |-> 3 ; 3 |-> 2,
  0 |-> 1 ; 1 |-> 1 ; 3 |-> 1
]

 

I do not what wrong I have done. So would someone please offer me help. I expect two functions can return the same result.

 

Best regards, Guoqiang LI