00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00300 #ifndef soe_INCLUDED
00301 #define soe_INCLUDED "soe.h"
00302
00303 #ifdef _KEEP_RCS_ID
00304 static char *soe_rcs_id = soe_INCLUDED "$Revision: 1.6 $";
00305 #endif
00306
00307 #ifndef _defs_INCLUDED
00308 #include "defs.h"
00309 #endif
00310 #ifndef _defs_INCLUDED
00311 #include "cxx_memory.h"
00312 #endif
00313 #ifndef mat_INCLUDED
00314 #include "lnopt_main.h"
00315 #include "mat.h"
00316 #endif
00317 #ifndef INFIN_DECLARE
00318 #include "infin.h"
00319 #endif
00320
00321
00322
00323 #ifdef LNO
00324 #ifndef lnoutils_INCLUDED
00325 #include "lnoutils.h"
00326 #endif
00327 #endif
00328
00329
00330 enum SVPC_RESULT { SVPC_CONSISTENT,SVPC_INCONSISTENT,SVPC_INAPPLICABLE };
00331 enum ACY_RESULT { ACY_CONSISTENT,ACY_INCONSISTENT,ACY_INAPPLICABLE };
00332
00333
00334 class SYSTEM_OF_EQUATIONS {
00335 public:
00336
00337 SYSTEM_OF_EQUATIONS(INT32 eqns_le,INT32 eqns_eq,INT32 vars, MEM_POOL *pool)
00338 : _Ale(eqns_le,vars,pool), _Aeq(eqns_eq,vars,pool) {
00339 _pool = pool;
00340 _ble = CXX_NEW_ARRAY(mINT64,eqns_le,pool);
00341 _beq = CXX_NEW_ARRAY(mINT64,eqns_eq,pool);
00342 _eqns_le = _eqns_eq = 0;
00343 _eqns_le_stored = eqns_le;
00344 _eqns_eq_stored = eqns_eq;
00345 _vars = vars;
00346 _work_rows = _work_rows_eq = 0;
00347 }
00348 SYSTEM_OF_EQUATIONS(const SYSTEM_OF_EQUATIONS *soe, MEM_POOL *pool);
00349 ~SYSTEM_OF_EQUATIONS() {
00350 CXX_DELETE_ARRAY(_ble,_pool);
00351 CXX_DELETE_ARRAY(_beq,_pool);
00352 }
00353
00354 INT32 Num_Eq_Constraints() const { return(_eqns_eq); }
00355 INT32 Num_Le_Constraints() const { return(_eqns_le); }
00356 INT32 Num_Vars() const { return(_vars); }
00357 void Add_Eq(const mINT32 row[], INT64 b);
00358 void Add_Eq(INT num_rows);
00359 void Add_Le(const mINT32 row[], INT64 b);
00360 BOOL Add_Le_Non_Redundant(const mINT32 row[], INT64 b);
00361 void Add_Le(INT num_rows);
00362 void Add_Vars(const INT32 num_vars);
00363 void Add_Soe(const SYSTEM_OF_EQUATIONS* soe);
00364 void Zero_Row_Le(INT32 r);
00365 void Complement_Le(INT32 r);
00366 INT32 Leftmost_Non_Zero_Le(INT32 r) const;
00367 void Sort_Le(INT* sort_criteria, BOOL descending = FALSE);
00368
00369 void Remove_Last_Eq(INT how_many=1) { _eqns_eq-=how_many; }
00370 void Remove_Last_Le(INT how_many=1) { _eqns_le-=how_many; }
00371 void Remove_Eq_Number(INT which);
00372 void Remove_Le_Number(INT which);
00373 void Remove_Last_Vars(INT num_vars);
00374 void Reset_To(INT32 nrows_le, INT32 nrows_eq, INT32 ncols);
00375
00376 BOOL Is_Consistent();
00377 void Mark_Redundant (BOOL *is_redundant);
00378 INT16 Mark_Simple_Redundant(BOOL *is_redundant);
00379 INT16 Mark_New_Redundant(BOOL *is_redundant);
00380 BOOL Copy_To_Work();
00381 void Add_Work_Le();
00382 void Add_Work_Le_Non_Simple_Redundant();
00383 BOOL Sub_In_Equal(BOOL *proved_inconsistent);
00384 static BOOL Project(const INT32 i,BOOL *proved_inconsistent,
00385 const INT32 min_var=0);
00386 INT Change_Base(const INT32 dim, const INT32 pos, MEM_POOL *pool);
00387 void Take_Gcds();
00388 const IMAT& Aeq() const { return(_Aeq); }
00389 IMAT& Aeq() { return(_Aeq); }
00390 const IMAT& Ale() const { return(_Ale); }
00391 IMAT& Ale() { return(_Ale); }
00392 mINT64 *Beq() { return(_beq); }
00393 const mINT64 *Beq() const { return(_beq); }
00394 mINT64 *Ble() { return(_ble); }
00395 const mINT64 *Ble() const { return(_ble); }
00396 mINT32 Work(const INT32 i, const INT32 j) const { return _work[i][j]; }
00397 mINT64 Work_Const(const INT32 i) const { return _work_const[i]; }
00398 mINT32 Work_Constraints() const { return _work_rows; }
00399 INT32 Simple_Redundant(const INT32 r1, const INT32 r2)
00400 { return Simple_Redundant(&_work[r1][0],&_work[r2][0],
00401 _work_const[r1], _work_const[r2],
00402 0, _work_cols);
00403 }
00404 static void Elim_Simple_Redundant(const INT32 min_var=0);
00405 BOOL Prove_Redundant(const INT set, const INT dim);
00406 BOOL Is_Consistent_Work();
00407
00408 MEM_POOL *Pool() const {return _pool;}
00409 void Print(FILE *fp) const;
00410 static void Print_Work(FILE *fp) ;
00411
00412 #ifdef KEY
00413
00414 BOOL SVPC_Applicable() { return SVPC() != SVPC_INAPPLICABLE; }
00415 INT32_INFIN Lower_Bound(INT col) { return _lower_bound[col]; }
00416 INT32_INFIN Upper_Bound(INT col) { return _upper_bound[col]; }
00417 mINT32 Work_Cols() { return _work_cols; }
00418 #endif
00419
00420 private:
00421
00422
00423
00424 INT32 ROW_INCR() const { return(32); }
00425
00426 SYSTEM_OF_EQUATIONS& operator = (const SYSTEM_OF_EQUATIONS&);
00427 SYSTEM_OF_EQUATIONS(const SYSTEM_OF_EQUATIONS&);
00428 SYSTEM_OF_EQUATIONS();
00429
00430 IMAT _Ale;
00431 IMAT _Aeq;
00432 mINT64* _ble;
00433 mINT64* _beq;
00434
00435 MEM_POOL* _pool;
00436 mINT32 _eqns_le;
00437 mINT32 _eqns_le_stored;
00438 mINT32 _eqns_eq;
00439 mINT32 _eqns_eq_stored;
00440 mINT32 _vars;
00441
00442
00443 #define SOE_MAX_WORK_ROWS 1000
00444 #define SOE_MAX_WORK_COLS 30
00445 static mINT32 _work[SOE_MAX_WORK_ROWS][SOE_MAX_WORK_COLS];
00446 static mINT64 _work_const[SOE_MAX_WORK_ROWS];
00447 static mINT32 _work_rows;
00448 static mINT32 _work_cols;
00449 static BOOL _is_redundant[SOE_MAX_WORK_ROWS];
00450 static BOOL _is_svpc[SOE_MAX_WORK_ROWS];
00451
00452
00453
00454 #define SOE_MAX_WORK_ROWS_EQ 100
00455 static mINT32 _work_eq[SOE_MAX_WORK_ROWS_EQ][SOE_MAX_WORK_COLS];
00456 static mINT64 _work_const_eq[SOE_MAX_WORK_ROWS_EQ];
00457 static mINT32 _work_rows_eq;
00458
00459
00460 static BOOL Elim_One(const INT32 i,const INT32 plus, const INT32 minus,
00461 BOOL *proved_inconsistent, const INT32 min_var);
00462 static INT32 Is_Simple_Redundant(const INT32* row1, const INT32* row2,
00463 INT64 row1c, INT64 row2c,
00464 INT min_var, INT cols);
00465 static INT32 Simple_Redundant(const INT32* row1, const INT32* row2,
00466 INT64 row1c, INT64 row2c,
00467 INT min_var, INT cols);
00468 BOOL Copy_To_Work(const INT32 from, const INT32 to);
00469 BOOL Copy_Inverse_To_Work(const INT32 i);
00470
00471
00472 static INT32_INFIN _lower_bound[SOE_MAX_WORK_COLS];
00473 static INT32_INFIN _upper_bound[SOE_MAX_WORK_COLS];
00474 BOOL One_Var_Consistent(INT32 var,INT32 from, INT32 to);
00475 void SVPC_Set_Bound(INT32 i, INT32 var);
00476 SVPC_RESULT SVPC();
00477 ACY_RESULT Acyclic_Test();
00478 INT Var_Leaf(INT i, INT *sign);
00479 void Acy_Set_Var(INT i, INT32_INFIN val, BOOL *inconsistent);
00480
00481
00482 BOOL Copy_To_Work_Eq();
00483 BOOL Sub_Last_Equal(BOOL *proved_inconsistent);
00484 BOOL Sub_Last_Equal_Unary(const INT32 i, const INT32 minvar);
00485 INT32 Normalize_Eq_and_Find_Smallest(INT32, INT32, BOOL *);
00486 INT32 Mod_Hat(INT32 a,INT32 b);
00487 BOOL Add_Work_Var();
00488
00489 void Gcd_Normalize();
00490 };
00491
00492 #endif
00493
00494
00495
