contained_variables.h
Go to the documentation of this file.
// -*- c++ -*-
//*****************************************************************************
//*****************************************************************************
#ifndef polybori_groebner_contained_variables_h_
#define polybori_groebner_contained_variables_h_
// include basic definitions
#include "groebner_defs.h"
BEGIN_NAMESPACE_PBORIGB
inline MonomialSet
contained_variables_cudd_style(const MonomialSet& m){
MonomialSet::navigator nav=m.navigation();
MonomialSet::navigator orig=nav;
typedef PBORI::CacheManager<CCacheTypes::contained_variables>
cache_mgr_type;
cache_mgr_type cache_mgr(m.ring());
while (!(nav.isConstant())){
MonomialSet::navigator cached =
cache_mgr.find(nav);
if (cached.isValid()) return cache_mgr.generate(cached);
idx_type v=*nav;
MonomialSet::navigator check_nav=nav.thenBranch();
while(!(check_nav.isConstant())){
check_nav.incrementElse();
}
if (check_nav.isTerminated()){
idx_type result_index=v;
MonomialSet result=MonomialSet(result_index,Polynomial(cache_mgr.one()).diagram(),contained_variables_cudd_style(cache_mgr.generate(nav.elseBranch())));
MonomialSet::navigator r_nav=result.navigation();
while(1){
MonomialSet::navigator last=orig;
cache_mgr.insert(orig, r_nav);
orig.incrementElse();
if(last==nav) break;
}
return result;
}
nav.incrementElse();
}
return MonomialSet(cache_mgr.zero());
}
inline MonomialSet
contained_deg2_cudd_style(const MonomialSet& m){
MonomialSet::navigator nav=m.navigation();
typedef PBORI::CacheManager<CCacheTypes::contained_deg2>
cache_mgr_type;
cache_mgr_type cache_mgr(m.ring());
if (!(nav.isConstant())){
MonomialSet::navigator cached =
cache_mgr.find(nav);
if (cached.isValid()) return cache_mgr.generate(cached);
MonomialSet::navigator then_branch=nav.thenBranch();
MonomialSet::navigator else_branch=nav.elseBranch();
MonomialSet then_res=contained_variables_cudd_style(cache_mgr.generate(then_branch));
MonomialSet else_res=contained_deg2_cudd_style(cache_mgr.generate(else_branch));
MonomialSet result=MonomialSet(*nav,then_res,else_res);
cache_mgr.insert(nav,result.navigation());
return result;
}
else return MonomialSet(cache_mgr.zero());
}
inline std::vector<idx_type>
contained_variables(const MonomialSet& m){
std::vector<idx_type> result;
MonomialSet::navigator nav=m.navigation();
while (!(nav.isConstant())){
idx_type v=*nav;
MonomialSet::navigator check_nav=nav.thenBranch();
while(!(check_nav.isConstant())){
check_nav.incrementElse();
}
if (check_nav.isTerminated()){
result.push_back(v);
}
nav.incrementElse();
}
return result;
}
END_NAMESPACE_PBORIGB
#endif /* polybori_groebner_contained_variables_h_ */
polybori::groebner::contained_deg2_cudd_style
MonomialSet contained_deg2_cudd_style(const MonomialSet &m)
Definition: contained_variables.h:63
polybori::groebner::contained_variables
std::vector< idx_type > contained_variables(const MonomialSet &m)
Definition: contained_variables.h:91
polybori::groebner::contained_variables_cudd_style
MonomialSet contained_variables_cudd_style(const MonomialSet &m)
Definition: contained_variables.h:25
END_NAMESPACE_PBORIGB
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
polybori::Polynomial
BoolePolynomial Polynomial
Definition: embed.h:51
polybori::CCuddDDFacade::navigation
navigator navigation() const
Navigate through ZDD by incrementThen(), incrementElse(), and terminated()
Definition: CCuddDDFacade.h:455
BEGIN_NAMESPACE_PBORIGB
#define BEGIN_NAMESPACE_PBORIGB
Definition: groebner_defs.h:15
polybori::CCuddNavigator::elseBranch
self elseBranch() const
Increment in else direction.
Definition: CCuddNavigator.h:98
polybori::CCuddDDFacade::ring
const ring_type & ring() const
Get reference to ring.
Definition: CCuddDDFacade.h:250
polybori::groebner::MonomialSet
polybori::BooleSet MonomialSet
Definition: groebner_defs.h:45
groebner_defs.h
polybori::CCuddNavigator::isTerminated
bool_type isTerminated() const
Check whether end of path was reached.
Definition: CCuddNavigator.h:128
polybori::CCuddNavigator::thenBranch
self thenBranch() const
Increment in then direction.
Definition: CCuddNavigator.h:92
polybori::groebner::idx_type
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
polybori::CCuddNavigator::isValid
bool_type isValid() const
Check whether *this is not the default iterator self() (NULL pointer)
Definition: CCuddNavigator.h:125
polybori::CCuddNavigator::isConstant
bool_type isConstant() const
Check whether constant node was reached.
Definition: CCuddNavigator.h:172
polybori::CCuddNavigator
This class defines an iterator for navigating through then and else branches of ZDDs.
Definition: CCuddNavigator.h:36
polybori::CCuddNavigator::incrementElse
self & incrementElse()
Increment in else direction.
Definition: CCuddNavigator.h:203
polybori::BooleSet
Definition: BooleSet.h:57