#include <Formula.hh>

Classes
class	CubeNode

Public Types
typedef Diades::Utils::Exception< FormulaFactory >	Exception

Public Member Functions
	FormulaFactory ()

	FormulaFactory (const VariableVector &varSet)

void	reset (const VariableVector &varSet)

	~FormulaFactory ()

const BDD &	noContext () const

const Formula &	context () const

const Formula &	newFormula (const Variable &variable, const Value &value) const

const Formula &	newFormula (int *cube)

const Formula &	newSwapFormula (const Formula &f, const VariableVector &var, const VariableVector &newVar)

void	extractAssignments (int *cube, const Variable &var, FormulaVector &assignments) const

void	extractValues (const int *cube, const Variable &var, ValueVector &values) const

const Value &	nullValue () const

const Formula &	newAndFormula (const Formula &f1, const Formula &f2)

const Formula &	newOrFormula (const Formula &f1, const Formula &f2)

const Formula &	newNotFormula (const Formula &f)

const Formula &	isTrue () const

const Formula &	isFalse () const

const Formula &	nullFormula () const

void	printInfoFactory () const

BDD	getBDD (bool positive, BDD var) const

void	increment (vector< bool > &encoding) const

void	bddFormulaToDot (DdNode *rootNode, const string &fileName) const

void	destroy ()

Variable &	getVariable (const string &name)

const VariableVector &	variables () const

bool	operator== (const FormulaFactory &factory) const

Cudd &	bddManager ()

const Cudd &	bddManager () const

bool	valid () const

void	addVariables (const vector< unsigned > &indexes, VariableVector &variables) const

const BDD &	getPositiveCube (const Variable &var) const

void	getModels (const Formula &formula, FormulaVector &models)

void	pickupModel (const Formula &formula, FormulaBox &model)

void	pickupModel (const Formula &formula, ValueVector &values)

Static Public Member Functions
static string	typeName ()

Static Public Attributes
static FormulaFactory	nullFactory

Private Member Functions
const Formula &	newFormula (const BDD &bdd)

const Formula &	createFormulaFromCube (const vector< int > &cube, const vector< BDD > &newVars)

BDD	encode (Variable &var, int &indexBDD)

void	searchAssignments (const int *cube, const Variable &var, list< CubeNode::Pointer > &leaves) const

Private Attributes
Cudd *	_mgr

vector< FormulaVector >	_assignments

vector< Formula::Pointer >	_allocatedFormulas

vector< int >	_indexesToVar

vector< vector< int > >	_varIndexes

vector< CubeNode *>	_rootCubeNode

vector< BDD >	_positiveCube

Formula::Pointer	_isNull

Formula::Pointer	_isTrue

Formula::Pointer	_isFalse

Formula::Pointer	_context

BDD	_nocontext

unordered_map< string, Variable::Reference >	_variableOfLabel

VariableVector	_varSet

Friends
class	Formula

Detailed Description

This class is the factory from which we can get any set of formulae based on a given set of variables.

Note: Here is the description of the encoding. For example, suppose two Variables v1 = {red blue yellow} and v2 = { yes, no } it is encoded with 3 bddVars (v1=red) is 00, (v1=blue) is 10, (v1=yellow) is 21 (i.e. 01 AND 11) (v2=yes) is 0 (v2=no) is 1.

Suppose now the following cube = 2 0 1, it represents (v1=red || v1=blue) && (v2 = n0). Suppose now the following cube = 2 1 2, it represents (v1=yellow). Suppose now the following cube = 2 2 2, it represents TRUE. Suppose now the following cube = 0 0 0, it represents (v1=red) && (v2=yes). With this encoding (v1=red) || (v1=blue) || (v1=yellow) is true and any conjunction like (v1=red) && (v1=blue) is False The BDD complement of an assignment Formula is also a Formula

Definition at line 509 of file Formula.hh.

Member Typedef Documentation

◆ Exception

typedef Diades::Utils::Exception<FormulaFactory> Diades::Sdmdl::FormulaFactory::Exception

Definition at line 673 of file Formula.hh.

Constructor & Destructor Documentation

◆ FormulaFactory() [1/2]

Diades::Sdmdl::FormulaFactory::FormulaFactory ( )

