Module `Mc2_core.Solver`Source

Main Interface for the Solver

Sourcetype proof = Proof.t

Sourcetype nonrec atom

The type of atoms given by the module argument for formulas

Types

Main Type

Sourcetype t

The type of a solver

Base operations

Sourceval create : plugins:Plugin.Factory.t list -> unit -> t

Create a new solver with the given plugins

Sourceval plugins : t -> Plugin.t Iter.t

Obtain the current plugins

Sourceval services : t -> Service.Registry.t

Sourceval get_service : t -> 'a Service.Key.t -> 'a option

Obtain a service by its key

Sourceval get_service_exn : t -> 'a Service.Key.t -> 'a

Obtain a service by its key, or fail

Sourceval 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.

Sourceval 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.

Sourceval unsat_core : t -> proof -> Mc2_core__.Solver_types.clause list

Returns the unsat core of a given proof.

Sourceval 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

Sourcetype '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

Sourceval clause_sets : t -> Mc2_core__.Solver_types.clause clause_sets

Iterate on current sets of clauses

Sourcetype 'a state

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

Sourceval state_solver : _ state -> t

Get the solver back from a solver.

Sourceexception UndecidedLit of Mc2_core__.Solver_types.term

Exception raised by the evaluating functions when a literal has not yet been assigned a value.

Sourceexception Out_of_time

Sourceexception Out_of_space

Sourcemodule Sat_state : sig ... end

Sourcemodule Unsat_state : sig ... end

Sourcetype 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

Source

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.

Sourceval pp_stats : t CCFormat.printer

Print stats

Install

Dune Dependency

Authors

Maintainers

Sources

doc/mc2.core/Mc2_core/Solver/index.html

Module `Mc2_core.Solver`Source

Types

Main Type

Base operations

package mc2

Install

Dune Dependency

Authors

Maintainers

Sources

doc/mc2.core/Mc2_core/Solver/index.html

Module Mc2_core.SolverSource

Types

Main Type

Base operations

Module `Mc2_core.Solver`Source