[SMT-LIB] [CVC-USERS] QF_RDL SMT-LIB2 format.

[Christopher L Conway]

Trevor,

There's an ambiguity here that will have to be resolved by the SMT-LIB folks.

The Reals theory defines addition with the signature
   (+ Real Real Real :left-assoc)
The attribute :left-assoc means that the function symbol can be used
with more than 2 arguments, e.g.,
   (+ a b c)
will be interpreted as
   (+ (+ a b) c)
I don't see any allowance made for '+' to take 0 or 1 arguments.

However, you are correct that the QF_RDL logic allows expressions of the form
    (op (- (+ x ... x) (+ y ... y)) c) with n > 0 occurrences of x and y
It is not clear to me whether this is an error or if it is intended as
syntactic sugar provided by the logic.

This may seem pedantic, but we use CVC3 as a reference implementation
for SMT-LIB v2 parsing (e.g., we use it to translate and check
benchmarks for the competition), so I'd like to make sure we implement
the intended behavior.

Regards,
Chris

On Fri, Sep 17, 2010 at 12:47 AM, Trevor Alexander HANSEN
<thansen at csse.unimelb.edu.au> wrote:
> Hello,
>
> I'm updating Robert Brummayer's FuzzSMT tool to output SMT-LIB2 format.
> I'm using CVC3 version 2010-09-01 to test its output.
>
> Given this instance:
>
> (set-info :source | fuzzsmt |)
> (set-logic  QF_RDL)
> (set-info :status unknown)
> (declare-fun v1 () Real)
> (assert
> (let ((e1 (< (- (+ v1) (+ v1 v1)) (- 1))))
> e1
> ))
> (check-sat)
>
>
> CVC3 reports:
> *** Parse Error: stdin:6: [bin,N]-ary operator used in unary context
>
> Because of the (+ v1) term.
>
> My reading of the SMTLIB2 QF_RDL specfication is that n>0 occurences are
> allowed. So it seems to me that the example should be parsed?
>
> Thanks,
>
> Trevor
>
> _______________________________________________
> CVC-USERS mailing list
> CVC-USERS at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/cvc-users
>