Comparator compares two formulas f1 and f2 with their integer value.

DefaultFormulaGraphicalGenerator returns a graphical formula generator with sensible defaults.

DefaultSymbols returns the standard symbols for printing formulas.

DualSort returns the dual sort for AND and OR.

EncodeFormula takes a formula sort and a unique ID an returns its encoding.

EncodeLiteral takes a unique ID an returns its encoding as a literal.

EncodeVariable takes a unique ID an returns its encoding as a variable.

FormulaDepth returns the depth of the given formula.

GenerateGraphicalFormulaAST generates a graphical representation of the formula with the configuration of the generator as an abstract syntax tree (AST).

GenerateGraphicalFormulaDAG generates a graphical representation of the formula with the configuration of the generator as a graph (DAG).

LiteralProfile returns the number of occurrences of each literal in the given formula.

Literals returns all literals of the given formula as a literal set.

LiteralsAsFormulas returns a list of literals as a list of formulas.

LiteralsAsVariables returns a list of literals as a list of variables or returns an error if there is a negative literal in the list.

LookupFunctionCache searches a cache entry for a given function sort and formula.

LookupPredicateCache searches a cache entry for a given predicate sort and formula.

LookupTransformationCache searches a cache entry for a given transformation sort and formula.

NewExtendedProposition returns a new extended proposition with the formula and the given backpack.

NewFactory returns a new caching formula factory.

NewFormulaSet generates a new formula set with the given formulas as content.

NewLitSet generates a new literal set with the given literal as content.

NewMutableFormulaSet generates a new mutable formula set with the given formulas as content.

NewMutableLitSet generates a new mutable literal set with the given literal as content.

NewMutableVarSet generates a new mutable variable set with the given variables as content.

NewMutableVarSetCopy returns a new mutable variable set with the content of all the given variable sets as content.

NewStandardProposition returns a new standard proposition with the formula and an optional textual description.

NewVarSet generates a new variable set with the given variables as content.

NewVarSetCopy returns a new variable set with the content of all the given variable sets as content.

NumberOfAtoms returns the number of atomic formulas of the given formula.

NumberOfNodes returns the number of nodes (in the DAG) of the given formula.

PropComparator compares two propositions p1 and p2.

SetFunctionCache sets a cache entry for a given function sort, formula and value to cache.

SetPredicateCache sets a cache entry for a given predicate sort, formula and value to cache.

SetTransformationCache sets a cache entry for a given transformation sort, formula and value to cache.

SubNodes returns all sub-nodes of the given formula.

TristateFromBool returns the tristate for the given Boolean value.

VariableProfile returns the number of occurrences of each variable in the given formula.

Variables returns all variables of the given formula as a variable set.

VariablesAsFormulas returns a list of variables as a list of formulas.

VariablesAsLiterals returns a list of variables as a list of literals.

equal.

greater or equal.

greater than.

less or equal.

less than.

conjunction.

cardinality constraint.

equivalence.

constant false.

implication.

literal (variable + phase).

negation.

disjunction.

pseudo-Boolean constraint.

constant true.

A CachingFactory is the default (and currently only) implementation of the formula factory in LogicNG.

An ExtendedProposition is a proposition implementation with a formula and a user provided generic backpack.

PrintSymbols gathers all symbols for Boolean and pseudo-Boolean formulas for printing formulas.

A StandardProposition is a simple proposition implementation with a formula and a textual description.

A Factory is the central concept of LogicNG and is always required when working with the library.

A Proposition is a formula with additional information like a textual description or a user-provided object.

An AbortableTransformation is a function which maps a formula to another formula.

AuxVarSort encodes the auxiliary variable sort.

CSort encodes the sort of an integer comparator.

Formula represents a Boolean (or pseudo-Boolean) formula in LogicNG.

FSort encodes the different formula sorts.

A Function is a function which maps a formula to an arbitrary value.

FunctionCacheSort encodes a formula function sort for which the result can be cached.

Literal represents a Boolean literal in LogicNG.

A Predicate is a function which maps a formula to a boolean value.

PredicateCacheSort encodes a formula predicate sort for which the result can be cached.

A Transformation is a function which maps a formula to another formula.

TransformationCacheSort encodes a formula transformation sort for which the result can be cached.

Tristate represents a Boolean value with the possibility of a third UNDEF value.

Variable represents a Boolean variable in LogicNG.