/*------------------------------------------------------------------------*/ /*! \file polynomial.h \brief contains arithmetic operations for polynomials Part of AMulet2.1 : AIG Multiplier Verification Tool. Copyright(C) 2020, 2021 Daniela Kaufmann, Johannes Kepler University Linz */ /*------------------------------------------------------------------------*/ #ifndef AMULET2_SRC_POLYNOMIAL_H_ #define AMULET2_SRC_POLYNOMIAL_H_ /*------------------------------------------------------------------------*/ #include #include #include #include "monomial.h" /*------------------------------------------------------------------------*/ /** \class Polynomial This class is used to polynomials. */ class Polynomial { int idx; // /< index as used in pac proofs int level = 1; // /< level of polynomials needed for certificates Monomial ** mon; // /< sorted deque of monomials public: size_t num_mon = 0; /** Constructor */ Polynomial(); Polynomial (Monomial ** m, size_t len); /** Getter for member idx @return integer */ int get_idx() const {return idx;} /** Setter for idx @param idx_ integer */ void set_idx(int idx_) {idx = idx_;} /** Getter for member level @return integer */ int get_level() const {return level;} /** Setter for level @param level_ integer */ void set_level(int level_) {level = level_;} Monomial * get_mon(size_t i) const { if(i < num_mon) return mon[i]; else return 0; } size_t size() const { return num_mon;} /** Returns the leading term @return Term* */ Term * get_lt() const {return mon[0]->get_term();} /** Copy routine @return A hard copy of the current polynomial */ Polynomial * copy() const; /** Printing routine @param file Output file @param end if true we print trailing ";" */ void print(FILE * file, bool end = 1) const; /** Destructor */ ~Polynomial(); /** Returns whether the polynomial is the constant zero polynomial @return bool */ bool is_constant_zero_poly() const; /** Returns whether the polynomial is the constant one polynomial @return bool */ bool is_constant_one_poly() const; /** Returns the size of the smallest term @return integer */ int min_term_size() const; }; /*------------------------------------------------------------------------*/ // Polynomials are generated using a sorted array "mstack" /** Enlarges the allocated size of mstack */ void enlarge_mstack(); /** Sets the number of elements in the stack to 0 */ void clear_mstack(); /** Deallocates mstack */ void deallocate_mstack(); /** Checks whether mstack is empty @return true if mstack is empty */ bool mstack_is_empty(); /** Pushes a monomial to the end of the stack @param t monomial to be added to the mstack */ void push_mstack_end(Monomial *t); /** Pushes a monomial to the stack such that mstack remains sorted @param t monomial to be added to the mstack */ void push_mstack(Monomial *t); /** Generates a polynomial from mstack and clears mstack @return Polynomial* */ Polynomial * build_poly(); /*------------------------------------------------------------------------*/ /** Add two polynomials p1+p2 @param p1 Polynomial* @param p2 Polynomial* @return Polynomial*, sum of p1+p2 */ Polynomial * add_poly(const Polynomial *p1, const Polynomial *p2); /** Multiplies two polynomials p1*p2 @param p1 Polynomial* @param p2 Polynomial* @return Polynomial*, product of p1*p2 */ Polynomial * multiply_poly(const Polynomial *p1, const Polynomial *p2); /** Multiplies a polynomial p1 with a constant c @param p1: Polynomial* @param c: mpz_t object @return Polynomial*, product of c*p1 */ Polynomial * multiply_poly_with_constant(const Polynomial *p1, mpz_t c); /** Returns the quotient of dividing a polynomial p1 by a term t @param p1 Polynomial* @param t Term * @return Polynomial defining the quotient of p1/t */ Polynomial * divide_by_term(const Polynomial * p1, const Term * t); /*---------------------------------------------------------------------------*/ // / gmp for 1 extern mpz_t one; // / gmp for -1 extern mpz_t minus_one; // / gmp for 2 extern mpz_t two; // / gmp for -2 extern mpz_t minus_two; // / gmp for 4 extern mpz_t four; // / gmp for -4 extern mpz_t minus_four; // / gmp for 2 extern mpz_t base; // / gmp for 2^NN extern mpz_t mod_coeff; /*---------------------------------------------------------------------------*/ /** Initializes all global gmp objects @param exp unsigned exponent for mod coeff */ void init_mpz(unsigned exp); /** Clears all globally allocated gmp objects */ void clear_mpz(); #endif // AMULET2_SRC_POLYNOMIAL_H_