Default constructor

◆ FormulaFactory() [2/2]

Diades::Sdmdl::FormulaFactory::FormulaFactory ( const VariableVector & varSet )

Constructor

Parameters

varSet the set of Variable involved in the encoding formulas created by this Factory

◆ ~FormulaFactory()

Diades::Sdmdl::FormulaFactory::~FormulaFactory ( )

Destructor

Member Function Documentation

◆ addVariables()

void Diades::Sdmdl::FormulaFactory::addVariables	(	const vector< unsigned > &	indexes,
		VariableVector &	variables
	)		const

add the set of Variables supported by the bdd variables of indexes

Parameters

indexes	the set of indexes associated to bdd variables
variables	the resulting set of Variable supported by the bdd variables

◆ bddFormulaToDot()

void Diades::Sdmdl::FormulaFactory::bddFormulaToDot	(	DdNode *	rootNode,
		const string &	fileName
	)		const

Parameters

rootNode
fileName

◆ bddManager() [1/2]

Cudd& Diades::Sdmdl::FormulaFactory::bddManager ( )

inline

Returns: the underlying Cudd manager

Definition at line 981 of file Formula.hh.

References require.

◆ bddManager() [2/2]

const Cudd& Diades::Sdmdl::FormulaFactory::bddManager ( ) const

inline

Returns: the underlying Cudd manager

Definition at line 992 of file Formula.hh.

References require.

◆ context()

const Formula& Diades::Sdmdl::FormulaFactory::context ( ) const

inline

Returns: the context of any Formula. That is the global and acceptable world in the BDD manager. Any BDD that does not entail the context is not encoding a Formula context.bdd() * noContext() is bddZero context.bdd() + noContext() is bddOne

Deprecated:: it should always return isTrue() now

Definition at line 747 of file Formula.hh.

References Diades::Sdmdl::Formula::value(), and Diades::Sdmdl::Formula::variable().

◆ createFormulaFromCube()

const Formula& Diades::Sdmdl::FormulaFactory::createFormulaFromCube	(	const vector< int > &	cube,
		const vector< BDD > &	newVars
	)

private

Creation of a Formula from a cube

Parameters

cube	the cube that corresponds to the encoding of the Assignment
newVars	the support of the encoded Assignment

Returns: the Assignment Formula

◆ destroy()

void Diades::Sdmdl::FormulaFactory::destroy ( )

Destroy the Factory

Referenced by Diades::Sdmdl::Experimental::BddStateMachine::~BddStateMachine().

◆ encode()

BDD Diades::Sdmdl::FormulaFactory::encode	(	Variable &	var,
		int &	indexBDD
	)

private

encode the set of variable assignments with a set of bdd variables starting at index indexBDD

Parameters

var	the variable to encode
indexBDD	the starting index

Returns: the BDD encoding the set of assignments (it should/must be isTrue)

Postcondition: indexBDD = indexBDD + number of BddVar required to encode the assignments.

◆ extractAssignments()

void Diades::Sdmdl::FormulaFactory::extractAssignments	(	int *	cube,
		const Variable &	var,
		FormulaVector &	assignments
	)		const

Creation of the set of assignment Formula based on a cube for a given Variable

Parameters

