package mc2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

package mc2

mc2.backend
- Mc2_backend
  - Backend_intf
    
    S
  - Dot
    
    Arg
    
    Default
    
    Make
    
    A
mc2.core
- Mc2_core
  - Actions
  - Atom
  - Bound_var
  - Builtins
  - Clause
  - Error
  - ID
    
    Smtlib
  - Lemma
    
    TC
  - Plugin
    
    Factory
    
    S
  - Proof
  - Service
    
    Key
    
    Registry
  - Solver
    
    Sat_state
    
    Unsat_state
  - Statement
  - Term
    
    Bool
    
    TC
    
    TERM_ALLOC
    
    TERM_ALLOC_OPS
    
    Term_allocator
    
    T
    
    Watch1
    
    Watch2
  - Tseitin
    
    Arg
    
    Make
    
    F
    
    S
  - Type
    
    Alloc
    
    T
    
    TC
    
    TY_ALLOC_OPS
  - Value
    
    TC
mc2.dimacs
- Mc2_dimacs
  - Plugin_sat
mc2.lra
- Mc2_lra
  - LE
    
    Infix
mc2.propositional
- Mc2_propositional
  - F
mc2.smtlib
- Mc2_smtlib
  - Make
    
    ARG
  - Typecheck
    
    Make
    
    ARG
mc2.uf
- Mc2_uf
mc2.unin_sort
- Mc2_unin_sort

Legend:
Library
Module
Module type
Parameter
Class
Class type

Tseitin's CNF conversion.

Parameters

module F : Arg

Signature

type atom = F.t

The type of atomic formulas.

type combinator =

| And
| Or
| Not

type id

type t = private {

id : id;
view : view;

}

and view =

| True
| Lit of atom
| Comb of combinator * t list
(*
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 view : t -> view

val true_ : t

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

val false_ : t

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

val atom : atom -> t

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

val not_ : t -> t

Creates the negation of a boolean formula.

val and_ : t list -> t

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

val or_ : t list -> t

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

val xor : t -> t -> t

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

val imply : t -> t -> t

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

val imply_l : t list -> t -> t

val equiv : t -> t -> t

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

val cnf : ?simplify:bool -> fresh:(unit -> atom) -> t -> atom list list

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.

parameter fresh
used to generate fresh atoms to name formulas

parameter simplify
if true (default) simplifiy formula

val pp : t CCFormat.printer

pp fmt f prints the formula on the formatter fmt.