CS292C-9: Computer-Aided Reasoning for Software
Lecture 9: Combining Theories in SMT (Nelson–Oppen Combination)

by Yu Feng

Lecture Roadmap
Motivation
Why combine theories?
Nelson–Oppen Framework
Signature, purification, shared constants
Algorithm
Convex vs non-convex theories
Examples & Extensions
Limitations and practical applications
Theory of Linear Integer and Real Arithmetic
Signature (Σ)
  • Domain: Integers (ℤ) or reals (ℝ)
  • Arithmetic operations: multiplication by constants, addition (+), subtraction (-)
  • Predicates: equality (=), inequality (≤)
  • Expanded with constant symbols: x, y, z, ...
Examples
Linear Real Arithmetic (LRA)
  • 2x + 3y - z ≤ 5
  • 4.5x - 2y = 7.3
  • x ≥ 0 ∧ y ≥ 0 ∧ x + y ≤ 1
Linear Integer Arithmetic (LIA)
  • 3x + 2y - 5z = 7
  • x ≥ 0 ∧ y ≥ 0 ∧ 2x + 3y = 10
Theory of Linear Integer and Real Arithmetic
Signature (Σ)
  • Domain: Integers (ℤ) or reals (ℝ)
  • Arithmetic operations: multiplication by constants, addition (+), subtraction (-)
  • Predicates: equality (=), inequality (≤)
  • Expanded with constant symbols: x, y, z, ...
This theory allows us to express and reason about linear constraints over integer or real variables, forming the foundation for many practical verification problems.
Linear Integer Arithmetic (LIA)
NP-complete
Linear Real Arithmetic (LRA)
Solvable in polynomial time
Why Combine Theories?
Consider this formula: 1 ≤ x ∧ x ≤ 2 ∧ f(x) ≠ f(1) ∧ f(x) ≠ f(2)
This formula cannot be handled by any single theory because it contains:
  • Linear inequalities (1 ≤ x ∧ x ≤ 2) from Linear Integer/Real Arithmetic
  • Uninterpreted functions (f(x) ≠ f(1) ∧ f(x) ≠ f(2)) from Equality with Uninterpreted Functions
To solve this formula, we need to combine theories: {T_=} ∪ {T_{LIA}} with the theory of uninterpreted functions. This is the fundamental motivation for theory combination frameworks.
The Challenge
Combining theories is a fundamental problem in SMT solving:
Decidability Issue
Even when theories T₁ and T₂ are individually decidable, their combination T₁ ∪ T₂ may not be decidable in general.
Nelson-Oppen Approach
Nelson-Oppen framework provides restrictions under which the combination of decidable theories remains decidable.
When Does Nelson–Oppen Work?
Decidable
Both theories must be decidable, quantifier-free conjunctive fragments
Shared symbols
Equality (=) is the only interpreted symbol
Signature intersection
Σ1 ∩ Σ2 = { = }
Stably infinite
Both theories must be stably infinite
What is Stably Infinite?
Definition
A theory T is stably infinite if for every satisfiable {Σ_T} -formula F, there exists a T-model that satisfies F and has a universe of infinite cardinality.
In simpler terms: If a formula is satisfiable in the theory, it must be satisfiable with an infinite domain.
Examples
  • EUF (Equality with Uninterpreted Functions) ✅
  • Arrays ✅
  • LRA (Linear Real Arithmetic) ✅
  • LIA (Linear Integer Arithmetic) ✅
  • {Σ_T} : {a,b,=}, {A_T} : ∀x. x=a ∨ x=b ❌
Overview of Nelson-Oppen
1
SMT formula F
Starting point
2
Purification
Split into F₁ (T₁) ∧ F₂ (T₂)
3
Equality Propagation
T₁ Solver ⇄ T₂ Solver
4
Result
SAT or UNSAT
Phase 1: Purification Explained
Purification transforms a (Σ₁ ∪ Σ₂)-formula F into an equisatisfiable formula F₁ ∧ F₂ with F₁ in T₁ and F₂ in T₂ through iterative variable introductions.
Purification Algorithm
Repeat until fix point:
  1. If f is in {T_i} and term t is not, introduce fresh variable u:
    F[f(...,t,...)] ⟿ F[f(...,u,...)] ∧ u = t
  1. If predicate p is in {T_i} and t is not, introduce fresh v:
    F[p(...,t,...)] ⟿ F[p(...,v,...)] ∧ v = t
Example
Original: x ≤ f(x) + 1
Step 1: Since f is in EUF but x is shared:
x ≤ u + 1 ∧ f(x) = u
Step 2: Since + is in LIA but f(x) is not:
x ≤ u + 1 ∧ u =f(x)
Final Result
F₁ (EUF): u = f(x)
F₂ (LIA): x ≤ u + 1
The purified formula F₁ ∧ F₂ is equisatisfiable to the original formula, with each subformula purely in its respective theory.
Purification Example
This example demonstrates how a mixed formula is purified into theory-specific parts:
1
Original Formula
f(f(x) − f(y)) ≠ f(z) ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z
2
Introduce Variables
w₁ = f(x), w₂ = f(y), w₃ = w₁ − w₂
3
Split Theories
F₁: f(w₃) ≠ f(z), w₁ = f(x), w₂ = f(y)
F₂: w₃ = w₁ − w₂, x ≤ y, y + z ≤ x, 0 ≤ z
A constant is shared if it occurs in both F₁ and F₂
Shared: {w₃, w₁, w₂, x, y, z} Local: {}
Phase 2: Equality Propagation
After purification, theory solvers share equality info between theories to find a solution together.
Convex Theories ✅
Theories that can show all valid solutions using only equalities (e.g., LRA, EUF).
Non-convex Theories ❌
Theories that need "or" statements to express solutions (e.g., LIA).
Convexity
Definition
A theory T is convex if for every conjunctive formula F: If F ⇒ x₁=y₁ ∨...∨ xₙ=yₙ for n>1, then F⇒xᵢ=yᵢ for some i∈{1,...,n}
Convex Theories
EUF ✅, LRA ✅
Non-convex Theories
LIA ❌
1≤ x ∧ x ≤ 2 ⇒ x = 1 ∨ x = 2
but not 1≤ x ∧ x ≤ 2 ⇒ x = 1
not 1≤ x ∧ x ≤ 2 ⇒ x = 2
If F implies a disjunction of equalities, then it also implies at least one of the equalities.
Equality Propagation Loop
The Nelson-Oppen procedure for convex theories:
NELSON-OPPEN-CONVEX(F)
1. Purify F into F₁ ∧ F₂
2. Run T₁-solver on F₁ and T₂-solver 
   on F₂ and return UNSAT if either is
   unsatisfiable
3. If there are shared constants x and
   y such that F1 ⇒ x=y but F2 does not
   - 3.1. F2 ← F2 ∧ x=y
   - 3.2. Go to step 2.
4. Return SAT
This algorithm iteratively propagates equalities between theory solvers until reaching a fixed point or determining unsatisfiability.
Key Takeaways
Nelson–Oppen Framework
Theory combination foundation
Requirements
Decidable, stably infinite, disjoint signatures, convexity
Core Mechanism
Purification + equality propagation
Practical Use
Real SMT solvers extend this framework
What's Next?
1
DPLL(T) internals
Core SMT solving algorithm
2
Midterm will be coming next Monday
3
Project check-in
Homework progress review