package msat

You can search for identifiers within the package.

in-package search v0.2.0

package msat

msat
- Msat
  - Cc
    
    Make
    
    T
  - Cnf
    
    S
  - Dedukti
    
    Arg
    
    Make
    
    A
    
    S
    
    St
  - Dot
    
    Arg
    
    Make
    
    A
    
    S
    
    St
  - Expr
    
    Formula
    
    Term
  - Expr_intf
    
    S
    
    Formula
    
    Term
  - External
    
    Make
    
    Dummy
    
    Proof
    
    St
    
    St
    
    Th
  - Formula_intf
    
    S
  - Internal
    
    Make
    
    Dummy
    
    Proof
    
    St
    
    St
    
    Th
  - Log
  - Mcsat
    
    Make
    
    Dedukti
    
    Dot
    
    Dummy
    
    Proof
    
    St
    
    St
    
    Tsmt
    
    CC
    
    M
  - Mcsolver
    
    Make
    
    Dummy
    
    E
    
    Formula
    
    Term
    
    Proof
    
    St
    
    St
    
    Th
  - Plugin_intf
    
    S
  - Res
    
    Make
    
    St
  - Res_intf
    
    S
    
    St
  - Sat
    
    Fsat
    
    Make
    
    Dummy
    
    Proof
    
    St
    
    St
    
    Tseitin
  - Sig
    
    OrderedType
  - Smt
    
    Make
    
    Dummy
    
    Proof
    
    St
    
    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
    
    S
  - Unionfind
    
    Make
    
    T

Legend:
Library
Module
Module type
Parameter
Class
Class type

module M : sig ... end

module CC : sig ... end

type term = Fsmt.Term.t

type formula = Fsmt.t

type proof = unit

type level = {

cc : CC.t;
assign : (term * int) M.t;

}

val dummy : level

val env : level ref

val current_level : unit -> level

val to_clause : (Fsmt.var * Fsmt.var * Fsmt.var list) -> Fsmt.t list

val assume : 
  (M.key, Fsmt.formula, 'a) Plugin_intf.slice ->
  (Fsmt.t, unit) Plugin_intf.res

val backtrack : level -> unit

val assign : String.t -> String.t

val iter_assignable : (Fsmt.var -> unit) -> Fsmt.formula -> unit

val max : int -> int -> int

val eval : Fsmt.formula -> Plugin_intf.eval_res

val if_sat : 'a -> unit