Nelson–Oppen combination

The Nelson–Oppen method combines decision procedures for separate theories into one for their union^[1]. Verification conditions routinely mix theories: a single formula may contain arithmetic, uninterpreted functions, arrays and datatypes, while decision procedures are written for one theory each. Nelson–Oppen requires that the theories share no function or predicate symbols except equality. It purifies the input so that each literal belongs to one theory, introducing variables for subterms that cross from one theory into another; the only connection left between the parts is that they share some variables. The procedures then need to agree only on which shared variables are equal. For convex theories, each procedure reports the equalities between shared variables that its part entails and passes them to the others until the parts are inconsistent or no new equalities appear; in general, the procedures must be tried on each possible arrangement of the shared variables into equal and distinct ones^[2]. Greg Nelson and Derek Oppen published the method in 1979^[1]. It is the basis of theory combination in SMT solvers.

§ 01

Purification

A term is pure if all its symbols come from one theory. Purification repeatedly replaces a maximal subterm that belongs to a different theory than its context by a fresh variable $v$ and adds the equation $v = t$ . The result is an equisatisfiable conjunction $φ_{1} \land φ_{2}$ with $φ_{i}$ in the language of theory $T_{i}$ . For example, $f (x + 1) \neq = f (y)$ becomes $v = x + 1$ for arithmetic and $f (v) \neq = f (y)$ for uninterpreted functions, sharing $v$ and $y$ .

The example x ≤ y ∧ y ≤ x ∧ f(x) ≠ f(y). After purification, arithmetic entails x = y and passes it on; with it, congruence closure derives f(x) = f(y), contradicting the disequation.

§ 02

Equality propagation

A theory is convex if, whenever a conjunction of its literals entails a disjunction of equalities between variables, it entails one of them. Linear real arithmetic and equality with uninterpreted functions are convex. For convex theories, the procedures can simply exchange entailed equalities: each theory solver reports the equalities between shared variables that its part entails, the other adds them, and this repeats. The input is unsatisfiable if some part becomes inconsistent, and satisfiable if the exchange stops with both parts consistent^[1]^[2]. With a polynomial procedure for each convex theory, the combination is polynomial.

Nelson–Oppen for difference logic and uninterpreted functions: each side reports the equalities between shared variables that it entails.

(* Nelson–Oppen for difference logic and uninterpreted functions. After
   purification each literal belongs to one theory, and the theories share
   variables. Shared variables are named by strings; in the EUF part they
   are constants. *)
let euf_var v = Euf.Const v
 
(* Does difference logic entail x = y? Only if x - y <= -1 and y - x <= -1
   are each inconsistent with the constraints (the integer negations of
   x = y, one side at a time). *)
let dl_entails_eq cs x y =
  let inconsistent extra = match Dl.check (extra :: cs) with Error _ -> true | Ok _ -> false in
  inconsistent { Dl.x; y; c = -1 } && inconsistent { Dl.x = y; y = x; c = -1 }
 
let euf_entails_eq lits x y =
  let eqs = List.filter_map (fun (e, b) -> if b then Some e else None) lits in
  Euf.implied eqs (euf_var x) (euf_var y)
 
(* The deterministic loop for convex theories: each theory reports the
   equalities between shared variables that it entails, and they are
   passed to the other, until one theory is inconsistent or nothing new
   is found. *)
let combine ~shared (dl : Dl.atom list) (euf : (Euf.Theory.atom * bool) list) =
  let pairs = List.concat_map (fun x -> List.filter_map (fun y -> if x < y then Some (x, y) else None) shared) shared in
  let rec loop dl euf =
    match Dl.check dl, Euf.Theory.check euf with
    | Error _, _ -> print_endline "  arithmetic: inconsistent"; false
    | _, Error _ -> print_endline "  uninterpreted functions: inconsistent"; false
    | Ok _, Ok () ->
      let known (x, y) = euf_entails_eq euf x y && dl_entails_eq dl x y in
      let from_dl = List.filter (fun (x, y) -> not (known (x, y)) && dl_entails_eq dl x y) pairs in
      let from_euf = List.filter (fun (x, y) -> not (known (x, y)) && euf_entails_eq euf x y) pairs in
      if from_dl = [] && from_euf = [] then (print_endline "  no new equalities: satisfiable"; true)
      else begin
        List.iter (fun (x, y) -> Printf.printf "  arithmetic entails %s = %s\n" x y) from_dl;
        List.iter (fun (x, y) -> Printf.printf "  uninterpreted functions entail %s = %s\n" x y) from_euf;
        let dl = dl @ List.concat_map (fun (x, y) -> [ { Dl.x; y; c = 0 }; { Dl.x = y; y = x; c = 0 } ]) from_euf in
        let euf = euf @ List.map (fun (x, y) -> ((euf_var x, euf_var y), true)) from_dl in
        loop dl euf
      end
  in
  loop dl euf

The example of the figure, and the same without y ≤ x.

open Euf
 
(* x <= y  and  y <= x  and  f(x) <> f(y), purified: the arithmetic part
   is x - y <= 0 and y - x <= 0, the functional part f(x) <> f(y). *)

Running it.

x <= y, y <= x, f(x) <> f(y):
  arithmetic entails x = y
  uninterpreted functions: inconsistent
x <= y, f(x) <> f(y):
  no new equalities: satisfiable

