#include <Formula.hh>

Public Types
enum	BinaryOperator { OrOp = 0, AndOp = 1 }

enum	UnaryOperator { NotOp = 0 }

typedef Utils::Exception< Formula >	Exception

typedef std::reference_wrapper< Formula const >	ConstReference

typedef std::vector< ConstReference >	FormulaVector

typedef Formula *	Pointer

Public Member Functions
void	getModels (FormulaVector &models) const

const Formula &	existAbstract (const VariableVector &variables, bool complementSet=false) const

bool	isAssignment () const

const VariableVector &	support () const

const Value &	value () const

const Variable &	variable () const

bool	isFalse () const

bool	isTrue () const

void	primes (FormulaVector &result) const

bool	operator== (const Formula &f) const

bool	operator!= (const Formula &f) const

virtual	~Formula ()

const Cudd &	bddManager () const

const BDD &	bdd () const

const Formula &	operator\|\| (const Formula &f) const

const Formula &	operator && (const Formula &f) const

const Formula &	operator! () const

const Formula &	apply (BinaryOperator op, const Formula &f) const

const Formula &	apply (UnaryOperator op) const

bool	entails (const Formula &f) const

bool	satisfies (const Formula &f) const

bool	isCube () const

bool	equivalent (const Formula &f) const

string	textify () const

string	latexify () const

bool	isNull () const

FormulaFactory &	owner () const

Static Public Member Functions
static string	typeName ()

Private Member Functions
	Formula (FormulaFactory &owner)

	Formula (const BDD &bdd, int index, FormulaFactory &owner)

Private Attributes
BDD	_bdd

int	_dataIndex

FormulaFactory *	_owner

VariableVector	_support

bool	_supportNotComputed

ValueVector	_value

Friends
class	FormulaFactory

ostream &	operator<< (ostream &os, const Formula &f)

Detailed Description

A Formula object. It represents boolean formula (use of Binary Decision Diagram)

Todo:: make a Formula a unique object (reference equality)

Definition at line 42 of file Formula.hh.

Member Typedef Documentation

◆ ConstReference

typedef std::reference_wrapper<Formula const> Diades::Sdmdl::Formula::ConstReference

Definition at line 73 of file Formula.hh.

◆ Exception

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

Definition at line 66 of file Formula.hh.

◆ FormulaVector

typedef std::vector<ConstReference> Diades::Sdmdl::Formula::FormulaVector

Definition at line 74 of file Formula.hh.

◆ Pointer

typedef Formula* Diades::Sdmdl::Formula::Pointer

Definition at line 75 of file Formula.hh.

Member Enumeration Documentation

◆ BinaryOperator

enum Diades::Sdmdl::Formula::BinaryOperator

Enumerator
OrOp
AndOp

Definition at line 49 of file Formula.hh.

◆ UnaryOperator

enum Diades::Sdmdl::Formula::UnaryOperator

Enumerator
NotOp

Definition at line 57 of file Formula.hh.

Constructor & Destructor Documentation

◆ Formula() [1/2]

Diades::Sdmdl::Formula::Formula ( FormulaFactory & owner )

inlineprivate

Null Formula constructor

Parameters

owner the FormulaFactory that creates this Formula

Definition at line 119 of file Formula.hh.

◆ Formula() [2/2]

Diades::Sdmdl::Formula::Formula	(	const BDD &	bdd,
		int	index,
		FormulaFactory &	owner
	)

inlineprivate

Formula constructor

Parameters

bdd	the underlying bdd
index	the data index provided by the FormulaFactory
owner	the FormulaFactory that creates this Formula

Definition at line 133 of file Formula.hh.

References existAbstract(), and getModels().

◆ ~Formula()

virtual Diades::Sdmdl::Formula::~Formula ( )

inlinevirtual

Destructor

Definition at line 273 of file Formula.hh.

References bddManager().

Member Function Documentation

◆ apply() [1/2]

const Formula& Diades::Sdmdl::Formula::apply	(	BinaryOperator	op,
		const Formula &	f
	)		const

Apply a binary operator

Parameters

op	the binaryoperator
f	the Formula to combine

Returns: *this op f

Referenced by bdd(), Diades::Sdmdl::FormulaBinaryOperator< OP >::operator()(), and Diades::Sdmdl::FormulaUnaryOperator< OP >::operator()().

◆ apply() [2/2]

const Formula& Diades::Sdmdl::Formula::apply ( UnaryOperator op ) const

Apply a unary operator

