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

Levent Erkok erkokl at gmail.com
Wed Nov 25 18:44:07 EST 2015


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
>


More information about the SMT-LIB mailing list