(** The solver: proof search over an admitted world.

    Functorized over {!World.WORLD} (decision 4): the standalone
    binary instantiates it with {!World.Standalone}; RNT instantiates
    it with its own catalog and links the same engine in-process.

    Execution is dynamic goal selection: at each step the engine
    runs any goal that is decidable at the current bindings, so
    conjunction stays honestly commutative and order on the page
    means nothing. A conjunction where no goal can ever run (an
    unbounded membership, an unbounded recursion) is rejected as a
    non-total plan, never attempted. Together with admission-time
    rule checking, this is what makes every accepted query
    terminate. *)

type error =
  | Non_total_plan of string list
      (** No remaining goal is decidable or residuatable; the
          relation names of the stuck goals, for the message. *)

val pp_error : Format.formatter -> error -> unit

(** A residual constraint: a membership goal that stayed
    underdetermined. It is decidable the moment its variables are
    ground; returning it is the honest answer to a satisfiable but
    open query. Only builtin membership residuates; searches never
    do. *)
type residual = string * Pattern.t Label.Map.t

val pp_residual : Format.formatter -> residual -> unit
(** Prints the constraint as the proposition it is, [[Rel l: t ...]]. *)

(** One answer: each free variable of the query resolved, plus the
    residual constraints the answer is conditioned on. Ground and
    residue-free in the common case. *)
type solution = {
  bindings : (string * Pattern.t) list;
  residue : residual list;
}

module Make (W : World.WORLD) : sig
  val solve : W.t -> World.expr -> (solution list, error) result
  (** All answers to the query, duplicates collapsed. Total: the
      world was admitted, so search terminates; the only failure is
      a plan the engine refuses to run. *)
end

module Standalone : sig
  val solve : World.Standalone.t -> World.expr -> (solution list, error) result
end