Module Logtk.Cnf

Reduction to CNF and Simplifications

type term = TypedSTerm.t
type form = TypedSTerm.t
type type_ = TypedSTerm.t
type lit = term SLiteral.t
exception Error of string
exception NotCNF of form
val miniscope : ?⁠distribute_exists:bool -> form -> form

Apply miniscoping transformation to the term.

parameter distribute_exists

see whether ?X:(p(X)|q(X)) should be transformed into (?X: p(X) | ?X: q(X)). Default: false

type options =
| DistributeExists

if enabled, will distribute existential quantifiers over disjunctions. This can make skolem symbols smaller (smaller arity) but introduce more of them.

| DisableRenaming

disables formula renaming. Can re-introduce the worst-case exponential behavior of CNF.

| InitialProcessing of form -> form

any processing, at the beginning, before CNF starts

| PostNNF of form -> form

any processing that keeps negation at leaves, just after reduction to NNF. Its output must not break the NNF form (negation at root only).

| PostSkolem of form -> form

transformation applied just after skolemization. It must not break skolemization nor NNF (no quantifier, no non-leaf negation).

Options are used to tune the behavior of the CNF conversion.

type clause = lit list

Basic clause representation, as list of literals

val clause_to_fo : ?⁠ctx:Term.Conv.ctx -> clause -> Term.t SLiteral.t list
type f_statement = (termtermtype_) Statement.t

A statement before CNF

type c_statement = (clausetermtype_) Statement.t

A statement after CNF

val pp_f_statement : f_statement CCFormat.printer
val pp_c_statement : c_statement CCFormat.printer
val pp_fo_c_statement : (Term.t SLiteral.t list, Term.tType.t) Statement.t CCFormat.printer
val is_clause : form -> bool
val is_cnf : form -> bool

Main Interface

val cnf_of : ?⁠opts:options list -> ?⁠ctx:Skolem.ctx -> f_statement -> c_statement CCVector.ro_vector

Transform the statement into proper CNF; returns a list of statements, including type declarations for new Skolem symbols or formulas proxies. Options are used to tune the behavior.

val cnf_of_seq : ?⁠opts:options list -> ?⁠ctx:Skolem.ctx -> f_statement Sequence.t -> c_statement CCVector.ro_vector
val type_declarations : c_statement Sequence.t -> type_ Logtk.ID.Map.t

Compute the types declared in the statement sequence

Conversions

val convert : c_statement Sequence.t -> Statement.clause_t CCVector.ro_vector

Converts statements based on TypedSTerm into statements based on Term and Type