if-then-else in SMT-LIB

[Jim Saxe]

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.

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.

Suppose that we start with a query (by "query", I mean a formula to be
tested for satisfiability) Q containing if-then-else terms, and that
we produce an equisatisfiable query Q' by eliminating if-then-else
terms in the way you suggest.  For example, an if-then-else term that
appears deep down in the parse tree of Q, for instance in a
subexpression of form

    (:or phi_1 (... (:ite phi_2 t_1 t_2) ...))

may give rise to a side-condition

    (:ite phi_2 (:eq c t_1) (:eq c t_2))

that appears as a top-level conjunct in Q'.  The structure of the
original query Q, makes it clear that the truth assignment for phi_2
(or at least of the particular occurrence of phi_2) is irrelevant to
the analysis of any partial truth assignment in which phi_1 has
already been assigned "true".  In Q' the relationship between the
points of occurrence of phi_1 and phi_2 is lost, or at very least
somewhat obscured.  This seems to me to be similar to the loss of
structural information that occurs when an arbitrary boolean formula
is transformed into CNF with the introduction of proxy variables for
subexpressions to avoid exponential blowup.

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

    ...
    (:iff
     phi_1
     (:forall (x_1 s_1)
      (:iff
       phi_2
       (:forall (x_2 s_2)
        ...
        (:iff
         phi_n
         (:forall (x_n s_n)
          ... 
          (:ite phi[x_1, ..., x_n] t_1[x_1, ..., x_n] t_2[x_1, ..., x_n])
          ...
         )
        )
        ...
       )
      )
     )
    )
    ...

where phi_1, ..., phi_n are formulas; x_1, ..., x_n are variables, 
s_1, ..., S_n are sort symbols; and where phi[x_1, ..., x_n], t_1[x_1, 
..., x_n], and t_2[x_1, ..., x_n] are a formula and two terms in 
which the variables x_1, ..., x_n occur free.  It is not at all clear 
to me what would be the best syntactic transformation to turn Q into 
an equisatisfiable formula containing no if-then-else terms, particularly 
if the goal is to do so "with no substantial loss of structural information". 

Regards,
--Jim
======================================================================