package msat

You can search for identifiers within the package.

in-package search v0.2.0

msat
- Msat
  - Backend_intf
    
    S
  - Dedukti
    
    Arg
    
    Make
    
    A
    
    S
    
    St
  - Dot
    
    Arg
    
    Make
    
    A
    
    S
    
    St
  - Expr_intf
    
    S
    
    Formula
    
    Term
  - External
    
    Make
    
    Dummy
    
    Proof
    
    St
    
    St
    
    Th
  - Formula_intf
    
    S
  - Internal
    
    Make
    
    Dummy
    
    Proof
    
    St
    
    St
    
    Th
  - Log
  - Mcsolver
    
    Make
    
    Dummy
    
    E
    
    Formula
    
    Term
    
    Proof
    
    St
    
    St
    
    Th
  - Plugin_intf
    
    S
  - Res
    
    Make
    
    St
  - Res_intf
    
    S
    
    St
  - Solver
    
    DummyTheory
    
    F
    
    Make
    
    Dummy
    
    F
    
    Proof
    
    St
    
    St
    
    Th
  - Solver_intf
    
    S
    
    Proof
    
    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

type eval_res =

| Valued of bool * int
| Unknown

type (!'formula, !'proof) res =

| Sat
| Unsat of 'formula list * 'proof

type (!'term, !'formula) assumption =

| Lit of 'formula
| Assign of 'term * 'term * int

type (!'term, !'formula, !'proof) slice = {

start : int;
length : int;
get : int -> ('term, 'formula) assumption;
push : 'formula list -> 'proof -> unit;
propagate : 'formula -> int -> unit;

}

module type S = sig ... end