PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00014 //***************************************************************************** 00015 00016 #ifndef polybori_groebner_fixed_path_divisors_h_ 00017 #define polybori_groebner_fixed_path_divisors_h_ 00018 00019 // include basic definitions 00020 #include "groebner_defs.h" 00021 00022 BEGIN_NAMESPACE_PBORIGB 00023 00024 #ifndef DANGEROUS_FIXED_PATH 00025 typedef PBORI::CacheManager<CCacheTypes::divisorsof_fixedpath> 00026 #else 00027 typedef PBORI::CacheManager<CCacheTypes::divisorsof> 00028 #endif 00029 fixed_divisors_cache_type; 00030 00031 // Variant navigator 00032 inline MonomialSet 00033 do_fixed_path_divisors(const fixed_divisors_cache_type & cache_mgr, 00034 MonomialSet::navigator a_nav, 00035 MonomialSet::navigator m_nav, 00036 MonomialSet::navigator n_nav){ 00037 00038 if (n_nav.isTerminated()) return 00039 MonomialSet(cache_mgr.generate(a_nav)).firstDivisorsOf(cache_mgr.generate(m_nav)); 00040 PBORI_ASSERT(!(n_nav.isConstant()&&(!(n_nav.terminalValue())))); 00041 00042 if (a_nav.isConstant()) return cache_mgr.generate(a_nav); 00043 00044 PBORI_ASSERT(!(n_nav.isConstant())); 00045 PBORI_ASSERT(!(m_nav.isConstant())); 00046 int m_index=*m_nav; 00047 int n_index=*n_nav; 00048 int a_index=*a_nav; 00049 00050 PBORI_ASSERT(m_index<=n_index); 00051 00052 00053 //here we rely on the fact, that in Cudd deref of constant nav. gives a bigger index than allow allowed real indices 00054 while((a_index=*a_nav)!=(m_index=*m_nav)){ 00055 if (a_index<m_index) a_nav.incrementElse(); 00056 else{ 00057 n_index=*n_nav; 00058 PBORI_ASSERT(n_index>=m_index); 00059 if (m_index==n_index){ 00060 n_nav.incrementThen(); 00061 m_nav.incrementThen(); 00062 } else { 00063 m_nav.incrementThen(); 00064 } 00065 } 00066 00067 } 00068 n_index=*n_nav; 00069 00070 if (a_nav.isConstant()){ 00071 return cache_mgr.generate(a_nav); 00072 } 00073 PBORI_ASSERT((*a_nav)==(*m_nav)); 00074 00075 MonomialSet::navigator cached; 00076 #ifndef DANGEROUS_FIXED_PATH 00077 cached = 00078 cache_mgr.find(a_nav, m_nav,n_nav); 00079 if (cached.isValid() ){ 00080 return cache_mgr.generate(cached); 00081 } 00082 #else 00083 //MonomialSet::navigator cached = 00084 //cache_mgr.find(a_nav, m_nav); 00085 #endif 00086 00087 00088 // here it is theoretically possible to get answers which don't contain the 00089 // fixed path n, but that doesn't matter in practice, 00090 // as it is optimization anyway 00091 typedef PBORI::CacheManager<CCacheTypes::divisorsof> 00092 cache_mgr_type2; 00093 00094 cache_mgr_type2 cache_mgr2(cache_mgr.manager()); 00095 00096 cached = 00097 cache_mgr2.find(a_nav, m_nav); 00098 00099 if (cached.isValid()){ 00100 return cache_mgr2.generate(cached); 00101 } 00102 00103 PBORI_ASSERT(a_index==m_index); 00104 int index=m_index; 00105 MonomialSet result(cache_mgr.zero()); 00106 if (m_index==n_index){ 00107 result=do_fixed_path_divisors(cache_mgr, a_nav.thenBranch(), 00108 m_nav.thenBranch(), n_nav.thenBranch()); 00109 if (!(result.isZero())) 00110 result = MonomialSet(index, result, cache_mgr.zero()); 00111 } else { 00112 MonomialSet 00113 then_path=do_fixed_path_divisors(cache_mgr, a_nav.thenBranch(), 00114 m_nav.thenBranch(), n_nav); 00115 MonomialSet 00116 else_path=do_fixed_path_divisors(cache_mgr, a_nav.elseBranch(), 00117 m_nav.thenBranch(), n_nav); 00118 if (then_path.isZero()){ 00119 result=else_path; 00120 } else { 00121 result=MonomialSet(index,then_path,else_path); 00122 } 00123 } 00124 #ifndef DANGEROUS_FIXED_PATH 00125 cache_mgr.insert(a_nav,m_nav,n_nav,result.navigation()); 00126 #else 00127 cache_mgr2.insert(a_nav,m_nav,result.navigation()); 00128 #endif 00129 return result; 00130 } 00131 // end of variant for navigator 00132 00133 // variant for MonomialSet 00134 inline MonomialSet 00135 do_fixed_path_divisors(MonomialSet a, 00136 MonomialSet m, MonomialSet n){ 00137 00138 //we assume that m is a multiple of n 00139 MonomialSet::navigator m_nav=m.navigation(); 00140 MonomialSet::navigator n_nav=n.navigation(); 00141 00142 MonomialSet::navigator a_nav=a.navigation(); 00143 00144 typedef fixed_divisors_cache_type cache_mgr_type; 00145 cache_mgr_type cache_mgr(a.ring()); 00146 00147 return do_fixed_path_divisors(cache_mgr, a_nav, m_nav, n_nav); 00148 } 00149 00150 00151 inline MonomialSet 00152 fixed_path_divisors(MonomialSet a, Monomial m, Monomial n){ 00153 PBORI_ASSERT(m.reducibleBy(n)); 00154 return do_fixed_path_divisors(a,m.diagram(),n.diagram()); 00155 } 00156 00157 00158 END_NAMESPACE_PBORIGB 00159 00160 #endif /* polybori_groebner_fixed_path_divisors_h_ */