Module formulas

Expand description

Types and datastructures to represent and manage formulas effectively.

Structs§

CacheConfig: Specifies which type of operations are allowed to cache their results.
CardinalityConstraint: Cardinality constraints CardinalityConstraint are a special type of formulas which enforce that a certain number of variables is assigned to true.
EncodedFormula: EncodedFormula represents a logical formula.
FormulaFactory: The formula factory is the central concept of LogicNG and is always required when working with LogicNG. A formula factory is an object consisting of two major components:
FormulaFactoryConfig: FormulaFactoryConfig is a configuration for a FormulaFactory.
NaryIterator: An iterator returning operands of a nary-operator.
PbConstraint: A pseudo-boolean constraint PbConstraint is a generalization of a CardinalityConstraint.
StringLiteral: Representation of a literals for external use.

AuxVarType: Implementation note: We’re not using a dedicated AuxVarType for CC/PBC vars created on solver, because this yields a problem: We do not want such variables to occur in formulas outside of the solver (otherwise we could just use CC), but it’s hard to prevent the solver from returning them (especially in the FormulaOnSolverFunction). We would need to transform such variables into CC variables then, but that could easily be forgotten or we would require MiniSat2Solver#variable_for_idx to also take a FF which would be a pain.
CType: Comparison types for pseudo-Boolean constraints.
Formula: A unpacked representation of an EncodedFormula. Allows access to the operands of the formula.
FormulaType: Specifies all types a EncodedFormula can have.
LitType: Specifies all types of literals.
Literal: Boolean literal.
VarType: Specifies all types of literals.
Variable: Boolean variables.

ToFormula: Trait for converting a type into a formula of the given FormulaFactory.
ToStringLiteral: Converts a type into a StringLiteral.