carl::formula::symmetry Namespace Reference

Data Structures
class	ColorGenerator
	Provides unique ids (colors) for all kinds of different objects in the formula: variable types, relations, formula types, numbers, special colors and indexes. More...
struct	Permutation
class	GraphBuilder

Enumerations
enum class	SpecialColors { If , Then , Else , VarExp }
	Special colors for structure nodes. More...

Functions
template<typename Poly >
Formula< Poly >	createComparison (Variable x, Variable y, Relation rel)
template<typename Poly >
Formula< Poly >	lexLeaderConstraint (const Symmetry &vars)
	Creates symmetry breaking constraints from the passed symmetries in the spirit of [1]. More...
void	addGenerator (void *p, const unsigned int n, const unsigned int *aut)

Enumeration Type Documentation

SpecialColors

enum carl::formula::symmetry::SpecialColors

strong

Special colors for structure nodes.

• If: condition from ite
• Then: first case from ite
• Else: second case from ite
• VarExp: pair of variable and exponent in terms

Enumerator
If
Then
Else
VarExp

Definition at line 21 of file SymmetryFinder.h.

Function Documentation

addGenerator()

void carl::formula::symmetry::addGenerator	(	void *	p,
		const unsigned int	n,
		const unsigned int *	aut
	)

Definition at line 73 of file SymmetryFinder.h.

Here is the caller graph for this function:

createComparison()

template<typename Poly >

Formula<Poly> carl::formula::symmetry::createComparison	(	Variable	x,
		Variable	y,
		Relation	rel
	)

Definition at line 12 of file SymmetryBreaker.h.

Here is the call graph for this function:

lexLeaderConstraint()

template<typename Poly >

Formula<Poly> carl::formula::symmetry::lexLeaderConstraint

(

const Symmetry &

vars

)

Creates symmetry breaking constraints from the passed symmetries in the spirit of [1].

Definition at line 39 of file SymmetryBreaker.h.