solver/Equation.h
```00001 /*
00002  * Equation.h
00003  *
00004  *  Created on: Dec 9, 2008
00005  *      Author: tdillig
00006  */
00007
00008 #ifndef EQUATION_H_
00009 #define EQUATION_H_
00010 #include "bignum.h"
00011
00012 #include <unordered_map>
00013 #include <unordered_set>
00014 #include <string.h>
00015 using namespace __gnu_cxx;
00016 #include <vector>
00017 using namespace std;
00018
00019 #define EQ_ASSERT true
00020
00021 #include "bigfraction.h"
00022
00023 class Equation {
00024         friend class slack_matrix;
00025 public:
00026         data_type* eq;
00027         int cols;
00028         bool infinite;
00029         bool proof;
00030
00031         /*
00032          * Careful! This constructor does NOT finish initializing.
00033          */
00034         inline Equation(int cols, bool infinite)
00035         {
00036                 this->cols = cols;
00037                 eq = new data_type[cols];
00038                 memset(eq, 0, sizeof(data_type) * cols);
00039                 this->infinite = infinite;
00040                 proof = false;
00041         }
00042
00043
00044
00045         inline void set_initial_value(int c, data_type d){
00046                 assert(c>=0 && c<cols);
00047                 if(!infinite){
00048                         eq[c].d = d.d;
00049                         return;
00050                 }
00051                 mpz_init_set(eq[c].i, d.i);
00052         }
00053
00054         inline size_t compute_hash_d()
00055         {
00056                 size_t hash_code = 0;
00057                 for(int i=0; i < cols; i++)
00058                 {
00059                         hash_code+=(eq[i].d<<((5*i)%27));
00060                 }
00061                 return hash_code;
00062         }
00063
00064         inline size_t compute_hash_i()
00065         {
00066                 assert(infinite);
00067                 size_t hash_code = 0;
00068                 for(int i=0; i < cols; i++)
00069                 {
00070                         long int val = mpz_get_si(eq[i].i);
00071                         hash_code+=(val<<((5*i)%27));
00072                 }
00073                 return hash_code;
00074         }
00075
00076         inline void make_infinite()
00077         {
00078                 infinite = true;
00079                 for(int i=0; i < cols; i++){
00080                         long int val = eq[i].d;
00081                         mpz_init_set_si(eq[i].i, val);
00082                 }
00083         }
00084
00085 public:
00086         inline Equation* clone()
00087         {
00088                 Equation* res = new Equation(cols);
00089                 if(!infinite){
00090                         memcpy(res->eq, eq, cols*sizeof(data_type));
00091                         res->infinite = false;
00092                         return res;
00093                 }
00094                 for(int i=0; i < cols; i++) {
00095                         mpz_init_set(res->eq[i].i, eq[i].i);
00096                 }
00097                 res->infinite = true;
00098                 return res;
00099         }
00100         inline void divide(bignum b)
00101         {
00102                 if(!infinite && !b.infinite)
00103                 {
00104                         for(int c=0; c < cols; c++) {
00105                                 eq[c].d/= b.data.d;
00106                         }
00107                         return;
00108                 }
00109                 if(infinite && !b.infinite)
00110                 {
00111                         mpz_t temp;
00112                         mpz_init_set_si(temp, b.data.d);
00113                         for(int c=0; c < cols; c++) {
00114                                 mpz_tdiv_q(eq[c].i, eq[c].i, temp);
00115                         }
00116                         mpz_clear(temp);
00117                         return;
00118                 }
00119
00120                 if(!infinite && b.infinite)
00121                 {
00122                         make_infinite();
00123                 }
00124                 for(int c=0; c < cols; c++) {
00125                         mpz_tdiv_q(eq[c].i, eq[c].i, b.data.i);
00126                 }
00127
00128         }
00129
00130         inline Equation(int cols)
00131         {
00132                 this->cols = cols;
00133                 eq = new data_type[cols];
00134                 memset(eq, 0, sizeof(data_type) * cols);
00135                 this->infinite = false;
00136                 proof = false;
00137         }
00138
00139         inline void set_proof()
00140         {
00141                 proof = true;
00142         }
00143
00144         inline void unset_proof()
00145         {
00146                 proof = false;
00147         }
00148
00149         inline bool is_proof()
00150         {
00151                 return proof;
00152         }
00153
00154         inline bignum compute_gcd(bool skip_last = false)
00155         {
00156                 if(cols == 0) return bignum(0);
00157                 if(infinite) {
00158                         mpz_t gcd;
00159                         mpz_init_set(gcd, eq[0].i);
00160                         mpz_abs(gcd, gcd);
00161                         int end = skip_last? cols-1:cols;
00162                         for(int i=1; i < end; i++) {
00163                                 mpz_gcd(gcd, gcd, eq[i].i);
00164                         }
00165                         bignum b(gcd);
00166                         mpz_clear(gcd);
00167                         return b;
00168                 }
00169                 long int gcd = labs(eq[0].d);
00170                 int end = skip_last? cols-1:cols;
00171                 for(int i=1; i < end; i++) {
00172                         gcd = bignum::compute_int_gcd(gcd, eq[i].d);
00173                 }
00174                 return bignum(gcd);
00175         }
00176
00177         inline int get_cols()
00178         {
00179                 return cols;
00180         }
00181
00182         inline bool satisfies(vector<bigfraction> &a)
00183         {
00184                 assert((int)a.size()==cols-1);
00185                 bigfraction cur;
00186                 for(int i=0; i < cols-1; i++) {
00187                         cur+=a[i]*get(i);
00188                 }
00189                 return cur == get(cols-1);
00190         }
00191
00192         inline bigfraction evaluate(vector<bigfraction>& a)
00193         {
00194                 assert((int)a.size()==cols);
00195                 bigfraction cur;
00196                 for(int i=0; i < cols; i++) {
00197                         cur+=a[i]*get(i);
00198                 }
00199                 return cur;
00200         }
00201
00202         inline void set(int c, const bignum b)
00203         {
00204                 //assert(c>=0 && c < this->cols);
00205
00206                 if(!infinite && !b.infinite) {
00207                         eq[c].d = b.data.d;
00208                         return;
00209                 }
00210                 if(!infinite && b.infinite) {
00211                         make_infinite();
00212                         mpz_set(eq[c].i, b.data.i);
00213                         return;
00214                 }
00215                 if(infinite && !b.infinite) {
00216                         mpz_set_si(eq[c].i, b.data.d);
00217                         return;
00218                 }
00219                 mpz_set(eq[c].i, b.data.i);
00220         }
00221
00222         inline void flip_sign(){
00223                 for(int i=0; i < cols; i++){
00224                         flip_sign(i);
00225                 }
00226
00227         }
00228
00229
00230         inline void flip_sign(int c){
00231                 if(!infinite){
00232                         eq[c].d = -eq[c].d;
00233                         return;
00234                 }
00235                 mpz_neg(eq[c].i, eq[c].i);
00236         }
00237
00238         inline bignum get(int c)
00239         {
00240                 if(!infinite)
00241                         return bignum(eq[c].d);
00242                 return bignum(eq[c].i);
00243         }
00244
00245         inline size_t hash_code()
00246         {
00247                 if(infinite) return compute_hash_i();
00248                 return compute_hash_d();
00249         }
00250
00251         friend ostream& operator <<(ostream &os,const Equation &obj);
00252
00253
00254         inline int num_entries()
00255         {
00256                 return cols;
00257         }
00258
00259         inline string to_string()
00260         {
00261                 string res;
00262                 for(int i=0; i < cols; i++) {
00263                         res+=get(i).to_string() +"\t";
00264                 }
00265                 return res;
00266         }
00267
00268         inline bool operator==(Equation& other)
00269         {
00270                 if(!infinite && !other.infinite){
00271                         for(int i=0; i < cols; i++) {
00272                                 if(eq[i].d!=other.eq[i].d) return false;
00273                         }
00274                         return true;
00275                 }
00276                 if(!infinite && other.infinite){
00277                         for(int i=0; i < cols; i++) {
00278                                 if(mpz_cmp_si(other.eq[i].i, eq[i].d) !=0) return false;
00279                         }
00280                         return true;
00281                 }
00282                 if(infinite && !other.infinite){
00283                         for(int i=0; i < cols; i++) {
00284                                 if(mpz_cmp_si(eq[i].i, other.eq[i].d) !=0) return false;
00285                         }
00286                         return true;
00287                 }
00288                 for(int i=0; i < cols; i++) {
00289                         if(mpz_cmp(eq[i].i, other.eq[i].i) !=0) return false;
00290                 }
00291                 return true;
00292         }
00293         inline bool operator<(Equation& other)
00294         {
00295                 if(!infinite && !other.infinite){
00296                         for(int i=0; i < cols; i++) {
00297                                 if(eq[i].d<other.eq[i].d) return true;
00298                                 if(eq[i].d>other.eq[i].d) return false;
00299                         }
00300                         return false;
00301                 }
00302                 if(!infinite && other.infinite){
00303                         for(int i=0; i < cols; i++) {
00304                                 int res = mpz_cmp_si(other.eq[i].i, eq[i].d);
00305                                 if(res > 0) return true;
00306                                 if(res < 0) return false;
00307                         }
00308                         return false;
00309                 }
00310                 if(infinite && !other.infinite){
00311                         for(int i=0; i < cols; i++) {
00312                                 int res = mpz_cmp_si(eq[i].i, other.eq[i].d);
00313                                 if(res < 0) return true;
00314                                 if(res > 0) return false;
00315                         }
00316                         return false;
00317                 }
00318                 for(int i=0; i < cols; i++) {
00319                         int res = mpz_cmp(eq[i].i, other.eq[i].i);
00320                         if(res < 0) return true;
00321                         if(res > 0) return false;
00322                 }
00323                 return false;
00324         }
00325
00326
00327
00328         inline bool operator!=(Equation& other)
00329         {
00330                 return !(*this==other);
00331         }
00332
00333         inline ~Equation()
00334         {
00335                 if(infinite){
00336                         for(int i=0; i < cols; i++) {
00337                                 mpz_clear(eq[i].i);
00338                         }
00339                 }
00340                 delete[] eq;
00341         }
00342 };
00343
00344 namespace std {
00352 template <>
00353 struct hash<Equation*> {
00354         inline size_t operator() (const Equation*const  & x) const {
00355                 Equation* xx = (Equation*)x;
00356                                 if(EQ_ASSERT) assert(xx != NULL);
00357                 return xx->hash_code();
00358         }
00359         };
00360 }
00361
00362
00363 struct equation_eq
00364 {
00365   inline bool operator()(const Equation*const _e1, const Equation*const _e2) const
00366   {
00367           Equation* e1 = (Equation*)_e1;
00368           Equation* e2 = (Equation*)_e2;
00369           if(EQ_ASSERT) assert(e1 != NULL);
00370           if(EQ_ASSERT) assert(e2 != NULL);
00371           return *e1==*e2;
00372   }
00373 };
00374
00375 struct equation_lt
00376 {
00377   inline bool operator()(const Equation*const _e1, const Equation*const _e2) const
00378   {
00379           Equation* e1 = (Equation*)_e1;
00380           Equation* e2 = (Equation*)_e2;
00381           if(EQ_ASSERT) assert(e1 != NULL);
00382           if(EQ_ASSERT) assert(e2 != NULL);
00383           return *e1<*e2;
00384   }
00385 };
00386
00387
00388 #endif /* EQUATION_H_ */
```