[SMT-LIB] you questions on SMT-LIB

[Cesare Tinelli]

Hi Domagoj,

I am copying the whole SMT-LIB list because I think our conversation  is 
of interest to everybody in list.

Domagoj Babic wrote:
> Hi,
> 
> Cesare Tinelli wrote:
>  > Hi Domagoj,
>  > thanks again for your feedback on SMT-LIB. My reply to your questions
>  > follows below. I'm CC'ing the other SMT-LIB/COMP organizers, for their
>  > information.
>  > Cheers,
>  > Cesare
> 
> Thx for your replies.
> 
> 
>  >  >>> If not,
>  >  >>> the standard should somewhere explicitly state the expected format,
>  >  >>> something like:
>  >  >>> {SGN}?(({DIGIT}+\.{DIGIT}*)|(\.{DIGIT}+))({EXP}{SGN}?{DIGIT}+)?
>  >  >>>
[Note: Domagoj was requesting that we allow this format for concrete 
constants in the real arithmetic logics of SMT-LIB.]


>  > Why should we allow this "expected format"? I really mean it.
>  >
>  > A major design goal of SMT-LIB is to keep it simple as much as possible.
>  > As I recall it, when we defined QF_LRA and similar logics, we thought
>  > that we did not really need that additional syntax.
>  > However, if you make a compelling case of why it would be good to
>  > complicate parsers to also allow the syntax above (or if we get enough
>  > requests) we will certainly consider the extension.
> 
> The "expected" format is (I think) the most standard one. The exact
> format does not really matter that much, as long as it is specified,
> handy to use, and has a specified border behaviour (rounding). The
> (/ m n) construct in LRA does not really meet the last two
> requirements.
> 
I do not quite understand your last statement. What do you mean by a 
"specified border behaviour". These logics axiomatize real arithmetic, 
not floating point arithmetic, these is no notion of rounding in the logic.

> I do not really care about that personally, but other people
> might. That's why I think that the benchmarks should be capable of
> unambigiously representing IEEE 754 floating point.
> 
Perhaps this is the main difference here. You are thinking as these as 
floating point numbers. What those logics model however are the real 
numbers in the mathematical sense. With the latter, coefficients are 
(infinite precision) rational numbers.

Of course one might argue whether these logics are the appropriate ones 
for verification benchmarks, which come from applications that have to 
deal with---usually, finite precision---floating point numbers, not the 
real numbers in the mathematical sense. (More on this below.)



> The other related point is just pure readability. It is not really
> obvious what (/ 80143857 25510582) or (+ 3 (/ 1 (7 + (/ 1 16))))
> stands for.
> 
Let me stress this once more, for everybody. The SMT-LIB format is meant 
to be an intermediate format, mostly for machine use. Human readability 
is not the driving concern.
That said, given that the logics in questions are about reals, not 
floating point numbers, at most we could use the decimal notation 
writing 3.45, say, instead of (/ 345 10). Using the IEE floating point 
notation is not an option because it refers to notions that simply are 
not in the logic (precision, number of bits, infinity and NaN values, etc.)
Now if there are enough requests, I do not see any problems in allowing 
the decimal notation for coefficients in addition to the fractional one. 
Anybody?


> Finally, the benchmark generators would need to come up with
> these approximations, and the decision procedures need to perform
> additional redundant divisions, which is a problem from both
> precision and performance point of view.
> 
Yes, but again this means that we are not using the right logic for 
those benchmarks and we should develop a mathematical (meta)theory of 
floating point numbers (axiomatization, determination of the 
decidability of the SMT problem, sound a complete satisfiability 
algorithms and so on).
Except for the axiomatization (done by the Maude people, 
http://maude.cs.uiuc.edu/) I'm not aware of the existence of such work. 
Are you, or anyone in the list, aware of such results?



> Perhaps my comment is of-the-track. But, what is the purpose of LRA
> if it cannot exactly model the floating point behaviour commonly
> found in HW & SW systems?
> 
Your question is in fact right on track. The answer is: the point of LRA 
for HW & SW verification is that it can used to do *approximate* 
reasoning over the floating point numbers. We use LRA at the moment 
because we do not have better options, yet.

As research advances, we will hopefully arrive to an accurate theory and 
logic of floating point numbers, and finally use that one for HW & SW 
verification.

The same point can be made about integer arithmetic of course. That is 
why I look forward to research like your own on reasoning about machine 
ints, not mathematical integers. Until then Presburger arithmetic will 
have to do.


> 
>  >  >>> 4) I've been thinking about writing ModInt.smt theory of modular
>  >  >>> arithmetic and corresponding QF_MLIA.smt. Some of the benchmarks 
> from
>  >  >>> other logics might be easily converted to QF_MLIA imposing 
> arbitrary
>  >  >>> constraints on the number of bits. Are there any chances that a
>  >  >>> competition category for QF_MLIA is opened at the next year's SMT
>  >  >>> competition?
>  >  >>>
>  > How's your progress on the solver?
>  > We are a little late (my fault) for having a QF_MLIA division at
>  > SMT-COMP'06. But we could try if you were able to provide enough
>  > benchmarks in the next couple of weeks, say. There is currently an open
>  > call for benchmarks for SMT-COMP'06 (see the SMT-COMP announcements in
>  > the SMT-COMP list archives for May).
>  > The sooner the benchmarks and logic
>  > are ready, the more likely it will be that they are included in a
>  > SMT-COMP'06 division. I should stress though that a division can be
>  > canceled in the end if not enough solvers enter it. Do you know of other
>  > people who might already have a solver for arithmetic modulo n?
> 
> For several reasons (mostly too complex boolean structure) I concluded
> that those benchmarks are not suitable for the decision procedure I
> was working on with Madan. But I tried something else: I assumed that
> all the values are of finite (8,16,32,64-bit) size, and flattened the
> benchmarks to ILP problems (standard CPLEX and LP formats). None of the
> several ILP solvers I tried could solve anything. CPLEX was running
> for days, others often ran into numerical instabilities. So, I
> abandoned that direction of work (for now).
> 
> Perhaps MSR Cambridge constraint solving group. 
 >
