[SMT-LIB] Question to AUFLIRA logic

[Tinelli, Cesare]

Hi Jochen and all,

On 14 Jul 2011, at 08:06, Jochen Hoenicke wrote:

> 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.

Strictly speaking the extension does not introduce any actual overloading: if an operator has only one rank (Real Real s) writing (op 3.4 6), say, does not add the rank (Real Real s) to the operator.
The expression (op 3.4 6) is simply syntactic sugar for (op 3.4 (to_real 6)).

The fact that this is only syntactic sugar and not actual overloading is an important difference. See below.


>  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)?
> 
All of the above. The use of the word "declaration" there is incorrect.
It should be "rank". I will fix it.


> Is the following behavior the desired behavior?
> 
Not in its entirety.

> (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)")

In the intention of the extension, the last three asserts above are all fine. Again no overloading is going on, only an implicit "upcasting". So reporting an error is not the correct behavior. 

Incidentally, a while ago Nikolaj Bjorner sent a message to this list recommending the elimination of this extension and so requiring explicit to_real conversions in every case, on the grounds that the extension makes parsing more difficult, even if is more convenient in other ways.
I asked this list for further opinions but only a couple of people expressed support for Nikolaj's proposal. So we left the extension there under the assumption that there was not enough interest in removing the extension.
We could reconsider that decision if now there is enough renewed support for removal.



> (declare-fun f (Int Int) Int)
> ;(error "Function f already defined")

Reporting an error here is correct, simply because user-defined symbols cannot be redefined (in the same scope).

> (define-fun abs ((x Int)) Int (ite (>= x 0) x (- x)))
> ;(error "Function abs already defined")

Same as above.

> (assert (= (abs 5) 5))
> ;(error "(abs 5) is not a linear term")

Correct behavior.

> (define-fun myabs ((x Int)) Int (ite (>= x 0) x (- x)))
> ;success
> (assert (= (myabs 5) 5))
> ;success
> 
Also correct. One may wonder why myabs is accepted and abs is not. The decision to exclude the predefined abs from the definition of linear terms is simply because of tradition, even if abs can be reduced to an ite combination of linear terms.

The main issue is as usual where to draw the line. For example, the formula 

   (and (= x 3) (= (* x y) 5))

is effectively linear, and any self-respecting linear solver will be able to process such formula. But allowing cases like this in the logic would greatly complicate its definition.


> 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.
> 

That is not completely true. Terms like (* (/ 1 3) x) are allowed.
See, e.g., the second :extension attribute of AULIRA's definition (http://www.smt-lib.org/logics/AUFLIRA.smt2).
The rationale was to allow the use of the operator / to represent rational coefficient in fractional form. The alternative would have been to introduce a new operator (frac Int Int Real) just for rational coefficients.

Terms (/ x 3.0) and (* (/ 1.0 3.0) x) are indeed forbidden. The first because it does not use / to express a rational coefficient. The second to simplify the definition and avoid the proliferation of alternative ways to write rational coefficients.

Best,


Cesare


> Regards,
> Jochen
> 
> -- 
> Jochen Hoenicke, University of Freiburg,
> Email: hoenicke at informatik.uni-freiburg.de  Tel: +49 761 203 8243
> 
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib