Module `Mc2_core.Solver`

Main Interface for the Solver

type proof = Proof.t
type nonrec atom = Mc2_core__.Solver_types.atom: The type of atoms given by the module argument for formulas

Types

Main Type

type t: The type of a solver

Base operations

val create : plugins:Plugin.Factory.t list -> unit -> t: Create a new solver with the given plugins

val plugins : t -> Plugin.t Iter.t: Obtain the current plugins

val services : t -> Service.Registry.t
val get_service : t -> 'a Service.Key.t -> 'a option: Obtain a service by its key

val get_service_exn : t -> 'a Service.Key.t -> 'a: Obtain a service by its key, or fail

val assume : t -> ?⁠tag:int -> atom list list -> unit: Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place.

val add_term : t -> Mc2_core__.Solver_types.term -> unit: Add a new literal (i.e term) to the solver. This term will be decided on at some point during solving, whether it appears in clauses or not.

val unsat_core : t -> proof -> Mc2_core__.Solver_types.clause list: Returns the unsat core of a given proof.

val true_at_level0 : t -> atom -> bool: true_at_level0 a returns true if a was proved at level0, i.e. it must hold in all models

type 'clause clause_sets = { cs_hyps : 'clause Mc2_core__.Vec.t; cs_history : 'clause Mc2_core__.Vec.t; cs_local : 'clause Mc2_core__.Vec.t; }: Current state of the SAT solver

val clause_sets : t -> Mc2_core__.Solver_types.clause clause_sets: Iterate on current sets of clauses

type 'a state: Opaque view on the solver in a given state, with a phantom parameter to indicate in which state it is

val state_solver : _ state -> t: Get the solver back from a solver.

exception UndecidedLit of Mc2_core__.Solver_types.term: Exception raised by the evaluating functions when a literal has not yet been assigned a value.

exception Out_of_time
exception Out_of_space

module Sat_state : sig ... end

module Unsat_state : sig ... end

type res = | Sat of Sat_state.t Returned when the solver reaches SAT | Unsat of Unsat_state.t Returned when the solver reaches UNSAT: Result type for the solver

val solve : ?⁠gc:bool -> ?⁠restarts:bool -> ?⁠time:float -> ?⁠memory:float -> ?⁠progress:bool -> ?⁠assumptions:atom list -> ?⁠switch:Util.Switch.t -> t -> res: Try and solves the current set of assumptions.

val pp_stats : t CCFormat.printer: Print stats