SMTPlan
SMTPlan copied to clipboard
Prefix to infix notation
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),