PolyBoRi
LiteralFactorization.h
Go to the documentation of this file.
1 /*
2  * LiteralFactorization.h
3  * PolyBoRi
4  *
5  * Created by Michael Brickenstein on 29.05.06.
6  * Copyright 2006 The PolyBoRi Team. See LICENSE file.
7  *
8  */
9 
10 #include <algorithm>
11 #include <vector>
12 #include <map>
13 #include <set>
14 #include <utility>
15 #include "groebner_defs.h"
16 
17 #ifndef PBORI_GB_LF_H
18 #define PBORI_GB_LF_H
20 
21 std::vector<Polynomial> easy_linear_factors(const Polynomial &p);
22 
23 class LiteralFactorizationIterator; // forward declaration
25 
26 public:
29 
30  typedef std::map<idx_type, int> map_type;
31  map_type factors;
34  bool occursAsLeadOfFactor(idx_type v) const;
35  bool trivial() const;
36  bool is11Factorization() const;
37  bool is00Factorization() const;
38  //Theorem: f BoolePolynomial with factor (x+b), b in 0, 1 (considered in the usual Polynomial Ring)
39  //then f/(x+b) does not involve the variable x
40  //typedef std::pair<idx_type,idx_type> var_pair_type;
41  //typedef std::set<var_pair_type> two_var_factors;
42  typedef std::map<idx_type, idx_type> var2var_map_type;
43  var2var_map_type var2var_map;
44 
45  const_iterator begin();
46  const_iterator end();
47 };
48 
50 
53 
55 #endif
deg_type common_literal_factors_deg(const LiteralFactorization &a, const LiteralFactorization &b)
Definition: LiteralFactorization.cc:319
This class defines LiteralFactorizationIterator.
Definition: LiteralFactorizationIterator.h:36
deg_type lmDeg
Definition: LiteralFactorization.h:33
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
Polynomial rest
Definition: LiteralFactorization.h:32
Definition: LiteralFactorization.h:24
int deg_type
Definition: groebner_defs.h:42
var2var_map_type var2var_map
Definition: LiteralFactorization.h:43
BoolePolynomial Polynomial
Definition: embed.h:51
#define BEGIN_NAMESPACE_PBORIGB
Definition: groebner_defs.h:15
std::map< idx_type, int > map_type
Definition: LiteralFactorization.h:30
This class wraps the underlying decicion diagram type and defines the necessary operations.
Definition: BoolePolynomial.h:85
Polynomial multiply_with_literal_factors(const LiteralFactorization &lf, Polynomial p)
Definition: LiteralFactorization.cc:423
map_type factors
Definition: LiteralFactorization.h:31
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
std::vector< Polynomial > easy_linear_factors(const Polynomial &p)
Definition: LiteralFactorization.cc:19
LiteralFactorizationIterator const_iterator
Definition: LiteralFactorization.h:27
std::map< idx_type, idx_type > var2var_map_type
Definition: LiteralFactorization.h:42