[SMT-LIB] Question to AUFLIRA logic

[Tinelli, Cesare]

Hi Jochen,

On 15 Jul 2011, at 10:39, Jochen Hoenicke wrote:

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



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


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

[...]
> 
> 
> An expressive and easily syntactically checkable restriction for
> linear terms would be:
> 
Your suggestions below are quite interesting. I will discuss them with Clark and Morgan after SMT-COMP and see if can redefine the logics along those lines.

Many thanks,


Cesare


> 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