[SMT-LIB] Command line to produce the competition results for the QF_FP division

[Christoph Wintersteiger]

Yes, you can. Instead of (check-sat) you can run a custom tactic that will not go all the way to solving the problem. The default tactic is called qffp and you can run it using
(check-sat-using qffp)
The default tactic is constructed (in C++) here:
https://github.com/Z3Prover/z3/blob/master/src/tactic/fpa/qffp_tactic.cpp
And you can use whatever parts you like. For instance, the most basic translation to BV is
(check-sat-using (then simplify fpa2bv))
(One call to simplify is almost always mandatory because gets rid of expressions that aren’t handled by the later tactics).

Cheers,
Christoph



Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter<http://research.microsoft.com/people/cwinter>

[MSFT_logo_Gray DE sized SIG1.png]
Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB

From: rdelmas [mailto:Remi.Delmas at onera.fr]
Sent: 19 January 2016 21:07
To: Christoph Wintersteiger <cwinter at microsoft.com>
Cc: Zhoulai <zell08v at gmail.com>; smt-lib <smt-lib at cs.nyu.edu>
Subject: Re: [SMT-LIB] Command line to produce the competition results for the QF_FP division


Hi, jumping in the discussion, in Z3 with theory FP is there any way to dump the SAT instance obtained after bitblasting the system in a dimacs file? Even better would be an intermediary bitvector instance in which FP operations would be coded using integer bv operations?

Regards,

/Rémi

Le 2016-01-19 19:10, Christoph Wintersteiger a écrit :
Hi,

Z3 is the default bit-blaster in Z3, no command line options.
IJCAR'14 is an approximation technique implemented inside of Z3, but it's not integrated into the Z3 master yet. It's available in Aleks Zeljic's fork of Z3 in the smallfloats branch here:
https://github.com/AleksandarZeljic/z3/tree/smallFloats
Also shouldn't take any command line options. That technique is describe in our IJCAR'14 paper, hence the name.

There were a number of bug and performance fixes since the last competition, so the numbers will not be the same for the latest version. Also, some fixes my not be in the smallfloats branch yet, but they are in Z3 proper.

Cheers,
Christoph


Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu<mailto:smt-lib-bounces at cs.nyu.edu> [mailto:smt-lib-bounces at cs.nyu.edu<mailto:smt-lib-bounces at cs.nyu.edu>] On Behalf Of Zhoulai
Sent: 19 January 2016 17:31
To: smt-lib <smt-lib at cs.nyu.edu<mailto:smt-lib at cs.nyu.edu>>
Subject: [SMT-LIB] Command line to produce the competition results for the QF_FP division

Hello,

I am trying to produce the competition results for the QF_FP division as reported at this page:
https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fsmtcomp.sourceforge.net%2f2015%2fresults-QF_FP.shtml%3fv%3d1446209369&data=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7c07b03765b9a74aa7533a08d320f696c4%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=rTDjO9YfANxBwxr7yoEFfe4THGW0K2QWVL%2bFWjXqL7s%3d

I have two questions for doing so:

1. What do Z3 (FP) and Z3 (IJCAR14) refer to respectively?
2. What are the  command line options used to run these benchmarks?

For MathSat5,  I use:
mathsat <filename> for MathSat 5,

and for Z3 4.4.2, I use:
z3 --smt2 <filename> for Z3.

Are there additional options I need to put for MathSat or Z3?

I do not use the same machine as StarExec and only need to produce the results on a local machine for comparison purpose.  Thanks for your help.

Zhoulai
_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu<mailto:SMT-LIB at cs.nyu.edu>
https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww.cs.nyu.edu%2fmailman%2flistinfo%2fsmt-lib&data=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7c07b03765b9a74aa7533a08d320f696c4%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=QPCqUZ3ygaRgL1iEg1WBQROhmnU1mOP0gmltS9%2b0ScQ%3d
_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu<mailto:SMT-LIB at cs.nyu.edu>
http://www.cs.nyu.edu/mailman/listinfo/smt-lib<https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww.cs.nyu.edu%2fmailman%2flistinfo%2fsmt-lib&data=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7c68a2f158572b4ad5c8ab08d32114736d%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=NnNP4Zm5hvj969t8gIuPKBma0Wsof1muAkML8nM0A7w%3d>



-------------- next part --------------
A non-text attachment was scrubbed...
Name: image001.jpg
Type: image/jpeg
Size: 1168 bytes
Desc: image001.jpg
URL: </pipermail/smt-lib/attachments/20160120/f1e74e0f/attachment-0001.jpg>