LLReduction.h
Go to the documentation of this file.
// -*- c++ -*-
//*****************************************************************************
//*****************************************************************************
#ifndef polybori_groebner_LLReduction_h_
#define polybori_groebner_LLReduction_h_
// include basic definitions
#include "groebner_defs.h"
BEGIN_NAMESPACE_PBORIGB
template <bool have_redsb, bool single_call_for_noredsb,
bool fast_multiplication>
class LLReduction {
public:
template<class RingType>
LLReduction(const RingType& ring): cache_mgr(ring) {}
Polynomial multiply(const Polynomial &p, const Polynomial& q){
typedef CommutativeCacheManager<CCacheTypes::multiply_recursive>
cache_mgr_type;
return dd_multiply<fast_multiplication>(cache_mgr_type(p.ring()),
p.navigation(), q.navigation(),
BoolePolynomial(p.ring()));
}
Polynomial operator()(const Polynomial& p, MonomialSet::navigator r_nav);
protected:
typedef PBORI::CacheManager<CCacheTypes::ll_red_nf> cache_mgr_type;
cache_mgr_type cache_mgr;
};
template <bool have_redsb, bool single_call_for_noredsb, bool fast_multiplication>
Polynomial
LLReduction<have_redsb, single_call_for_noredsb,
fast_multiplication>::operator() (const Polynomial& p,
MonomialSet::navigator r_nav) {
if PBORI_UNLIKELY(p.isConstant()) return p;
MonomialSet::navigator p_nav=p.navigation();
idx_type p_index=*p_nav;
while((*r_nav)<p_index) {
r_nav.incrementThen();
}
if PBORI_UNLIKELY(r_nav.isConstant())
return p;
MonomialSet::navigator cached = cache_mgr.find(p_nav, r_nav);
if PBORI_LIKELY(cached.isValid())
return MonomialSet(cache_mgr.generate(cached));
Polynomial res(0, p.ring());
Polynomial p_nav_else(cache_mgr.generate(p_nav.elseBranch()));
Polynomial p_nav_then(cache_mgr.generate(p_nav.thenBranch()));
if ((*r_nav) == p_index){
Polynomial r_nav_else(cache_mgr.generate(r_nav.elseBranch()));
if ((!have_redsb) && single_call_for_noredsb) {
res = operator()(p_nav_else + multiply(r_nav_else, p_nav_then),
r_nav.thenBranch());
}
else {
Polynomial tmp1 = operator()(p_nav_else, r_nav.thenBranch());
Polynomial tmp2 = operator()(p_nav_then, r_nav.thenBranch());
Polynomial tmp( have_redsb? r_nav_else:
operator()(r_nav_else, r_nav.thenBranch()) );
res = tmp1 + multiply(tmp, tmp2);
}
}
else{
PBORI_ASSERT((*r_nav)>p_index);
res = MonomialSet( p_index,
operator()(p_nav_then, r_nav).diagram(),
operator()(p_nav_else, r_nav).diagram());
}
cache_mgr.insert(p_nav, r_nav, res.navigation());
return res;
}
END_NAMESPACE_PBORIGB
#endif /* polybori_LLReduction_h_ */
polybori::groebner::LLReduction::LLReduction
LLReduction(const RingType &ring)
Definition: LLReduction.h:34
polybori::BoolePolynomial::navigation
navigator navigation() const
Navigate through structure.
Definition: BoolePolynomial.h:441
END_NAMESPACE_PBORIGB
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
polybori::CacheManager< CCacheTypes::ll_red_nf >
polybori::BoolePolynomial::ring
const ring_type & ring() const
Access ring, where this belongs to.
Definition: BoolePolynomial.h:478
polybori::groebner::LLReduction::cache_mgr_type
polybori::CacheManager< CCacheTypes::ll_red_nf > cache_mgr_type
Definition: LLReduction.h:48
BEGIN_NAMESPACE_PBORIGB
#define BEGIN_NAMESPACE_PBORIGB
Definition: groebner_defs.h:15
polybori::BoolePolynomial
This class wraps the underlying decicion diagram type and defines the necessary operations.
Definition: BoolePolynomial.h:85
PBORI_LIKELY
#define PBORI_LIKELY(expression)
For optimizing if-branches.
Definition: pbori_defs.h:56
polybori::CommutativeCacheManager
Definition: CacheManager.h:48
polybori::groebner::MonomialSet
polybori::BooleSet MonomialSet
Definition: groebner_defs.h:45
groebner_defs.h
polybori::groebner::multiply
Polynomial multiply(const Polynomial &p, const Polynomial &q)
Definition: ll_red_nf.h:34
PBORI_ASSERT
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
polybori::CCuddNavigator::incrementThen
self & incrementThen()
Increment in then direction.
Definition: CCuddNavigator.h:191
polybori::groebner::LLReduction::multiply
Polynomial multiply(const Polynomial &p, const Polynomial &q)
Definition: LLReduction.h:36
polybori::groebner::LLReduction::cache_mgr
cache_mgr_type cache_mgr
Definition: LLReduction.h:49
polybori::groebner::idx_type
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
polybori::CCuddNavigator
This class defines an iterator for navigating through then and else branches of ZDDs.
Definition: CCuddNavigator.h:36
PBORI_UNLIKELY
#define PBORI_UNLIKELY(expression)
Definition: pbori_defs.h:59
polybori::groebner::LLReduction
This class defines LLReduction.
Definition: LLReduction.h:30