§ 03

Non-convex theories

Integer arithmetic is not convex: $1 \leq x \leq 2$ entails $x = 1 \lor x = 2$ but neither equality alone. Exchanging entailed equalities is then incomplete. The general method guesses an arrangement, a partition of the shared variables into classes of equal variables, and checks each theory's part together with the equalities within classes and the disequalities between them; the input is satisfiable if and only if some arrangement is consistent with every part^[1]^[3]. The number of arrangements is the Bell number of the number of shared variables, and Oppen showed that the combination problem becomes NP-hard in general, even when each theory is polynomial^[2].

Over the integers, 1 ≤ x ≤ 2, f(x) ≠ f(1) and f(x) ≠ f(2): equality propagation against guessing arrangements.

open Euf
 
(* Over the integers: 1 <= x <= 2, f(x) <> f(1), f(x) <> f(2). With a
   zero variable z and constants one = 1 and two = 2, all as shared
   variables. Arithmetic entails x = one or x = two, but neither alone. *)
let dl = [ { Dl.x = "z"; y = "x"; c = -1 }; { Dl.x = "x"; y = "z"; c = 2 };
           { Dl.x = "one"; y = "z"; c = 1 }; { Dl.x = "z"; y = "one"; c = -1 };
           { Dl.x = "two"; y = "z"; c = 2 }; { Dl.x = "z"; y = "two"; c = -2 } ]
let f v = App ("f", [ Const v ])
let euf = [ ((f "x", f "one"), false); ((f "x", f "two"), false) ]
let shared = [ "x"; "one"; "two" ]
 
(* All partitions of a list: the arrangements of the shared variables. *)
let rec partitions = function
  | [] -> [ [] ]
  | x :: rest ->
    List.concat_map (fun p ->
        ([ x ] :: p) :: List.mapi (fun i _ -> List.mapi (fun j b -> if i = j then x :: b else b) p) p)
      (partitions rest)
 
(* An arrangement as equalities and disequalities between shared variables. *)
let constraints arr =
  let block v = List.find (List.mem v) arr in
  List.concat_map (fun x -> List.filter_map (fun y ->
      if x < y then Some (x, y, block x == block y) else None) shared) shared
 
let dl_with arr =
  (* a disequality is a disjunction; try every way of choosing a side *)
  let eqs, diseqs = List.partition (fun (_, _, e) -> e) (constraints arr) in
  let base = dl @ List.concat_map (fun (x, y, _) -> [ { Dl.x; y; c = 0 }; { Dl.x = y; y = x; c = 0 } ]) eqs in
  let rec try_ acc = function
    | [] -> (match Dl.check acc with Ok _ -> true | Error _ -> false)
    | (x, y, _) :: rest -> try_ ({ Dl.x; y; c = -1 } :: acc) rest || try_ ({ Dl.x = y; y = x; c = -1 } :: acc) rest in
  try_ base diseqs
 
let euf_with arr =
  let lits = List.map (fun (x, y, e) -> ((Const x, Const y), e)) (constraints arr) in
  match Theory.check (euf @ lits) with Ok () -> true | Error _ -> false

Running it.

the deterministic loop:
  no new equalities: satisfiable
guessing arrangements:
  x | one | two      arithmetic false functions true
  x = one | two      arithmetic true  functions false
  one | x = two      arithmetic true  functions false
  x | one = two      arithmetic false functions true
  x = one = two      arithmetic false functions false

Equality propagation wrongly finds the formula satisfiable, since neither theory entails any single equality. Enumerating the five arrangements of $x$ , $1$ and $2$ shows that each is rejected by one theory or the other, so the formula is unsatisfiable.

§ 04

Correctness conditions

The method is sound for any theories, but complete only under conditions. The signatures must be disjoint apart from equality, and each theory must be stably infinite: every quantifier-free formula satisfiable in the theory must be satisfiable in a model with infinitely many elements. The condition ensures that the models of the separate parts, which agree on the shared variables, can be taken to have the same size and merged into one model of the union^[1]^[3]. Tinelli and Harandi gave a clean proof of correctness in 1996^[3]. Theories over finite domains, such as fixed-width bit-vectors, are not stably infinite, and combining them requires further care, for instance the conditions of shiny or polite theories^[6]^[7].

§ 05

In SMT solvers

Inside DPLL(T), the choice of an arrangement can be delegated to the SAT solver. Delayed theory combination introduces Boolean atoms for the equalities between shared variables and lets the search decide them like any other atom, each theory solver checking its part together with those decisions^[8]. Model-based theory combination, used in Z3, lets each theory solver build a candidate model and propagates only the equalities that hold in it, repairing the model when another theory disagrees^[9]. Both avoid enumerating arrangements explicitly.

§ 06

History

Nelson and Oppen introduced the method in 1979 for the Stanford Pascal Verifier, as a way to build a simplifier from cooperating decision procedures^[1]. Oppen analyzed its complexity and the role of convexity in 1980^[2]. Shostak proposed an alternative in 1978 and 1984 for theories with canonizers and solvers, which combines them more tightly^[4]; its correctness was debated until Rueß and Shankar gave a corrected account in 2001^[5]. The conditions for completeness were clarified in the 1990s and 2000s^[3]^[6]^[7], and the integration of combination into DPLL(T) produced delayed and model-based combination^[8]^[9].