Something went wrong. Try again.
An implementation of the PubGrub version solving algorithm in OCaml.
Something went wrong. Try again.
2.0 kB · 51 lines
OCaml
at backup-main
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152(** The partial solution: the assignments the solver has accumulated so far. *)
module Make (N : Types.NAME) (V : Types.VERSION) : sig include module type of Types.Make (N) (V) module NameSet : Set.S with type elt = N.t
type assignment = | Decision of package | RootDecision | Derivation of term * incompatibility
type t
val empty : t
val add : t -> decision_level -> assignment -> t (** [add ps lvl a]: push [a] at decision level [lvl] onto [ps]. *)
val backtrack : t -> decision_level -> t * N.t list (** [backtrack ps level]: drop every assignment whose decision level exceeds [level]. Also returns the names whose constraints changed; all other names are unaffected. *)
val assignments : t -> (assignment * decision_level) list (** The assignments, newest first. *)
val name_range : t -> N.t -> bool * Ranges.t (** [name_range ps n]: [(has_pos, r)] where [r] is the intersection of all constraints on [n] and [has_pos] is true iff some assignment forces [n] to be selected. *)
val is_decided : t -> N.t -> bool val root_selected : t -> bool
val undecided_pos_names : t -> NameSet.t (** Names that have a Pos derivation but no Decision yet. Candidates for the next decision. *)
val term_status : t -> term -> term_status val incompatibility_status : t -> incompatibility -> incomp_status
val find_satisfier : t -> incompatibility -> ((assignment * decision_level) * decision_level) option (** The earliest assignment whose inclusion first makes [incomp] All_satisfied, together with the previous satisfier level: the decision level at which some prefix of the earlier assignments plus the satisfier first satisfies [incomp] (0 if the satisfier needs no prefix). [None] if [incomp] is not satisfied. *)
val pp_assignment : Format.formatter -> assignment -> unit val pp_assignments : Format.formatter -> (assignment * decision_level) list -> unit val assignment_name : assignment -> nameend