# Functions
Anonymize anonymizes the given formula by replacing all variables in it by newly generated ones, starting with v0, v1, ...
ExistentialQE eliminates a number of existentially quantified variables by replacing them with the Shannon expansion.
ExpandAMOAndEXO expands all at-most-one and exactly-one cardinality constraints in the given formula by their pure encoding, meaning without the introduction of auxiliary variables.
NewAnonymizer generates a new anonymizer with an optional prefix for the generated variables.
NewSubstitution generates a new empty substitution.
Substitute performs the given substitution on the given formula and returns a new formula where all variables of the substitution are replaced by their mapped formulas.
SubstituteLiterals performs a special substitution from literal to literal on the given formula.
UniversalQE eliminates a number of universally quantified variables by replacing them with the Shannon expansion.
# Structs
An Anonymizer can be used to replace variables in a formula with newly generated ones with a given prefix.
A Substitution represents a mapping from variables to formulas.