Parameters

op	the unaryoperator

Returns: op *this

◆ bdd()

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

inline

Returns: the underlying bdd

Definition at line 288 of file Formula.hh.

References _bdd, apply(), entails(), equivalent(), isCube(), isNull(), latexify(), operator &&(), operator!(), operator<<, operator||(), owner(), satisfies(), and textify().

Referenced by Diades::Sdmdl::CubeGenerator::CubeGenerator(), and Diades::Sdmdl::FormulaFactory::valid().

◆ bddManager()

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

Returns: the cudd manager

Referenced by Diades::Sdmdl::CubeGenerator::CubeGenerator(), Diades::Sdmdl::CubeGenerator::cubeSize(), and ~Formula().

◆ entails()

bool Diades::Sdmdl::Formula::entails ( const Formula & f ) const

Entailment

Parameters

f a Formula

Returns: true iff (*this) |= f

Referenced by bdd().

◆ equivalent()

bool Diades::Sdmdl::Formula::equivalent ( const Formula & f ) const

Equivalence

Parameters

f a Formula

Returns: true iff (*this) is equivalent to f

Referenced by bdd().

◆ existAbstract()

const Formula& Diades::Sdmdl::Formula::existAbstract	(	const VariableVector &	variables,
		bool	complementSet = `false`
	)		const

Perform the abstraction: "there exists a model satisfying 'variables', such that *this" So called existancial quantification abstraction. Suppose for instance a Formula f defined over the variable v1, v2, v3, v4 and the domain of v1 is {1,2,3} Then the result of the abstraction of over v1 is abst(f) = f|v1=1 or f|v1=2 or f|v1=3 where f|v1=a is the restriction of f over v1=a that is (v1=a) and f

If the Boolean complementSet is set to true then perform the abstraction on the complement set of 'variables'

Parameters

variables	the set of variables to abstract
complementSet	if true, the abstraction is done on the complemented set

Returns: the resulting abstraction

Referenced by Formula().

◆ getModels()

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

Model enumerations

Parameters

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

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

Referenced by Formula(), and Diades::Sdmdl::FormulaFactory::valid().

◆ isAssignment()

bool Diades::Sdmdl::Formula::isAssignment ( ) const

inline

Returns: true if this Formula is an assignment

Definition at line 180 of file Formula.hh.

References Diades::Sdmdl::Value::isNull(), support(), and value().

◆ isCube()

bool Diades::Sdmdl::Formula::isCube ( ) const