cube	the given cube (an array of size bddManager().ReadSize() containing 0's 1's and 2's) cube[i] = 0 means the bddVar(i) is complemented cube[i] = 1 means the bddVar(i) is not complemented and cube[i] = 2 means the bddVar(i) is not involved in the bdd
var	the Variable
assignments	the returned assignment Formulas.

Note: For example suppose v1 = {red blue yellow} and v2 = { yes, no } it is encoded with 3 bddVars red = 00, blue = 10, yellow = 21 yes = 0 no = 1 Now suppose the cube 2 0 2, if 'var' is 'v1' then the cube encodes 2 0 for 'var' which represents two assignments v1 = red or v1 = blue. In this case the method returns two formulas: 'v1 = red', 'v1 = blue'. If var is 'v2' then the cube encodes 2 for 'var' which represents two assignments v2 = yes or v2 = no. In this case the disjunction of assignments is a tautology so nothing is returned.

◆ extractValues()

void Diades::Sdmdl::FormulaFactory::extractValues	(	const int *	cube,
		const Variable &	var,
		ValueVector &	values
	)		const

Get the values based on a cube for a given Variable

Parameters

cube	the given cube (an array of size bddManager().ReadSize() containing 0's 1's and 2's) cube[i] = 0 means the bddVar(i) is complemented cube[i] = 1 means the bddVar(i) is not complemented and cube[i] = 2 means the bddVar(i) is not involved in the bdd
var	the Variable
assignments	the returned assignment Formulas.

Note: For example suppose v1 = {red blue yellow} and v2 = { yes, no } it is encoded with 3 bddVars red = 00, blue = 10, yellow = 21 yes = 0 no = 1 Now suppose the cube 2 0 2, if 'var' is 'v1' then the cube encodes 2 0 for 'var' which represents two assignments v1 = red or v1 = blue. In this case the method returns two formulas: 'v1 = red', 'v1 = blue'. If var is 'v2' then the cube encodes 2 for 'var' which represents two assignments v2 = yes or v2 = no. In this case the disjunction of assignments is a tautology so nothing is returned.

◆ getBDD()

BDD Diades::Sdmdl::FormulaFactory::getBDD	(	bool	positive,
		BDD	var
	)		const

Parameters

positive
var

Returns: var if positive or not(var) if not positive

◆ getModels()

void Diades::Sdmdl::FormulaFactory::getModels	(	const Formula &	formula,
		FormulaVector &	models
	)

Model enumerations

Parameters

formula	a given formula
models	the set of full/complete assignments F such that F is a model of 'formula'

Note: Use this method with caution as the number of models that can entail 'formula' might be in the worst case (when 'formula.isTrue()') exponential to the number of variables in the BddManager.

◆ getPositiveCube()

const BDD& Diades::Sdmdl::FormulaFactory::getPositiveCube ( const Variable & var ) const

Parameters

var	a Variable

Returns: the positive cube of var that is b1 * b2 *... * bn where the bi's are the CUDD variables encoding var

◆ getVariable()

Variable& Diades::Sdmdl::FormulaFactory::getVariable ( const string & name )

Parameters

name	name of the Variable to look for

Returns: the corresponding Variable if it exists, a null Variable otherwise

Precondition: a non-empty set of Variable must be declared in the FormulaFactory

◆ increment()

void Diades::Sdmdl::FormulaFactory::increment ( vector< bool > & encoding ) const

Parameters

encoding the boolean counter to increment

◆ isFalse()

const Formula& Diades::Sdmdl::FormulaFactory::isFalse ( ) const

inline

Returns: the always false formula

Definition at line 884 of file Formula.hh.

Referenced by Diades::Sdmdl::Experimental::BddStateMachine::BddStateMachine(), Diades::Sdmdl::Experimental::BddStateMachine::resetInternalFormulaFactory(), and runGlobalDiagnosisProblem().

◆ isTrue()

const Formula& Diades::Sdmdl::FormulaFactory::isTrue ( ) const

inline

Returns: the always true formula

Definition at line 874 of file Formula.hh.

◆ newAndFormula()

const Formula& Diades::Sdmdl::FormulaFactory::newAndFormula	(	const Formula &	f1,
		const Formula &	f2
	)

Parameters

f1	a Formula
f2	a Formula

Returns: f1 and f2

◆ newFormula() [1/3]

const Formula& Diades::Sdmdl::FormulaFactory::newFormula	(	const Variable &	variable,
		const Value &	value
	)		const

Assignment formula

Parameters

variable	a declared Variable
value	a Value of the Variable

Returns: the formula (variable=value)

Referenced by Diades::Sdmdl::Experimental::encodeInitialStates(), and Diades::Sdmdl::Experimental::encodeTransitions().

◆ newFormula() [2/3]

const Formula& Diades::Sdmdl::FormulaFactory::newFormula ( int * cube )

Creation of a Formula based on a cube

Parameters

cube	the given cube (an array of size bddManager().ReadSize() containing 0's 1's and 2's) cube[i] = 0 means the bddVar(i) is complemented cube[i] = 1 means the bddVar(i) is not complemented and cube[i] = 2 means the bddVar(i) is not involved in the bdd

Returns: the Formula

◆ newFormula() [3/3]

const Formula& Diades::Sdmdl::FormulaFactory::newFormula ( const BDD & bdd )

private

Creation of a Formula from a BDD

Parameters

bdd	a predefined BDD

◆ newNotFormula()

const Formula& Diades::Sdmdl::FormulaFactory::newNotFormula ( const Formula & f )

Parameters

f a Formula

Returns: not(f)

◆ newOrFormula()

const Formula& Diades::Sdmdl::FormulaFactory::newOrFormula	(	const Formula &	f1,
		const Formula &	f2
	)

Parameters

f1	a Formula
f2	a Formula

Returns: f1 or f2

◆ newSwapFormula()

const Formula& Diades::Sdmdl::FormulaFactory::newSwapFormula	(	const Formula &	f,
		const VariableVector &	var,
		const VariableVector &	newVar
	)

Creation of a Formula as a swap of variable in another Formula

Returns: the Formula

◆ noContext()

const BDD& Diades::Sdmdl::FormulaFactory::noContext ( ) const

inline

Returns: the BDD that expresses the undefined context in the BDD manager See context() for mor details

Deprecated:: it should always return isFalse() now

Definition at line 733 of file Formula.hh.

◆ nullFormula()

const Formula& Diades::Sdmdl::FormulaFactory::nullFormula ( ) const

inline

Returns: the null Formula

Definition at line 893 of file Formula.hh.

Referenced by Diades::Sdmdl::FormulaFactory::CubeNode::getAssignment().

◆ nullValue()

const Value& Diades::Sdmdl::FormulaFactory::nullValue ( ) const

inline

Returns: a null Value

Definition at line 834 of file Formula.hh.

References Diades::Sdmdl::ValueFactory::nullValue(), and Diades::Sdmdl::Value::owner().

Referenced by Diades::Sdmdl::FormulaFactory::CubeNode::getValue().

◆ operator==()

bool Diades::Sdmdl::FormulaFactory::operator== ( const FormulaFactory & factory ) const

inline

Parameters

factory

Returns

Definition at line 971 of file Formula.hh.

◆ pickupModel() [1/2]

void Diades::Sdmdl::FormulaFactory::pickupModel	(	const Formula &	formula,
		FormulaBox &	model
	)

Pickup a model

Parameters

formula	a given formula
model	a complete set of assignments F such that F is a model of 'formula', empty if such a model does not exist

◆ pickupModel() [2/2]

void Diades::Sdmdl::FormulaFactory::pickupModel	(	const Formula &	formula,
		ValueVector &	values
	)

Pickup a model

Parameters

formula	a given formula
values	the set of values assigned to variables() to get the model

◆ printInfoFactory()

void Diades::Sdmdl::FormulaFactory::printInfoFactory ( ) const

◆ reset()

void Diades::Sdmdl::FormulaFactory::reset ( const VariableVector & varSet )

Parameters

varSet the new Variable set involved in the encoding formulas created by this Factory

Referenced by Diades::Sdmdl::Experimental::BddStateMachine::resetInternalFormulaFactory().

◆ searchAssignments()

void Diades::Sdmdl::FormulaFactory::searchAssignments	(	const int *	cube,
		const Variable &	var,
		list< CubeNode::Pointer > &	leaves
	)		const

private

Search assignments from a cube

Parameters

cube	a cube
var	the variable involved in the assignments to look for
leaves	the CubeNode that contains the assignments to look for

◆ typeName()

static string Diades::Sdmdl::FormulaFactory::typeName ( )

inlinestatic

Definition at line 670 of file Formula.hh.

◆ valid()

bool Diades::Sdmdl::FormulaFactory::valid ( ) const

inline

Returns: true if the fcatory is valid

Definition at line 1003 of file Formula.hh.

References Diades::Sdmdl::Formula::bdd(), Diades::Sdmdl::Experimental::encode(), and Diades::Sdmdl::Formula::getModels().

◆ variables()

const VariableVector& Diades::Sdmdl::FormulaFactory::variables ( ) const

inline

Returns: the set of declared variables

Definition at line 960 of file Formula.hh.

Friends And Related Function Documentation

◆ Formula

friend class Formula

friend

Definition at line 1107 of file Formula.hh.

Member Data Documentation

◆ _allocatedFormulas

vector<Formula::Pointer> Diades::Sdmdl::FormulaFactory::_allocatedFormulas

private

Definition at line 679 of file Formula.hh.

◆ _assignments

vector< FormulaVector > Diades::Sdmdl::FormulaFactory::_assignments

private

Definition at line 678 of file Formula.hh.

◆ _context

Formula::Pointer Diades::Sdmdl::FormulaFactory::_context

private

Definition at line 687 of file Formula.hh.

◆ _indexesToVar

vector<int> Diades::Sdmdl::FormulaFactory::_indexesToVar

private

Definition at line 680 of file Formula.hh.

◆ _isFalse

Formula::Pointer Diades::Sdmdl::FormulaFactory::_isFalse

private

Definition at line 686 of file Formula.hh.

◆ _isNull

Formula::Pointer Diades::Sdmdl::FormulaFactory::_isNull

private

Definition at line 684 of file Formula.hh.

◆ _isTrue

Formula::Pointer Diades::Sdmdl::FormulaFactory::_isTrue

private

Definition at line 685 of file Formula.hh.

◆ _mgr

Cudd* Diades::Sdmdl::FormulaFactory::_mgr

private

Definition at line 677 of file Formula.hh.

◆ _nocontext

BDD Diades::Sdmdl::FormulaFactory::_nocontext

private

Definition at line 688 of file Formula.hh.

◆ _positiveCube

vector< BDD > Diades::Sdmdl::FormulaFactory::_positiveCube

private

Definition at line 683 of file Formula.hh.

◆ _rootCubeNode

vector< CubeNode * > Diades::Sdmdl::FormulaFactory::_rootCubeNode

private

Definition at line 682 of file Formula.hh.

◆ _variableOfLabel

unordered_map<string, Variable::Reference> Diades::Sdmdl::FormulaFactory::_variableOfLabel

private

Definition at line 689 of file Formula.hh.

◆ _varIndexes

vector< vector<int> > Diades::Sdmdl::FormulaFactory::_varIndexes

private

Definition at line 681 of file Formula.hh.

◆ _varSet

VariableVector Diades::Sdmdl::FormulaFactory::_varSet

private

_varSet the current set of declared Variables

Definition at line 695 of file Formula.hh.

◆ nullFactory

FormulaFactory Diades::Sdmdl::FormulaFactory::nullFactory

static

Definition at line 674 of file Formula.hh.

The documentation for this class was generated from the following file:

/home/yannick/laas/redmine/tools/diades/include/diades/sdmdl/Formula.hh

Classes

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Private Member Functions

Private Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ Exception

Constructor & Destructor Documentation

◆ FormulaFactory() [1/2]

◆ FormulaFactory() [2/2]

◆ ~FormulaFactory()

Member Function Documentation

◆ addVariables()

◆ bddFormulaToDot()

◆ bddManager() [1/2]

◆ bddManager() [2/2]

◆ context()

◆ createFormulaFromCube()

◆ destroy()

◆ encode()

◆ extractAssignments()

◆ extractValues()

◆ getBDD()

◆ getModels()

◆ getPositiveCube()

◆ getVariable()

◆ increment()

◆ isFalse()

◆ isTrue()

◆ newAndFormula()

◆ newFormula() [1/3]

◆ newFormula() [2/3]

◆ newFormula() [3/3]

◆ newNotFormula()

◆ newOrFormula()

◆ newSwapFormula()

◆ noContext()

◆ nullFormula()

◆ nullValue()

◆ operator==()

◆ pickupModel() [1/2]

◆ pickupModel() [2/2]

◆ printInfoFactory()

◆ reset()

◆ searchAssignments()

◆ typeName()

◆ valid()

◆ variables()

Friends And Related Function Documentation

◆ Formula

Member Data Documentation

◆ _allocatedFormulas

◆ _assignments

◆ _context

◆ _indexesToVar

◆ _isFalse

◆ _isNull

◆ _isTrue

◆ _mgr

◆ _nocontext

◆ _positiveCube

◆ _rootCubeNode

◆ _variableOfLabel

◆ _varIndexes

◆ _varSet

◆ nullFactory