package mc2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Main for dimacs

package mc2

mc2.backend
- Mc2_backend
  - Backend_intf
    
    S
  - Dot
    
    Arg
    
    Default
    
    Make
    
    A
mc2.core
- Mc2_core
  - Actions
  - Atom
  - Bound_var
  - Builtins
  - Clause
  - Error
  - ID
    
    Smtlib
  - Lemma
    
    TC
  - Plugin
    
    Factory
    
    S
  - Proof
  - Service
    
    Key
    
    Registry
  - Solver
    
    Sat_state
    
    Unsat_state
  - Statement
  - Term
    
    Bool
    
    TC
    
    TERM_ALLOC
    
    TERM_ALLOC_OPS
    
    Term_allocator
    
    T
    
    Watch1
    
    Watch2
  - Tseitin
    
    Arg
    
    Make
    
    F
    
    S
  - Type
    
    Alloc
    
    T
    
    TC
    
    TY_ALLOC_OPS
  - Value
    
    TC
mc2.dimacs
- Mc2_dimacs
  - Plugin_sat
mc2.lra
- Mc2_lra
  - LE
    
    Infix
mc2.propositional
- Mc2_propositional
  - F
mc2.smtlib
- Mc2_smtlib
  - Make
    
    ARG
  - Typecheck
    
    Make
    
    ARG
mc2.uf
- Mc2_uf
mc2.unin_sort
- Mc2_unin_sort

Legend:
Library
Module
Module type
Parameter
Class
Class type

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

val plugin : Mc2_core.Plugin.Factory.t

val k_atom : (int -> Mc2_core.atom) Mc2_core.Service.Key.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

val solve : Mc2_core.Solver.t -> Mc2_core.Solver.res or_error

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