mc2 0.1 (latest) · OCaml Package

Main Interface for the Solver

type proof = Proof.t

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

Try and solves the current set of assumptions.

val pp_stats : t CCFormat.printer

Print stats

package mc2

Types

Main Type

Base operations