[SMT-LIB] Question to AUFLIRA logic

[Jochen Hoenicke]

Hello,

we are planning to support mixed real and integer linear arithmetic in
the future.  One stumbling thing is the strange extension

 "For every operator op with declaration (op Real Real s) for some sort s..."

that allows overloading.  What is meant by "operator" in the
description? Is this restricted to the function symbols
<,<=,>,>=,*,+,-,/, or does this also apply to user defined functions
that are declared as (declare-fun op (Real Real) s)? Also does it
apply to = and distinct, even though they are declared as   (= A A
Bool)?

Is the following behavior the desired behavior?

(set-logic AUFLIRA)
;success
(declare-fun f (Real Real) Real)
;success
(assert (= (f 5.0 5.0) (+ 0 0.0)))
;success
(assert (= (f 5.0 5.0) (+ 0 0)))
;(error "No overload for (= Real Int)
(assert (= (f 5 5.0) 0.0))
;(error "No overload for (f Int Real)")
(assert (= (f 5 5) 0.0))
;(error "No overload for (f Int Int)")
(declare-fun f (Int Int) Int)
;(error "Function f already defined")
(define-fun abs ((x Int)) Int (ite (>= x 0) x (- x)))
;(error "Function abs already defined")
(assert (= (abs 5) 5))
;(error "(abs 5) is not a linear term")
(define-fun myabs ((x Int)) Int (ite (>= x 0) x (- x)))
;success
(assert (= (myabs 5) 5))
;success

It also appears that one cannot express x/3 without overloading, since
the way to express this is (* (/ 1 3) x); the terms (/ x 3.0) or (* (/
1.0 3.0) x)  are forbidden in AUFLIA.

Regards,
 Jochen

--
Jochen Hoenicke, University of Freiburg,
Email: hoenicke at informatik.uni-freiburg.de  Tel: +49 761 203 8243