package msat

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

package msat

msat
- Msat
  - Backend_intf
    
    S
  - Coq
    
    Arg
    
    Make
    
    A
    
    S
    
    H
    
    St
    
    Simple
    
    A
    
    S
    
    H
    
    St
  - Dedukti
    
    Arg
    
    Make
    
    A
    
    S
    
    H
    
    St
  - Dimacs
    
    Make
    
    Dummy
    
    St
    
    S
  - Dot
    
    Arg
    
    Default
    
    S
    
    H
    
    St
    
    Make
    
    A
    
    S
    
    H
    
    St
    
    Simple
    
    A
    
    S
    
    H
    
    St
  - Expr_intf
    
    S
    
    Formula
    
    Term
  - External
    
    Make
    
    Dummy
    
    Proof
    
    H
    
    St
    
    St
    
    Th
  - Formula_intf
    
    S
  - Internal
    
    Make
    
    Dummy
    
    Proof
    
    H
    
    St
    
    St
    
    Th
  - Log
  - Mcsolver
    
    Make
    
    Dummy
    
    E
    
    Formula
    
    Term
    
    Proof
    
    H
    
    St
    
    St
    
    Th
  - Plugin_intf
    
    S
  - Res
    
    Make
    
    H
    
    St
  - Res_intf
    
    S
    
    H
    
    St
  - Sat
    
    Expr
    
    Make
    
    Dummy
    
    Proof
    
    H
    
    St
    
    St
  - Solver
    
    DummyTheory
    
    F
    
    Make
    
    Dummy
    
    F
    
    Proof
    
    H
    
    St
    
    St
    
    Th
  - Solver_intf
    
    S
    
    Proof
    
    H
    
    St
    
    St
  - Solver_types
    
    McMake
    
    Dummy
    
    E
    
    Formula
    
    Term
    
    SatMake
    
    Dummy
    
    E
  - Solver_types_intf
    
    S
  - Theory_intf
    
    S
  - Tseitin
    
    Make
    
    F
  - Tseitin_intf
    
    Arg
    
    S

Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module Dummy : sig ... end

Signature

module St : sig ... end

module Proof : sig ... end

type atom = St.formula

type res =

| Sat of (St.term, St.formula) Solver_intf.sat_state
| Unsat of (St.clause, Proof.proof) Solver_intf.unsat_state

exception UndecidedLit

val assume : ?tag:int -> atom list list -> unit

val solve : ?assumptions:atom list -> unit -> res

val new_lit : St.term -> unit

val new_atom : atom -> unit

val unsat_core : Proof.proof -> St.clause list

val true_at_level0 : atom -> bool

val get_tag : St.clause -> int option

val export_dimacs : Format.formatter -> unit -> unit

val export_icnf : Format.formatter -> unit -> unit