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

[Christoph Wintersteiger]

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] On Behalf Of Zhoulai
Sent: 19 January 2016 17:31
To: smt-lib <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
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