[SMT-LIB] Question to AUFLIRA logic

[Jochen Hoenicke]

Hello Cesare,

2011/7/14 Tinelli, Cesare <cesare-tinelli at uiowa.edu>:
> Hi Jochen and all,
>>
>>  "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)?
>>
> All of the above. The use of the word "declaration" there is incorrect.
> It should be "rank". I will fix it.

Maybe "operator" should also be changed to "function symbol" to be
consistent with the notation in the standard.

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

It makes the code a bit ugly, since at some places one needs to
explicitly check for the logic AUF[LN]IRA when searching for the
function symbol.  All other logics do not need such a hack.  So I
would vote to remove it.

>> It also appears that one cannot express x/3 without overloading, [...]
>>
>
> That is not completely true. Terms like (* (/ 1 3) x) are allowed.

Yes, what I meant was that this syntax requires overloading, so
changing overloading would also have consequences here.  (* (/
(to_real 1) (to_real 3)) x) is probably not the desired syntax.

>> (assert (= (abs 5) 5))
>> ;(error "(abs 5) is not a linear term")
>
> 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.

An expressive and easily syntactically checkable restriction for
linear terms would be:

In every application of the function symbol *, at least one of the two
arguments must be a constant term.  In every application of /, div,
mod the second argument must be a constant term.  A constant term is a
numeral, a decimal, an application of +,-,*,/,to_real to constant
terms, or a variable that is bound to a constant term by an outer let.

Allowing only +,-,*,/ for constants should be enough. I also include
"to_real" to make it compatible with the syntactic sugar for
overloading and "let" since it is heavily used by benchmark
transformers.

It is not that difficult to implement. It would also allow "div" and
"mod" with a constant divisor, which may be a problem for existing
solvers---although (_ divisible n) is already allowed by the standard.
 In AUFLIRA, (div x c) would be syntactic sugar for (to_int (* (/ 1 c)
x)), and in other logics one can easily remove it by introducing an
auxiliary constant.  The term (mod x c) can be defined as (- x (* c
(div x c))). Maybe as a compromise with existing solvers, one can
leave the LRA/LIA logics unchanged and only use this more expressive
definition of linear for the logics *UFL[IR]A.

Also the restriction to the two array types seems very arbitrary.
AUFLIRA is not even a super-set of AUFLIA.

BTW: in most *UFL[IR]A logics (* 2 (f x)) is forbidden although it is
allowed in QF_AUFLIA and AUFLIA.  Also, omitting the extra condition
in QF_AUFLIA that "f" is not an "Ints"-symbol should not be a problem
for a "self respecting" solver and makes the logic definition simpler.

  Jochen

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