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

[rdelmas]

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] 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
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib