if-then-else in SMT-LIB

[Shuvendu Lahiri]

Dear all,
	We would like to add a few words about Jim's comment about
if-then-else (ITE).

	We feel that it is helpful to have if \phi then t1 else t2 in
the language, at least for efficiency purpose. Here are a couple of reaons
that we have encountered in our work with UCLID.

	1. Eliminating ITEs by introducing auxiliary variables as
placeholders destroys the "positive equality" [Bryant,German,Velev]
property for the logic of Equality with Uninterpreted functions (EUF).
Positive equality has been crucial in several verification efforts and
would be nice to retain it.
	Intuitively, positive equality creates a worst case for the
validity checking problem. Suppose we are interested in proving the
validity of the following formula in unsorted first-order logic:

	ITE(b,f(x),f(y)) = g(z)

	Positive equality identifies that f(x),f(y),g(z) all appear under
positive polarity in the formula, hence it allows us to restrict the
values of f(x), f(y), g(z) to be DISTINCT, provided there is no functional
inconsistency (x=y => f(x) = f(y)). Thus the formula is transformed into a
validity preserving form:

	ITE(b,v1, ITE(x=y,vf1,vf2)) = vg1

	The next step is to assign DISTINCT values to x,y,vf1,vf2,vg1 (say
1,2,3,4,5 respectively). The formula immediately becomes false indicating
that the formula is not valid.

	If we think of removing the ITE in the initial formula, then the
resulting formula would become:

	(b=> t1 = f(x)) & (~b => t1 = f(y)) => t1 = g(z)

	Removing the function application gives:

	(b => t1 = vf1) & (~b => t1 = ITE(x=y,vf1,vf2)) => t1 = vg1

	removal of ITE gives

	(b => t1 = vf1) & (~b => t1 = t2) & (x=y => t2 = vf1) & (x!=y =>
t2 =vf2)  => t1 = vg1


	We can no longer assign DISTINCT values to t1,t2,vf1,vf2,vg1
because the resultant formula becomes valid. It is not clear how to
exploit positive equality readily with this transformation.


	2. The second reason for keeping ITE would be to maintain the
structure in the formula, as Jim pointed out. We have found that the
efficiency of the solver
changes by orders of magnitude (for worse), when we use the syntactic
removal of ITE. We get much better performance with SAT-solvers, even when
we take the path to produce an potentially exponentially large formula, by
multiplying out ITEs.
	ITE(b1,T1,T2) = ITE(b2,T3,T4) --> b1 & b2 & T1 = T3 | ~b1 & b2 &
T2 = T3 ...

	Making use of sharing and dag simplification often reduces the
formula size, and we rarely see an exponential blowup on our benchmarks.


Thanks,
Shuvendu and Sanjit





---------- Forwarded message ----------
Date: Fri, 15 Aug 2003 15:03:18 -0700
From: Jim Saxe <Jim.Saxe at hp.com>
To: Cesare Tinelli <tinelli at cs.uiowa.edu>, Silvio.Ranise at loria.fr
Cc: smt-disc at cs.uiowa.edu, GNelson at hp.com, Rajeev.Joshi at hp.com,
     c at cormacflanagan.com
Subject: if-then-else in SMT-LIB

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
======================================================================