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
  - Make_cdcl_t
    
    Atom
    
    Clause
    
    Tbl
    
    Proof
    
    Tbl
    
    Th
    
    Formula
    
    Value
  - Make_mcsat
    
    Atom
    
    Clause
    
    Tbl
    
    Proof
    
    Tbl
    
    Th
    
    Formula
    
    Term
    
    Value
    
    Value
  - Make_pure_sat
    
    Atom
    
    Clause
    
    Tbl
    
    Proof
    
    Tbl
    
    Th
    
    Formula
    
    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
    
    A
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
    
    Simple
    
    A
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
  - Dedukti
    
    Arg
    
    Make
    
    A
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
  - Dot
    
    Arg
    
    Default
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
    
    Make
    
    A
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
    
    Simple
    
    A
    
    S
    
    Atom
    
    Clause
    
    Tbl
    
    Formula
    
    Proof
    
    Tbl
    
    Term
    
    Value
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
    
    F
  - S

Legend:
Library
Module
Module type
Parameter
Class
Class type

This functor provides an implementation of Tseitin's CNF conversion.

CNF conversion

This modules allows to convert arbitrary boolean formulas into CNF.

Parameters

module F : Arg

Signature

type atom = F.t

The type of atomic formulas.

type t

The type of arbitrary boolean formulas. Arbitrary boolean formulas can be built using functions in this module, and then converted to a CNF, which is a list of clauses that only use atomic formulas.

val f_true : t

The true formula, i.e a formula that is always satisfied.

val f_false : t

The false formula, i.e a formula that cannot be satisfied.

val make_atom : atom -> t

make_atom p builds the boolean formula equivalent to the atomic formula p.

val make_not : t -> t

Creates the negation of a boolean formula.

val make_and : t list -> t

Creates the conjunction of a list of formulas. An empty conjunction is always satisfied.

val make_or : t list -> t

Creates the disjunction of a list of formulas. An empty disjunction is never satisfied.

val make_xor : t -> t -> t

make_xor p q creates the boolean formula "p xor q".

val make_imply : t -> t -> t

make_imply p q creates the boolean formula "p implies q".

val make_equiv : t -> t -> t

make_equiv p q creates the boolena formula "p is equivalent to q".

val make_cnf : t -> atom list list

make_cnf f returns a conjunctive normal form of f under the form: a list (which is a conjunction) of lists (which are disjunctions) of atomic formulas.

val pp : Format.formatter -> t -> unit

print fmt f prints the formula on the formatter fmt.