• OCaml logo OCaml logo
  • Learn
  • Packages
  • Community
  • Blog
  • Playground
  • Learn
  • Packages
  • Community
  • Blog
  • Playground
  • Get started
  • msat
  • Documentation
  • msat.backtrack lib
  • Msat_backtrack Module
package msat
  • msat
    • Msat
      • Make_cdcl_t
        • 1-Th
          • Formula
        • Atom
        • Clause
          • Tbl
        • Proof
          • Tbl
        • Value
      • Make_mcsat
        • 1-Th
          • Formula
          • Term
          • Value
        • Atom
        • Clause
          • Tbl
        • Proof
          • Tbl
        • Value
      • Make_pure_sat
        • 1-Th
          • Formula
        • Atom
        • Clause
          • Tbl
        • Proof
          • Tbl
        • Value
      • Solver_intf
        • EXPR
          • Formula
          • Term
          • Value
        • FORMULA
        • PLUGIN_CDCL_T
          • Formula
        • PLUGIN_MCSAT
          • Formula
          • Term
          • Value
        • PLUGIN_SAT
          • Formula
        • PROOF
          • Tbl
        • S
          • Atom
          • Clause
            • Tbl
          • Formula
          • Proof
            • Tbl
          • Term
          • Value
  • msat.backend
    • Msat_backend
      • Backend_intf
        • S
      • Coq
        • Arg
        • Make
          • 1-S
            • Atom
            • Clause
              • Tbl
            • Formula
            • Proof
              • Tbl
            • Term
            • Value
          • 2-A
        • Simple
          • 1-S
            • Atom
            • Clause
              • Tbl
            • Formula
            • Proof
              • Tbl
            • Term
            • Value
          • 2-A
      • Dedukti
        • Arg
        • Make
          • 1-S
            • Atom
            • Clause
              • Tbl
            • Formula
            • Proof
              • Tbl
            • Term
            • Value
          • 2-A
      • Dot
        • Arg
        • Default
          • 1-S
            • Atom
            • Clause
              • Tbl
            • Formula
            • Proof
              • Tbl
            • Term
            • Value
        • Make
          • 1-S
            • Atom
            • Clause
              • Tbl
            • Formula
            • Proof
              • Tbl
            • Term
            • Value
          • 2-A
        • Simple
          • 1-S
            • Atom
            • Clause
              • Tbl
            • Formula
            • Proof
              • Tbl
            • Term
            • Value
          • 2-A
  • msat.backtrack
    • Msat_backtrack
      • Ref
  • msat.sat
    • Msat_sat
      • Atom
      • Clause
        • Tbl
      • Formula
      • Int_lit
      • Proof
        • Tbl
      • Term
      • Value
  • msat.tseitin
    • Msat_tseitin
      • Arg
      • Make
        • 1-F
      • S
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Ref : sig ... end

Footer

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS

About Us

  • Industrial Users
  • Academic Users
  • Why OCaml

Resources

  • Get Started
  • Language Docs
  • Books
  • Releases

Community

  • Blog
  • Jobs

Policies

  • Carbon Footprint
  • Governance
  • Privacy
  • Code of Conduct