#include "pbori_defs.h"
#include "pbori_func.h"
#include "CCuddNavigator.h"
Go to the source code of this file.
Classes | |
class | dd_operations< CTypes::dd_type::navigator > |
Functions | |
BEGIN_NAMESPACE_PBORI void | inc_ref (DdNode *node) |
template<class NaviType > | |
void | inc_ref (const NaviType &navi) |
void | dec_ref (DdNode *node) |
template<class NaviType > | |
void | dec_ref (const NaviType &navi) |
DdNode * | do_get_node (DdNode *node) |
template<class NaviType > | |
DdNode * | do_get_node (const NaviType &navi) |
template<class MgrType > | |
void | recursive_dec_ref (const MgrType &mgr, DdNode *node) |
template<class MgrType , class NaviType > | |
void | recursive_dec_ref (const MgrType &mgr, const NaviType &navi) |
template<class NaviType , class ReverseIterator , class DDOperations > | |
NaviType | indexed_term_multiples (NaviType navi, ReverseIterator idxStart, ReverseIterator idxFinish, const DDOperations &apply) |
template<class NaviType > | |
bool | is_reducible_by (NaviType first, NaviType second) |
template<class NaviType , class ReverseIterator , class DDOperations > | |
NaviType | minimal_of_two_terms (NaviType navi, NaviType &multiples, ReverseIterator idxStart, ReverseIterator idxFinish, const DDOperations &apply) |
template<class NaviType , class SizeType , class ReverseIterator , class DDOperations > | |
NaviType | prepend_multiples_wrt_indices (NaviType navi, SizeType minIdx, ReverseIterator start, ReverseIterator finish, const DDOperations &apply) |
template<class FunctionType , class ManagerType , class NodeType > | |
void | apply_assign_cudd_function (FunctionType func, ManagerType &mgr, NodeType &first, const NodeType &second) |
template<class FunctionType , class ManagerType , class ResultType , class NodeType > | |
void | apply_replacing_cudd_function (FunctionType func, ManagerType &mgr, ResultType &newNode, const NodeType &first, const NodeType &second) |
template<class FunctionType , class ManagerType , class NodeType > | |
NodeType | apply_cudd_function (FunctionType func, ManagerType &mgr, const NodeType &first, const NodeType &second) |
template<class NaviType , class DDType2 , class ReverseIterator , class DDOperations > | |
NaviType | dd_minimal_elements (NaviType navi, DDType2 &multiples, ReverseIterator idxStart, ReverseIterator idxEnd, const DDOperations &apply) |
This file includes some templates of simple transformations and similar procedures.
void apply_assign_cudd_function | ( | FunctionType | func, | |
ManagerType & | mgr, | |||
NodeType & | first, | |||
const NodeType & | second | |||
) | [inline] |
References do_get_node(), inc_ref(), and recursive_dec_ref().
Referenced by dd_operations< CTypes::dd_type::navigator >::diffAssign(), and dd_operations< CTypes::dd_type::navigator >::uniteAssign().
NodeType apply_cudd_function | ( | FunctionType | func, | |
ManagerType & | mgr, | |||
const NodeType & | first, | |||
const NodeType & | second | |||
) | [inline] |
References do_get_node(), and inc_ref().
Referenced by dd_operations< CTypes::dd_type::navigator >::diff().
void apply_replacing_cudd_function | ( | FunctionType | func, | |
ManagerType & | mgr, | |||
ResultType & | newNode, | |||
const NodeType & | first, | |||
const NodeType & | second | |||
) | [inline] |
References do_get_node(), inc_ref(), and recursive_dec_ref().
Referenced by dd_operations< CTypes::dd_type::navigator >::replacingUnite().
NaviType dd_minimal_elements | ( | NaviType | navi, | |
DDType2 & | multiples, | |||
ReverseIterator | idxStart, | |||
ReverseIterator | idxEnd, | |||
const DDOperations & | apply | |||
) | [inline] |
A first version Function templates extracting minimal elements of dd wrt. inclusion Assumption, navi is navigator of dd
References dd_minimal_elements(), inc_ref(), indexed_term_multiples(), is_reducible_by(), minimal_of_two_terms(), and prepend_multiples_wrt_indices().
void dec_ref | ( | const NaviType & | navi | ) | [inline] |
void dec_ref | ( | DdNode * | node | ) | [inline] |
DdNode* do_get_node | ( | const NaviType & | navi | ) | [inline] |
DdNode* do_get_node | ( | DdNode * | node | ) | [inline] |
Referenced by apply_assign_cudd_function(), apply_cudd_function(), and apply_replacing_cudd_function().
void inc_ref | ( | const NaviType & | navi | ) | [inline] |
BEGIN_NAMESPACE_PBORI void inc_ref | ( | DdNode * | node | ) | [inline] |
NaviType indexed_term_multiples | ( | NaviType | navi, | |
ReverseIterator | idxStart, | |||
ReverseIterator | idxFinish, | |||
const DDOperations & | apply | |||
) | [inline] |
References inc_ref().
Referenced by dd_minimal_elements(), and minimal_of_two_terms().
bool is_reducible_by | ( | NaviType | first, | |
NaviType | second | |||
) | [inline] |
Referenced by dd_minimal_elements().
NaviType minimal_of_two_terms | ( | NaviType | navi, | |
NaviType & | multiples, | |||
ReverseIterator | idxStart, | |||
ReverseIterator | idxFinish, | |||
const DDOperations & | apply | |||
) | [inline] |
!!!!!!!!!!!!
elseTail = elseNavi;
Cudd_Ref(elseTail); 1 elseMult = elseTail;
!2 thenTail = thenNavi;
!1 thenMult= thenTail;
References indexed_term_multiples(), and prepend_multiples_wrt_indices().
Referenced by dd_minimal_elements().
NaviType prepend_multiples_wrt_indices | ( | NaviType | navi, | |
SizeType | minIdx, | |||
ReverseIterator | start, | |||
ReverseIterator | finish, | |||
const DDOperations & | apply | |||
) | [inline] |
Referenced by dd_minimal_elements(), and minimal_of_two_terms().
void recursive_dec_ref | ( | const MgrType & | mgr, | |
const NaviType & | navi | |||
) | [inline] |
void recursive_dec_ref | ( | const MgrType & | mgr, | |
DdNode * | node | |||
) | [inline] |
Referenced by apply_assign_cudd_function(), apply_replacing_cudd_function(), dd_operations< CTypes::dd_type::navigator >::kill(), dd_operations< CTypes::dd_type::navigator >::newNodeAssign(), dd_operations< CTypes::dd_type::navigator >::replace(), and dd_operations< CTypes::dd_type::navigator >::replacingNode().