Theory solver

also: theory, explanation

The decision procedure plugged into a DPLL(T) core for one specific theory. Its interface is small: accept assertions, report consistent or inconsistent, and on inconsistency return a subset of the assertions that already conflict, because a smaller explanation becomes a stronger learned clause.

The decision procedure plugged into a DPLL(T) core. Its interface is deliberately narrow, which is what lets theories be swapped and combined:

module type THEORY = sig
  type t
  type atom
  val create : unit -> t
  val assert_atom : t -> atom -> bool -> unit
  (* None when consistent; Some conflicting subset otherwise *)
  val check : t -> atom list option
  val push : t -> unit          (* checkpoint, for backjumping *)
  val pop : t -> unit
end

Two requirements beyond correctness. It must be incremental, because the core asserts atoms one at a time and retracts them on every backjump, so re-deciding from scratch each call is not affordable. And it must explain: on failure it returns a subset of the assertions that already conflict, because the negation of that subset is the learned clause.

Combining theories is the part that is harder than it looks. Nelson-Oppen combines decision procedures for theories that share only equality, by having them exchange the equalities between shared variables that each can deduce, and it requires the theories to be stably infinite for the argument to go through.

DPLL(T) · Difference logic

Congruence closure · SMT

• Implementing SAT in OCaml Part 3From SAT to SMT: the DPLL(T) architecture, reusing conflict-driven learning for theory conflicts, and a union-find equality theory.