package mc2

  1. Overview
  2. Docs

Main Interface for the Solver

type proof = Proof.t
type nonrec atom

The type of atoms given by the module argument for formulas


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 = {
  1. cs_hyps : 'clause Mc2_core__.Vec.t;
  2. cs_history : 'clause Mc2_core__.Vec.t;
  3. 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 =
  1. | Sat of Sat_state.t

    Returned when the solver reaches SAT

  2. | 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:Mc2_core__.Util.Switch.t -> t -> res

Try and solves the current set of assumptions.

val pp_stats : t CCFormat.printer

Print stats