package mc2

  1. Overview
  2. Docs
package mc2
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Mc2_core.SolverSource

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 = {
  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

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 =
  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

Sourceval 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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct