I'm not sure if this is a bug, so I just wanted to check: how should the prefix notation for arithmetic operations (+, -, *, /) be converted to infix notation? I expected that (- x y) was the same as (x - y), but it seems to be (y - x) instead. However, for division, it seems that (/ x y) does mean (x / y), not (y / x). To me, this seems confusing and likely to lead to errors. Is this the intended behavior or a bug?

I tested this using the following domain and problem files:

Domain

(define (domain debug)

(:requirements :numeric-fluents)

(:functions
  (x)
)

(:action xInc
  :parameters ()
  :precondition (and )
  :effect (and
    (assign (x) (+ x 1))
  )
)

(:action xDec
  :parameters ()
  :precondition (and )
  :effect (and
    (assign (x) (- x 1))
  )
)

(:action xMul
  :parameters ()
  :precondition (and )
  :effect (and
    (assign (x) (* x 1))
  )
)

(:action xDiv
  :parameters ()
  :precondition (and )
  :effect (and
    (assign (x) (/ x 1))
  )
)

)

Problem

(define (problem debug1) (:domain debug)

(:init
  (= x 0)
)

(:goal (and
  (= x 10)
))

)

Then I run smtplan with the -n option to print the constraints out. After parsing with z3 (so they're easier to read), the relevant constraints are

Implies((xinc)0_sta, (x)0_1 == 1 + (x)0_0),
Implies((xdec)0_sta, (x)0_1 == 1 - (x)0_0),
Implies((xmul)0_sta, (x)0_1 == 1*(x)0_0),
Implies((xdiv)0_sta, (x)0_1 == (x)0_0/1),