if-then-else in SMT-LIB

[Cesare Tinelli]

Dear Jim,

thanks a lot for your comments on the SMT-LIB format proposal.

You raise some good points and we believe you are right in
advocating a native support of the second kind of if-then-else
construct. Similar observations were raised at the PDPAR panel
on SMT-LIB last July by Clark Barrett and others.
We are going to modify the proposal along the lines you suggest.

Before that however we plan to distribute soon a report on the
panel discussion and all the modifications to the proposals
suggested there, together with our own recommendations.

So, everybody stay tuned for more updates.

Best,


Silvio & Cesare


PS: A little more detailed reply follows below.


Jim Saxe wrote:
> Dear Cesare and Silvio,
> 
> Thanks for your work on the initial SMT-LIB format proposal
> (http://combination.cs.uiowa.edu/smtlib/proposal.pdf).
> 
> In the proposal, you remark that "conceptually there are two kinds of
> if-then-else construct" namely (1) a formula
> 
>     if phi then phi_1 else phi_2
> 
> where phi, phi_1, and phi_2 are formulas, and (2) a term
> 
>     if t then t_1 else t_2
> 
> where t, t_1, and t_2 are terms.  You propose not to support the
> second kind.  I am writing to question this decision and the reasons
> given in support of it.
> 
> First, you say that the term-valued if-then-else "is problematic because
> its semantics is domain dependent as it is based on the type of t."  I
> suggest that appropriate form for an if-then-else term is
> 
>     if phi then t1 else t2
> 
> where phi is a formula and t1 and t2 are terms.  With this form, the
> of what what value(s) of the first argument should be treated as
> "true" becomes trivial.
>
That is true. On the other hand it slightly complicates the logic 
because we know have formulas inside terms. This is a non-standard 
extension of FOL which needs to be properly defined formally.
We think though that this extension is not really problematic, and
it is worth it in order to avoid the problems you mention below.


> Second, you suggest that the effect of if-then-else terms can be
> achieved "with no substantial loss of structural information" by
> replacing occurrences of if-then-else terms with fresh constants and
> introducing what I will call "side-conditions" forcing those constants
> to have the appropriate values.  It appears to me that this
> potentially involves substantial loss of structural information.
> 
You are right here. We did not think this through.

[...]

> Another difficulty with the proposed technique for eliminating
> if-then-else terms is that it becomes more complicated in the presence
> of quantifiers, particularly quantifiers appearing in positions that
> cannot be uniquely haracterized as positive or negative.  As an
> extreme example, consider a query Q of the form
>
[...]

Your example is a good one.

You are glad that you and other spotted these problems in our proposal
and pointed that out.
It show that the SMT-LIB working group is indeed working!