elimination/Cooper.h
00001 /*
00002  * Cooper.h
00003  *
00004  *  Created on: Nov 25, 2011
00005  *      Author: isil
00006  */
00007
00008 #ifndef COOPER_H_
00009 #define COOPER_H_
00010
00011 #include <set>
00012 using namespace std;
00013 #include "bignum.h"
00014
00015 class CNode;
00016 class Term;
00017
00018 class Cooper {
00019 private:
00020         CNode* c;
00021         Term* elim_t;
00022         bignum delta;
00023         set<Term*> a_terms; // x<a
00024         set<Term*> b_terms; // b<x
00025         CNode* res;
00026
00027 public:
00028         Cooper(CNode* c, Term* elim_t);
00029         CNode* get_result();
00030         ~Cooper();
00031 private:
00032
00033         /*
00034          * Rewrites the formula Ex. F to an equivalent formula Ex. F'
00035          * such that no leaf in the formula contains x with coefficients.
00036          */
00037         void remove_coefficients();
00038
00039         void collect_coefficients(CNode* c, set<bignum>& coefficients);
00040
00041         bignum get_lcm(set<bignum>& coefs);
00042
00043         CNode* normalize_coefficients(CNode* c, bignum lcm);
00044
00045         /*
00046          * delta is defined same way as in the Cooper paper, i.e.,
00047          * lcm of constants in the mod terms
00048          */
00049         bignum compute_delta();
00050         bignum compute_delta_rec(bignum delta, CNode* c);
00051
00052         /*
00053          * Compute terms a such that x<a and terms b such that b<x
00054          */
00055         void compute_a_and_b_terms(CNode* c, bool in_neg);
00056
00057
00058         /*
00059          * Computes the left or right infinite projection of c
00060          */
00061         CNode* compute_infinite_projection(CNode* c, bool left,
00062                         Term* rt);
00063
00064
00065
00066
00067 };
00068
00069 #endif /* COOPER_H_ */