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

[rdelmas]

Thank you Christoph, 

is it possible to ask z3 for a dump of the simplified/bitblasted formula
using a specific tactic in the smt2 file or must I use the API to
introspect the solver contents and print it back to a file? 

Best, 

/Rémi 

Le 2016-01-20 12:02, Christoph Wintersteiger a écrit : 

> 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 [2] 
> 
> _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] 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 [1]

  

Links:
------
[1]
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
[2] http://research.microsoft.com/people/cwinter