§ Implementing Nelson Oppen

§ Disjoint theories

• Two theories are disjoint of they do not share predicates and function symbols, except for $=$.

§ Ensuring Disjointness and Purification

• Transform a formula in $\Sigma_1 \cup \Sigma_2$ into an equisatisfiable formula $F_1 \land F_2$ with $F_1 \in T_1$ and $F_2 \in T_2$
• Introduce fresh symbols for shared subterms.
• Algorithmically, to purify a formula $f(x_1, \dots)$ to be in theory $T_1$:

repeat until fixpoint:
      u = gesym()
      Purify[f(..., t, ...)] => Purify[f(..., u, ...)] /\ u = t

• Consider example:

x + 2 == y, f(Store(A, x, 3)[y - 2]) != f(y - x + 1)

• Purify, introduce new constants:
• Purified:

Functions:  f(v1) != f(v2)
Arrays:     v1 == v3[v4], v3 == Store(x, y, v5)
Arithmetic: x + 2 == y, v2 == y - x + 1, v4 == y - 2, v5 == 2

§ Convex Theory

• Let $F$ be a conjunctive formula.
• Let $F \implies x_1 = y_1 \lor x_2 = y_2$.
• Then we must have $F \implies x_1 = y_1$ or $F = x_2 = y_2$.
• Generalize to $n$ disjuncts.
• Inutitively, if $F$ implies a disjunction of equalities, then it implies at least one equality.
• LIA is not convex: suppose $F = 1 \leq x \leq 2$. Then we have $F \implies x = 1 \lor x = 2$. But, $F$ does not imply either $x = 1$ or $x = 2$.
• Convexity reduces what we need to handle: If we want to show $x_1 = y_1 \lor x_2 = y_2$, we can try to prove each disjunct first.
• See that in the case of LIA, If we want $A \implies B$ to be true, if we view $A, B$ as sets, then we want $\lnot A \lor B$to be the whole space, which means that $B$ covers whatever $A$ used to cover, so we need $A \subseteq B$.
• Another way to look at the LIA thing: $A \implies B$ is us saying that $x \in A \implies x \in B$ for arbitrary $x$, and thus we need $A \subseteq B$!.
• Let us now view this in terms of $F \implies H_1 \lor H_2$.
• $F$ is a conjunctive formula, so it is geometricaly a convex set.
• $H_1, H_2$ are equalities of the form $x_i = y_i$, so they are hyperplanes.
• To have $F \implies H_1 \lor H_2$ be true, we need $F \subset H_1 \cup H_2$.
• We now want that $F \subset H_1 \cup H_2$, which can only happen if $F \subset H_1$ or $F \subset H_2$, since a convex set can be a subset of hyperplanes only if it is contained in any hyperplane! Otherwise, we can "interpolate" a point $x_1 \in H_1$ and $x_2 \in H_2$ and get a point $(x_1 + x_2) / 2$ that lies in neither.

§ Convex theory w/ Non Trivial Model is Stably Infinite

• Suppose a theory $T$ has a non-trivial model, and is convex.
• Then we need to show that it's stably infinite.
• Theory $T$ is stably infinite iff for every ground quantifier free formula $F$ that is satisfiable, there is an infinite model.
• So we are given a ground formaul $F$ that's true in some model $M$ of $T$, and we need to show that it's true in an infinite model.
• If the model $M$ is the trivial model $M = {*}$, then the formula $F$ must hold in a larger model (why?)
• Suppose size of $M \geq 2$.
• We will build an infinite model for $F$ by compactness.
• For every $n \in N$, we know that $M^{\log_2 n}$ will have cardinality greater than or equal to $n$.

§ References

• Simplification by cooperating decision procedures
• Programming Z3