[SMT-LIB] A beginner's question about Wintersteiger's benchmark

[Levent Erkok]

Yes; you can think of this sort of a benchmark as a unit-test essentially;
it's making sure that the fp.add function works "as expected" on two
particular inputs with the expected output given in r.

Not something most people would usually write, but these sorts of
benchmarks arise very naturally when writing test-benches for tools that
are built on top of SMT-solvers, or for SMT-solvers themselves.

-Levent.

On Wed, Nov 25, 2015 at 2:55 PM, Zhoulai <zell08v at gmail.com> wrote:

> Hello,
>
> I am new to SMT-LIB format and want to learn something about the recently
> added FP theory. Below is a piece of syntax from the benchmark of
> Wintersteiger (thanks): add-has-solution-12196.smt2.
>
>
>  (set-logic QF_FP)
> (set-info :status sat)
> (define-sort FPN () (_ FloatingPoint 11 53))
> (declare-fun x () FPN)
> (declare-fun y () FPN)
> (declare-fun r () FPN)
> (assert (= x (fp #b0 #b01111101100
> #b1110010110001100001110000101110111111011011010000001)))
> (assert (= y (fp #b1 #b01010111111
> #b1110111010100000001111111010111000001000101111000001)))
> (assert (= r (fp #b0 #b01111101100
> #b1110010110001100001110000101110111111011011010000000)))
> (assert (= (fp.add roundTowardNegative x y) r))
> (check-sat)
>
> Question: Am I correct in understanding that the first three 'assert'
> specify the values of x,y and r through their sign, exponent, and mantissa,
> and the last 'assert' check-sat for x+y==r (with the specified rounding
> mode)?
>
> I feel confused since usually we check-sat for a formula where all
> variables are *not* yet assigned a concrete value, such as (x+y<=0 /\
> x<-y+3).
>
> Thanks.
> Zhoulai
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>