ContainsPBC reports whether the given formula contains a pseudo-Boolean constraint of any sort.

DefaultConfig returns the default configuration for an encoder configuration.

EncodeCC encodes a cardinality constraint to a CNF formula as a list of clauses.

EncodeCCInResult encodes a cardinality constraint into an encoding result.

EncodeIncremental encodes an incremental cardinalityConstraint into an encoding result and return the incremental data with this result.

EncodePBC encodes a pseudo-Boolean constraint to a CNF formula as a list of clauses.

EncodePBCInResult encodes a pseudo-Boolean constraint into an encoding result.

NegatePBC returns the negation of the given pseudo-Boolean constraint.

Normalize returns a normalized <= constraint of the given pseudo-Boolean or cardinality constraint.

ResultForFormula creates a new encoding result backed by the given formula factory.

CcAlkEncoder represents the different algorithms for encoding an at-least-k constraint (ALK) to a CNF.

CcAlkEncoder represents the different algorithms for encoding an at-least-k constraint (ALK) to a CNF.

CcAlkEncoder represents the different algorithms for encoding an at-least-k constraint (ALK) to a CNF.

CcAlkEncoder represents the different algorithms for encoding an at-least-k constraint (ALK) to a CNF.

CcAmkEncoder represents the different algorithms for encoding an at-most-k constraint (AMK) to a CNF.

CcAmkEncoder represents the different algorithms for encoding an at-most-k constraint (AMK) to a CNF.

CcAmkEncoder represents the different algorithms for encoding an at-most-k constraint (AMK) to a CNF.

CcAmkEncoder represents the different algorithms for encoding an at-most-k constraint (AMK) to a CNF.

CcAmoEncoder represents the different algorithms for encoding an at-most-one constraint (AMO) to a CNF.

CcAmoEncoder represents the different algorithms for encoding an at-most-one constraint (AMO) to a CNF.

CcAmoEncoder represents the different algorithms for encoding an at-most-one constraint (AMO) to a CNF.

CcAmoEncoder represents the different algorithms for encoding an at-most-one constraint (AMO) to a CNF.

CcAmoEncoder represents the different algorithms for encoding an at-most-one constraint (AMO) to a CNF.

CcAmoEncoder represents the different algorithms for encoding an at-most-one constraint (AMO) to a CNF.

CcAmoEncoder represents the different algorithms for encoding an at-most-one constraint (AMO) to a CNF.

CcAmoEncoder represents the different algorithms for encoding an at-most-one constraint (AMO) to a CNF.

BimanderGroupSize is a parameter which can be used for defining the group size in the Bimander encoding for AMO constraints.

BimanderGroupSize is a parameter which can be used for defining the group size in the Bimander encoding for AMO constraints.

BimanderGroupSize is a parameter which can be used for defining the group size in the Bimander encoding for AMO constraints.

CcExkEncoder represents the different algorithms for encoding an exactly-k constraint (EXK) to a CNF.

CcExkEncoder represents the different algorithms for encoding an exactly-k constraint (EXK) to a CNF.

CcExkEncoder represents the different algorithms for encoding an exactly-k constraint (EXK) to a CNF.

PbcEncoder represents the different algorithms for encoding a pseudo-Boolean constraint to a CNF.

PbcEncoder represents the different algorithms for encoding a pseudo-Boolean constraint to a CNF.

PbcEncoder represents the different algorithms for encoding a pseudo-Boolean constraint to a CNF.

PbcEncoder represents the different algorithms for encoding a pseudo-Boolean constraint to a CNF.

CCIncrementalData gathers data for an incremental at-most-k cardinality constraint.

Config describes the configuration for a cardinality or pseudo-Boolean encoding.

FormulaEncoding implements a Result backed by a formula factory.

A Result is used to abstract CNF encodings for cardinality and pseudo-Boolean constraints.