# Functions
AIG returns the given formula as AIG (and-inverter-graph), therefore only containing conjunctions and negations.
CNF returns a conjunctive normal form of the given formula with the optional CNF configuration.
DefaultCNFConfig returns the default configuration for a CNF configuration.
FactorizedCNF returns the given formula in conjunctive normal form.
FactorizedCNFWithHandler returns the given formula in conjunctive normal form.
FactorizedDNF returns the given formula in disjunctive normal form.
FactorizedDNFWithHandler returns the given formula in disjunctive normal form.
HandlerWithTimeout generates a new timeout handler with the given timeout.
IsAIG reports whether the given formula is in AIG (and-inverter-graph) normal-form, therefore only containing conjunctions and negations.
IsCNF reports whether the given formula is in conjunctive normal form.
IsDNF reports whether the given formula is in disjunctive normal form.
IsMaxterm reports whether the given formula is a maxterm, i.e.
IsMinterm reports whether the given formula is a minterm, i.e.
IsNNF reports whether the given formula is in negation normal form.
NewCNFAuxState generates a new empty state for Tseitin or Plaisted & Greenbaum CNF transformations.
NewCNFHandler returns a new handler for the advanced CNF transformation with the given distribution and clause boundary.
NNF returns the negation normal form of the given formula.
PGCNF transforms a formula to CNF with the algorithm by Plaisted & Greenbaum.
PGCNFDefault transforms a formula to CNF with the algorithm by Plaisted & Greenbaum.
PGCNFWithBoundary transforms a formula to CNF with the algorithm by Plaisted & Greenbaum.
TseitinCNF transforms a formula to CNF with the algorithm by Tseitin.
TseitinCNFDefault transforms a formula to CNF with the algorithm by Tseitin.
TseitinCNFWithBoundary transforms a formula to CNF with the algorithm by Tseitin.
# Constants
No description provided by the author
No description provided by the author
No description provided by the author
No description provided by the author
# Structs
CNFAuxState is holds the variable and formula mapping for a Tseitin or Plaisted & Greenbaum CNF transformation.
CNFConfig represents the configuration for the CNF conversion.
CNFHandler is a special handler for the advanced CNF algorithm.
A TimeoutHandler can be used to abort a CNF factorization depending on a timeout set beforehand.
# Interfaces
FactorizationHandler is a special handler able to abort CNF or DNF factorizations.
# Type aliases
CNFAlgorithm encodes the different algorithms for converting a formula to CNF.