Some of them subscribe to this list. Maybe the can jump in here.


> I'd suggest asking
> Byron Cook. In a month-or-two, I'm going to generate a set of modular
> arithmetic SW verification benchmarks (too late for SMT'06). Also,
> I'll have my own decision procedure (unrelated to the work I did
> with Madan) by autumn.
> 
> BTW, what's the current status of the QF_MLIA spec?
> 
> If the spec is nonexisting, or in a very nascent state, I'd be
> interested to get involved in its development for SMT'07.
> 
Great. Let's keep in touch on that.


> 
>  >  >>> Suggestions:
>  >  >>> 1) Only '+' operator can have multiple terms. It might be a good
>  > idea to
>  >  >>> allow any commutative operator to have multiple terms.
>  >  >
>  > I suppose you meant "associative" here?
> 
> Yes, sorry.
> 
>  > The standard per se needs no fixing. Among the Boolean connectives (the
>  > only ones that are predefined by the standard) the associative ones
>  > already allow more than two arguments. As for theory specific symbols,
>  > it is each single logics that might need to be adjusted. Now, QF_LRA,
>  > QF_LIA and related logics already allow multiple arguments for +.
> 
> Excellent.
> 
>  > I think this is a point that needs broader discussion. 
 >
[Note: the point was using flattened expressions like (+ t1 t2 ... tn) 
instead of the deeply nested ones generated by treating the associative 
operators strictly as binary only.]


>  > As I said above,
>  > the standard already takes your point into consideration. The current
>  > benchmarks in the library do not take advantage of that. What is needed
>  > then is a conversion of those benchmarks to flatten the nested
>  > associative operators. I'm sure that Clark Barrett, who is in charge of
>  > of managing the benchmarks would not be opposed to that. The only
>  > problem for now would be to find the time ...
>  > I urge you to raise it in the SMT-LIB list.
> 
> Yes, conversion is not a problem, but it does take a day-or-two of work.
> 
[...]
> 
>  >  >>> 3) It is not clear to me whether redefinition of of
>  >  >>> fvars/vars/quant_vars is allowed: (and (flet ($twin (not sig1))
>  >  >>> $twin) (flet ($twin (not sig2)) $twin)).
>  >  >>>
>  >  >>> I'd suggest forbidding this in the standard. If each identifier
>  > must be
>  >  >>> unique, it's easy to check in symbol table whether the 
> identifier has
>  >  >>> been properly declared. If redefinition is allowed, the parser 
> should
>  >  >>> remove the symbol when its scope is left, and that's an unnecessary
>  >  >>> burden that makes parsing slower, more error-prone, and much more
>  >  >>> complicated.
>  >  >>>
>  > This issue has already been discussed at some length in the SMT-LIB
>  > list. The conclusion was to allow redefinitions given that there are
>  > standard parsing techniques to deal with that. Uniqueness of bound
>  > variables is really not needed and having that adds another constraint
>  > to the format that must be enforced when certifying that a benchmark
>  > complies to the format.
> 
> Hmm... Uniqueness is very simple to enforce while the benchmark is being
> generated. 
 >
Not necessarily,. I think it depends on the internal format used to 
store expression.

> However, the decision procedures need to do (at least local)
> flattening and renaming of terms. I just thought that's redundant and
> complicates the decision procedure. 
 >
In my experience most sophisticated enough decision procedures have to 
these sorts of things anyway. So the additional cost of properly dealing 
with scoping issues is relatively small.

> Also, checking for compliance is
> trivial.
> 
Especially if someone else (i.e., the SMT-LIB mantainers) is doing that 
for you :)


Cheers,


Cesare


> Regards,
>     Domagoj
>