package mc2

  1. Overview
  2. Docs
On This Page
  1. Main for dimacs

Main for dimacs

This library provides a parser for DIMACS files, to represent SAT problems.

http://www.satcompetition.org/2009/format-benchmarks2009.html

module Plugin_sat : sig ... end
type 'a or_error = ('a, string) CCResult.t

Key to build atoms

val parse : Mc2_core.Service.Registry.t -> string -> Mc2_core.atom list list or_error

Parse a file into a list of clauses.

  • parameter registry

    used to build atoms from integers, see k_atom

Solve a problem

val process : ?gc:bool -> ?restarts:bool -> ?dot_proof:string -> ?pp_model:bool -> ?check:bool -> ?time:float -> ?memory:float -> ?progress:bool -> ?switch:Mc2_core.Util.Switch.t -> Mc2_core.Solver.t -> Mc2_core.atom list list -> unit or_error

Add clauses to solver, solve, and prints the results.

  • parameter check

    check proof/model

  • parameter progress

    print progress bar

  • parameter dot_proof

    file into which to print the proof