[SMT-LIB] QF_AUFBV. difficulty, status, syntax.

[Clark Barrett]

This reply was lost...I am reposting it.

> Date: Mon, 20 Jul 2009 09:24:29 -0500
> Message-ID: <687571cb0907200724i7671f548o3f3d0c8ae76fc2f0 at mail.gmail.com>
> Subject: Re: [SMT-LIB] QF_AUFBV. difficulty, status, syntax.
> From: Aaron Stump <aaron.stump at gmail.com>
> To: Trevor Alexander HANSEN <thansen at csse.unimelb.edu.au>
> Cc: smt-lib at cs.nyu.edu
> 
> Hello, Trevor.  Thanks for your questions, which I will answer inline below
> (other SMT-LIB/-COMP organizers can jump in, of course, if they want to add
> to this).
> 
> On Thu, Jul 16, 2009 at 6:21 AM, Trevor Alexander HANSEN <
> thansen at csse.unimelb.edu.au> wrote:
> 
> > Hi,
> >
> > I'm new to the competition and have been looking through the QF_AUFBV
> > benchmarks and have three questions.
> >
> > In the newly addeded benchmarks, many have a status of "uknown". Some of
> > the
> > benchmarks with the unknown status are easy to solve. I understand that
> > "uknown" status benchmarks are not included in the competition. Will the
> > status
> > of these benchmarks be updated before the competition?
> >
> 
> We are discussing this point right now (someone else asked a similar
> question).  Personally I think that the time before the competition begins
> is quite short now, and it is best not to make additional changes like this.
>  But we will have an official reply soon.
> 
> 
> > I note that the difficulty of the new benchmarks isn't set. Also that the
> > difficulty of existing benchmarks not updated. This year's contest rules
> > state
> > that the difficulty will be updated before selection begins. Is calculating
> > the
> > difficulty of the benchmarks something that happens after the benchmarks
> > are
> > frozen? Are the revised difficulties made available before the contest?
> >
> 
> We have been computing difficulties with SMT-EXEC recently, yes.  I do not
> know that we planned to release the updated difficulties before the
> competition -- not that they are secret.
> 
> 
> > testcase7.stp.smt uses an "if_then_else" function. Now it's easy to see
> > what it
> > should do, and easy to parse it properly. It's implemented by most solvers.
> > But
> > is this function actually in the language?
> >
> 
> Yes, it is: see Figure 10 (page 31) of the SMT-LIB specification, version
> 1.2 (from www.smtlib.org).
> 
> Best wishes,
> Aaron