package mc2

You can search for identifiers within the package.

in-package search v0.2.0

A mcsat-based SMT solver in pure OCaml

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (1)

Authors

Maintainers

S

simon.cruanes.2007@m4x.org

Sources

v0.1.tar.gz

md5=92de696251ec76fbf3eba6ee917fd80f

sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0

doc/mc2.propositional/Mc2_propositional/F/index.html

Module `Mc2_propositional.F`Source

Formulas

Sourcetype combinator =

| And
| Or
| Not

Sourcetype id

Sourcetype t = private {

id : id;
view : view;

}

Sourceand view =

| True
| Lit of Mc2_core.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.
*)

Sourceval view : t -> view

Sourceval true_ : t

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

Sourceval false_ : t

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

Sourceval atom : Mc2_core.atom -> t

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

Sourceval not_ : t -> t

Creates the negation of a boolean formula.

Sourceval and_ : t list -> t

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

Sourceval or_ : t list -> t

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

Sourceval xor : t -> t -> t

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

Sourceval imply : t -> t -> t

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

Sourceval imply_l : t list -> t -> t

Sourceval equiv : t -> t -> t

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

Source

val cnf : 
  ?simplify:bool ->
  fresh:(unit -> Mc2_core.atom) ->
  t ->
  Mc2_core.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

Sourceval pp : t CCFormat.printer

pp fmt f prints the formula on the formatter fmt.