Returns: true if the current formula is a cube (that is a simple path from a node to a terminal in the BDD

Referenced by bdd().

◆ isFalse()

bool Diades::Sdmdl::Formula::isFalse ( ) const

Returns: true if the formula is isFalse

Referenced by variable().

◆ isNull()

bool Diades::Sdmdl::Formula::isNull ( ) const

Returns: true if the Formula is null

Referenced by bdd(), Diades::Sdmdl::CubeGenerator::CubeGenerator(), Diades::Sdmdl::Rule::makeEffect(), and Diades::Sdmdl::Rule::makePrecondition().

◆ isTrue()

bool Diades::Sdmdl::Formula::isTrue ( ) const

Returns: true if the formula is isTrue

Referenced by variable().

◆ latexify()

string Diades::Sdmdl::Formula::latexify ( ) const

Returns: the textified Formula

Referenced by bdd().

◆ operator &&()

const Formula& Diades::Sdmdl::Formula::operator&& ( const Formula & f ) const

And operator

Parameters

f a Formula

Returns: the Formula (*this) and f

Referenced by bdd().

◆ operator!()

const Formula& Diades::Sdmdl::Formula::operator! ( ) const

Not operator

Returns: the Formula not (*this)

Referenced by bdd().

◆ operator!=()

bool Diades::Sdmdl::Formula::operator!= ( const Formula & f ) const

inline

Parameters

f	The Formula to compare with

Returns: true if both formula are not the same (reference equality)

Definition at line 265 of file Formula.hh.

◆ operator==()

bool Diades::Sdmdl::Formula::operator== ( const Formula & f ) const

inline

Parameters

f	The Formula to compare with

Returns: true if both formula are the same (reference equality)

Definition at line 254 of file Formula.hh.

◆ operator||()

const Formula& Diades::Sdmdl::Formula::operator|| ( const Formula & f ) const

Or operator

Parameters

f a Formula

Returns: the Formula (*this) or f

Referenced by bdd().

◆ owner()

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

Returns: the underlying factory of this Formula. An invalid factory if the Formula is invalid

Referenced by bdd().

◆ primes()

void Diades::Sdmdl::Formula::primes ( FormulaVector & result ) const

Compute the prime implicants of the Formula F Recall that an implicant of F is a formula I such that I implies F A prime implicant PI is a conjunction of litterals that is an implicant of F such that no subconjunction of litterals in PI is an implicant So 'primes' compute the set of prime implicants PI1,..,PIn of F which means that F is equivalent to PI1 or ... or PIN.

Parameters

result the resulting set of prime implicants

Todo:: efficiency issues due to prime formula redundancies

Referenced by variable().

◆ satisfies()

bool Diades::Sdmdl::Formula::satisfies ( const Formula & f ) const

Parameters

f a Formula

Returns: true if (*this) and f shares at least one model (interpretation)

Referenced by bdd().

◆ support()

const VariableVector& Diades::Sdmdl::Formula::support ( ) const

Returns: the set of Variable involved in this Formula

Referenced by isAssignment(), and variable().

◆ textify()

string Diades::Sdmdl::Formula::textify ( ) const

Returns: the textified Formula

Referenced by bdd().

◆ typeName()

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

inlinestatic

Definition at line 68 of file Formula.hh.

◆ value()

const Value& Diades::Sdmdl::Formula::value ( ) const

Returns: the value associated to the variable() in this assignment in any other case it returns a null value.

Referenced by Diades::Sdmdl::FormulaFactory::context(), and isAssignment().

◆ variable()

const Variable& Diades::Sdmdl::Formula::variable ( ) const

inline

Returns: the variable associated to this assignment

Precondition: isAssignment()

Definition at line 210 of file Formula.hh.

References isFalse(), isTrue(), primes(), and support().

Referenced by Diades::Sdmdl::FormulaFactory::context().

Friends And Related Function Documentation

◆ FormulaFactory

friend class FormulaFactory

friend

Definition at line 428 of file Formula.hh.

◆ operator<<

ostream& operator<<	(	ostream &	os,
		const Formula &	f
	)

friend

Output stream

Parameters

os	the output stream
f	the Formula to print out

Returns: the output stream

Referenced by bdd().

Member Data Documentation

◆ _bdd

BDD Diades::Sdmdl::Formula::_bdd

private

_bdd the underlying Binary Decision Diagram (CUDD package)

Definition at line 81 of file Formula.hh.

Referenced by bdd().

◆ _dataIndex

int Diades::Sdmdl::Formula::_dataIndex

private

_dataIndex the data index

Definition at line 85 of file Formula.hh.

◆ _owner

FormulaFactory* Diades::Sdmdl::Formula::_owner

mutableprivate

_factory the FormulaFactory that created and owns this Formula

Definition at line 89 of file Formula.hh.

◆ _support

VariableVector Diades::Sdmdl::Formula::_support

mutableprivate

_support the support of the Formula

Definition at line 96 of file Formula.hh.

◆ _supportNotComputed

bool Diades::Sdmdl::Formula::_supportNotComputed

mutableprivate

_supportNotComputed the support is not computed yet

Definition at line 103 of file Formula.hh.

◆ _value

ValueVector Diades::Sdmdl::Formula::_value

mutableprivate

_value the potential Value of the Formula if it is an assignment

Definition at line 110 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

Public Types

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ ConstReference

◆ Exception

◆ FormulaVector

◆ Pointer

Member Enumeration Documentation

◆ BinaryOperator

◆ UnaryOperator

Constructor & Destructor Documentation

◆ Formula() [1/2]

◆ Formula() [2/2]

◆ ~Formula()

Member Function Documentation

◆ apply() [1/2]

◆ apply() [2/2]

◆ bdd()

◆ bddManager()

◆ entails()

◆ equivalent()

◆ existAbstract()

◆ getModels()

◆ isAssignment()

◆ isCube()

◆ isFalse()

◆ isNull()

◆ isTrue()

◆ latexify()

◆ operator &&()

◆ operator!()

◆ operator!=()

◆ operator==()

◆ operator||()

◆ owner()

◆ primes()

◆ satisfies()

◆ support()

◆ textify()

◆ typeName()

◆ value()

◆ variable()

Friends And Related Function Documentation

◆ FormulaFactory

◆ operator<<

Member Data Documentation

◆ _bdd

◆ _dataIndex

◆ _owner

◆ _support

◆ _supportNotComputed

◆ _value