Documentation
¶
Overview ¶
Package transformation gathers various transformations on formulas. A formula transformations always takes a formula factory and formula as input and yields some transformed formula.
Currently, the following transformations are implemented
- formula anonymization
- substitution from variable to formula
- substitution from literal to literal
- pure expansion of AMO and EXO constraints
- existential and universal quantifier elimination
- CNF and DNF subsumption
Index ¶
- func Anonymize(fac f.Factory, formula f.Formula) f.Formula
- func CNFSubsumption(fac f.Factory, formula f.Formula) (f.Formula, error)
- func DNFSubsumption(fac f.Factory, formula f.Formula) (f.Formula, error)
- func ExistentialQE(fac f.Factory, formula f.Formula, variable ...f.Variable) f.Formula
- func ExpandAMOAndEXO(fac f.Factory, formula f.Formula) (f.Formula, error)
- func Substitute(fac f.Factory, formula f.Formula, subst *Substitution) (f.Formula, error)
- func SubstituteLiterals(fac f.Factory, formula f.Formula, substitution *map[f.Literal]f.Literal) f.Formula
- func UniversalQE(fac f.Factory, formula f.Formula, variable ...f.Variable) f.Formula
- type Anonymizer
- type Substitution
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func Anonymize ¶
Anonymize anonymizes the given formula by replacing all variables in it by newly generated ones, starting with v0, v1, ...
func CNFSubsumption ¶
CNFSubsumption performs subsumption on a given CNF formula and returns a new CNF. I.e. it performs as many subsumptions as possible. A subsumption in a CNF means, that e.g. a clause A | B | C is subsumed by another clause A | B and can therefore be deleted for an equivalent CNF. Returns with an error if the input formula was not in CNF.
func DNFSubsumption ¶
DNFSubsumption performs subsumption on a given DNF formula and returns a new DNF. I.e. it performs as many subsumptions as possible. A subsumption in a DNF means, that e.g. a minterm A & B is subsumed by another clause A & B & C and can therefore be deleted for an equivalent DNF. Returns with an error if the input formula was not in DNF.
func ExistentialQE ¶
ExistentialQE eliminates a number of existentially quantified variables by replacing them with the Shannon expansion. If x is eliminated from the formula, the resulting formula is formula[true/x] | formula[false/x].
func ExpandAMOAndEXO ¶
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. Since there are no such encodings for pseudo-Boolean constraints or arbitrary cardinality constraints, in this case the function returns an error.
func Substitute ¶
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. Variables not in the substitution are left as-is. The function returns an error when you try to substitute a formula for a literal which is used in a cardinality or Pseudo-Boolean constraint since this is not possible.
func SubstituteLiterals ¶
func SubstituteLiterals(fac f.Factory, formula f.Formula, substitution *map[f.Literal]f.Literal) f.Formula
SubstituteLiterals performs a special substitution from literal to literal on the given formula. In contrast to the standard Substitute function which can only map variables, this function can also map literals.
Always the best fit is chosen. So if there are two mappings for e.g. a -> b and ~a -> c. Then ~a will be mapped to c and not to ~b. On the other hand if there is only the mapping a -> b, the literal ~a will be mapped to ~b.
func UniversalQE ¶
UniversalQE eliminates a number of universally quantified variables by replacing them with the Shannon expansion. If x is eliminated from the formula, the resulting formula is formula[true/x] & formula[false/x].
Types ¶
type Anonymizer ¶
type Anonymizer struct {
Substitution *Substitution
// contains filtered or unexported fields
}
An Anonymizer can be used to replace variables in a formula with newly generated ones with a given prefix. Thus, it can be used to anonymize a formula. An Anonymizer can be used for multiple transformations and holds its internal substitution map for the variables.
func NewAnonymizer ¶
func NewAnonymizer(fac f.Factory, prefix ...string) *Anonymizer
NewAnonymizer generates a new anonymizer with an optional prefix for the generated variables. The default Prefix is `v`.
type Substitution ¶
type Substitution struct {
// contains filtered or unexported fields
}
A Substitution represents a mapping from variables to formulas. When executing the Substitute function with such a substitution, all variables in a formula are replaced by their mapped formula.
func NewSubstitution ¶
func NewSubstitution() *Substitution
NewSubstitution generates a new empty substitution.
func (*Substitution) AddMapping ¶
func (s *Substitution) AddMapping(mapping map[f.Variable]f.Formula)
AddMapping adds the given mapping from variables to formulas to the substitution.
Source Files