[SMT-LIB] Benchmarks Compliant to SMTLIB

[Cesare Tinelli]

Hi Paulo,

On Aug 18, 2008, at 10:40 AM, Paulo J. Matos wrote:

> Hello all,
>
> I have seen some benchmarks (/sal) in QF_LRA, that contain terms of
> the form: (* (- x10 x11) 10). This doesn't seem to comply with the
> smtlib official syntax for QF_LRA, right?
>
It complies. It matches the pattern (* t n) below.


> <time to read the file>
> I have just re-read the syntax for QF_LRA:
> :extensions
>  "Terms with positive integer coefficients are allowed, that is,  
> expressions
>   of the form (* n t) or (* t n) for some numeral n, both of which  
> abbreviate
>   the term (+ t ... t) having n occurrences of t.
>  "
>
> I would assume that it complies because it would be equivalent to (+
> (- x10 x11) (- x10 x11) (- x10 x11) ...) , however, would this be
> compliant: (* (- x10 x11) (/ 1 10))? It shouldn't because it says n
> should be a numeral, right?

Right. The original rationale for not allowing rational coefficients  
is that they can be eliminated from equations by means of standard  
equivalence preserving transformations.

Best,


Cesare

>
> Cheers,
> -- 
> Paulo Jorge Matos - pocm at ecs.soton.ac.uk
> http://www.personal.soton.ac.uk/pocm
> PhD Student @ ECS
> University of Southampton, UK
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib