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

[Clark Barrett]

Regarding two of the points below:

We are in the process of calculating updated status and difficulty information
for all benchmarks.  This information will be available soon.

-Clark

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