00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #ifndef PPL_Grid_defs_hh
00024 #define PPL_Grid_defs_hh 1
00025
00026 #define STRONG_REDUCTION
00027
00028 #include "Grid.types.hh"
00029 #include "globals.defs.hh"
00030 #include "Variable.defs.hh"
00031 #include "Linear_Expression.defs.hh"
00032 #include "Constraint.defs.hh"
00033 #include "Constraint_System.defs.hh"
00034 #include "Constraint_System.inlines.hh"
00035 #include "Congruence_System.defs.hh"
00036 #include "Congruence_System.inlines.hh"
00037 #include "Grid_Generator_System.defs.hh"
00038 #include "Grid_Generator_System.inlines.hh"
00039 #include "Grid_Generator.types.hh"
00040 #include "Poly_Con_Relation.defs.hh"
00041 #include "Poly_Gen_Relation.defs.hh"
00042 #include "Grid_Certificate.types.hh"
00043 #include <vector>
00044 #include <iosfwd>
00045
00046
00047 #define print_dim_kinds(msg, dim_kinds) \
00048 std::cout << msg << "dim_kinds:"; \
00049 for (Dimension_Kinds::iterator i = dim_kinds.begin(); i != dim_kinds.end(); ++i) \
00050 std::cout << " " << *i; \
00051 std::cout << std::endl;
00052 #if 0
00053 #define trace_dim_kinds(msg, dim_kinds) print_dim_kinds(msg, dim_kinds)
00054 #else
00055 #define trace_dim_kinds(msg, dim_kinds)
00056 #endif
00057
00058 namespace Parma_Polyhedra_Library {
00059
00060 namespace IO_Operators {
00061
00063
00071 std::ostream&
00072 operator<<(std::ostream& s, const Grid& gr);
00073
00074 }
00075
00084 bool operator==(const Grid& x, const Grid& y);
00085
00094 bool operator!=(const Grid& x, const Grid& y);
00095
00096 }
00097
00098
00100
00362 class Parma_Polyhedra_Library::Grid {
00363 public:
00365 static dimension_type max_space_dimension();
00366
00368
00379 explicit Grid(dimension_type num_dimensions = 0,
00380 const Degenerate_Element kind = UNIVERSE);
00381
00383
00393 explicit Grid(const Congruence_System& cgs);
00394
00396
00407 explicit Grid(Congruence_System& cgs);
00408
00410
00420 explicit Grid(const Constraint_System& cs);
00421
00423
00433 explicit Grid(Constraint_System& cs);
00434
00436
00449 explicit Grid(const Grid_Generator_System& const_gs);
00450
00452
00465 explicit Grid(Grid_Generator_System& gs);
00466
00468
00526 template <typename Box>
00527 Grid(const Box& box, From_Bounding_Box dummy);
00528
00530
00597 template <typename Box>
00598 Grid(const Box& box, From_Covering_Box dummy);
00599
00601 Grid(const Grid& y);
00602
00607 Grid& operator=(const Grid& y);
00608
00610
00611
00613 dimension_type space_dimension() const;
00614
00619 dimension_type affine_dimension() const;
00620
00622 const Congruence_System& congruences() const;
00623
00625 const Congruence_System& minimized_congruences() const;
00626
00628 const Grid_Generator_System& generators() const;
00629
00631 const Grid_Generator_System& minimized_generators() const;
00632
00634
00635
00636
00637
00638
00639
00640
00641 Poly_Con_Relation relation_with(const Congruence& cg) const;
00642
00644
00645
00646
00647
00648
00649 Poly_Gen_Relation
00650 relation_with(const Grid_Generator& g) const;
00651
00656 bool is_empty() const;
00657
00662 bool is_universe() const;
00663
00668 bool is_topologically_closed() const;
00669
00677 bool is_disjoint_from(const Grid& y) const;
00678
00680
00685 bool is_discrete() const;
00686
00688 bool is_bounded() const;
00689
00691
00697 bool bounds_from_above(const Linear_Expression& expr) const;
00698
00700
00706 bool bounds_from_below(const Linear_Expression& expr) const;
00707
00735 bool maximize(const Linear_Expression& expr,
00736 Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const;
00737
00769 bool maximize(const Linear_Expression& expr,
00770 Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
00771 Grid_Generator& point) const;
00772
00800 bool minimize(const Linear_Expression& expr,
00801 Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const;
00802
00834 bool minimize(const Linear_Expression& expr,
00835 Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
00836 Grid_Generator& point) const;
00837
00839
00843 bool contains(const Grid& y) const;
00844
00852 bool strictly_contains(const Grid& y) const;
00853
00855
00927 template <typename Box>
00928 void shrink_bounding_box(Box& box) const;
00929
00931
00996 template <typename Box>
00997 void get_covering_box(Box& box) const;
00998
01000
01016 bool OK(bool check_not_empty = false) const;
01017
01019
01021
01022
01024
01029 void add_congruence(const Congruence& cg);
01030
01032
01038 void add_congruence(const Constraint& c);
01039
01050 bool add_congruence_and_minimize(const Congruence& c);
01051
01053
01062 bool add_congruence_and_minimize(const Constraint& c);
01063
01072 void add_generator(const Grid_Generator& g);
01073
01085 bool add_generator_and_minimize(const Grid_Generator& g);
01086
01088
01096 void add_congruences(const Congruence_System& cgs);
01097
01099
01107 void add_congruences(const Constraint_System& cs);
01108
01110
01122 void add_recycled_congruences(Congruence_System& cgs);
01123
01125
01138 void add_recycled_congruences(Constraint_System& cs);
01139
01154 bool add_congruences_and_minimize(const Congruence_System& cgs);
01155
01170 bool add_congruences_and_minimize(const Constraint_System& cs);
01171
01190 bool add_recycled_congruences_and_minimize(Congruence_System& cgs);
01191
01193
01208 bool add_recycled_congruences_and_minimize(Constraint_System& cs);
01209
01211
01217 void add_constraint(const Constraint& c);
01218
01220
01229 bool add_constraint_and_minimize(const Constraint& c);
01230
01232
01236 void add_constraints(const Constraint_System& cs);
01237
01248 bool add_constraints_and_minimize(const Constraint_System& cs);
01249
01251
01259 void add_recycled_constraints(Constraint_System& cs);
01260
01273 bool add_recycled_constraints_and_minimize(Constraint_System& cs);
01274
01288 void add_generators(const Grid_Generator_System& gs);
01289
01307 void add_recycled_generators(Grid_Generator_System& gs);
01308
01325 bool add_generators_and_minimize(const Grid_Generator_System& gs);
01326
01347 bool add_recycled_generators_and_minimize(Grid_Generator_System& gs);
01348
01356 void intersection_assign(const Grid& y);
01357
01368 bool intersection_assign_and_minimize(const Grid& y);
01369
01376 void join_assign(const Grid& y);
01377
01388 bool join_assign_and_minimize(const Grid& y);
01389
01391 void upper_bound_assign(const Grid& y);
01392
01401 bool join_assign_if_exact(const Grid& y);
01402
01404 bool upper_bound_assign_if_exact(const Grid& y);
01405
01416 void grid_difference_assign(const Grid& y);
01417
01419 void difference_assign(const Grid& y);
01420
01482 void affine_image(Variable var,
01483 const Linear_Expression& expr,
01484 Coefficient_traits::const_reference denominator
01485 = Coefficient_one());
01486
01546 void affine_preimage(Variable var,
01547 const Linear_Expression& expr,
01548 Coefficient_traits::const_reference denominator
01549 = Coefficient_one());
01550
01577 void generalized_affine_image(Variable var,
01578 const Linear_Expression& expr,
01579 Coefficient_traits::const_reference denominator
01580 = Coefficient_one(),
01581 Coefficient_traits::const_reference modulus
01582 = Coefficient_one());
01583
01610 void generalized_affine_preimage(Variable var,
01611 const Linear_Expression& expr,
01612 Coefficient_traits::const_reference denominator
01613 = Coefficient_one(),
01614 Coefficient_traits::const_reference modulus
01615 = Coefficient_one());
01616
01637 void generalized_affine_image(const Linear_Expression& lhs,
01638 const Linear_Expression& rhs,
01639 Coefficient_traits::const_reference modulus
01640 = Coefficient_one());
01641
01662 void generalized_affine_preimage(const Linear_Expression& lhs,
01663 const Linear_Expression& rhs,
01664 Coefficient_traits::const_reference modulus
01665 = Coefficient_one());
01666
01674 void time_elapse_assign(const Grid& y);
01675
01677 void topological_closure_assign();
01678
01694 void widening_assign(const Grid& y, unsigned* tp = NULL);
01695
01715 void limited_extrapolation_assign(const Grid& y,
01716 const Congruence_System& cgs,
01717 unsigned* tp = NULL);
01718
01720
01722
01723
01749 void add_space_dimensions_and_embed(dimension_type m);
01750
01776 void add_space_dimensions_and_project(dimension_type m);
01777
01786 void concatenate_assign(const Grid& y);
01787
01789
01798 void remove_space_dimensions(const Variables_Set& to_be_removed);
01799
01808 void remove_higher_space_dimensions(dimension_type new_dimension);
01809
01857 template <typename Partial_Function>
01858 void map_space_dimensions(const Partial_Function& pfunc);
01859
01861
01882 void expand_space_dimension(Variable var, dimension_type m);
01883
01885
01907 void fold_space_dimensions(const Variables_Set& to_be_folded, Variable var);
01908
01910
01911 friend bool Parma_Polyhedra_Library::operator==(const Grid& x,
01912 const Grid& y);
01913
01914 friend class Parma_Polyhedra_Library::Grid_Certificate;
01915
01917
01918
01920 ~Grid();
01921
01926 void swap(Grid& y);
01927
01928 PPL_OUTPUT_DECLARATIONS;
01929
01930 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01931
01938 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
01939 bool ascii_load(std::istream& s);
01940
01942 memory_size_type total_memory_in_bytes() const;
01943
01945 memory_size_type external_memory_in_bytes() const;
01946
01948
01949 private:
01950
01952 Congruence_System con_sys;
01953
01955 Grid_Generator_System gen_sys;
01956
01957 #define PPL_IN_Grid_CLASS
01958 #include "Grid_Status.idefs.hh"
01959 #undef PPL_IN_Grid_CLASS
01960
01962 Status status;
01963
01965 dimension_type space_dim;
01966
01967 enum Dimension_Kind {
01968 PARAMETER,
01969 LINE,
01970 GEN_VIRTUAL,
01971 PROPER_CONGRUENCE = PARAMETER,
01972 CON_VIRTUAL = LINE,
01973 EQUALITY = GEN_VIRTUAL
01974 };
01975
01976 typedef std::vector<Dimension_Kind> Dimension_Kinds;
01977
01978
01979
01980
01981
01982
01983
01984 Dimension_Kinds dim_kinds;
01985
01987
01993 void construct(const Congruence_System& cgs);
01994
01996
02002 void construct(const Grid_Generator_System& gs);
02003
02005
02006
02008
02012 bool marked_empty() const;
02013
02015 bool congruences_are_up_to_date() const;
02016
02018 bool generators_are_up_to_date() const;
02019
02021 bool congruences_are_minimized() const;
02022
02024 bool generators_are_minimized() const;
02025
02027
02029
02030
02035 void set_zero_dim_univ();
02036
02041 void set_empty();
02042
02044 void set_congruences_up_to_date();
02045
02047 void set_generators_up_to_date();
02048
02050 void set_congruences_minimized();
02051
02053 void set_generators_minimized();
02054
02056
02058
02059
02061 void clear_empty();
02062
02064 void clear_congruences_up_to_date();
02065
02067 void clear_generators_up_to_date();
02068
02070 void clear_congruences_minimized();
02071
02073 void clear_generators_minimized();
02074
02076
02078
02079
02081
02085 bool update_congruences() const;
02086
02088
02096 bool update_generators() const;
02097
02099
02101
02102
02104
02112 bool minimize() const;
02113
02115
02116 enum Three_Valued_Boolean {
02117 TVB_TRUE,
02118 TVB_FALSE,
02119 TVB_DONT_KNOW
02120 };
02121
02123 Three_Valued_Boolean quick_equivalence_test(const Grid& y) const;
02124
02126 bool is_included_in(const Grid& y) const;
02127
02129
02146 bool bounds(const Linear_Expression& expr, const char* method_call) const;
02147
02149
02180 bool max_min(const Linear_Expression& expr,
02181 char* method_call,
02182 Coefficient& ext_n, Coefficient& ext_d, bool& included,
02183 Grid_Generator* point = NULL) const;
02184
02186
02187
02189 void select_wider_congruences(const Grid& y,
02190 Congruence_System& selected_cgs) const;
02191
02193
02195
02208 void add_space_dimensions(Congruence_System& cgs,
02209 Grid_Generator_System& gs,
02210 const dimension_type dims);
02211
02213
02226 void add_space_dimensions(Grid_Generator_System& gs,
02227 Congruence_System& cgs,
02228 const dimension_type dims);
02229
02231
02232
02234
02253 static Coefficient
02254 normalize_divisors(Grid_Generator_System& sys,
02255 Coefficient_traits::const_reference divisor
02256 = Coefficient_one(),
02257 Grid_Generator* first_point = NULL);
02258
02260
02265 static void normalize_divisors(Grid_Generator_System& sys,
02266 Grid_Generator_System& gen_sys);
02267
02272 static void conversion(Congruence_System& source,
02273 Grid_Generator_System& dest,
02274 Dimension_Kinds& dim_kinds);
02275
02280 static void conversion(Grid_Generator_System& source,
02281 Congruence_System& dest,
02282 Dimension_Kinds& dim_kinds);
02283
02285
02289 static bool simplify(Congruence_System& cgs,
02290 Dimension_Kinds& dim_kinds);
02291
02293
02296 static void simplify(Grid_Generator_System& gs,
02297 Dimension_Kinds& dim_kinds);
02298
02300
02304
02305 static void reduce_line_with_line(Grid_Generator& row,
02306 Grid_Generator& pivot,
02307 dimension_type col);
02308
02310
02315
02316 static void reduce_equality_with_equality(Congruence& row,
02317 Congruence& pivot,
02318 dimension_type col);
02319
02321
02328
02329 template <typename R>
02330 static void reduce_pc_with_pc(R& row,
02331 R& pivot,
02332 dimension_type col,
02333 dimension_type start,
02334 dimension_type end);
02335
02337
02342
02343 static void reduce_parameter_with_line(Grid_Generator& row,
02344 Grid_Generator& pivot,
02345 dimension_type col,
02346 Grid_Generator_System& sys);
02347
02349
02354
02355 static void reduce_congruence_with_equality(Congruence& row,
02356 Congruence& pivot,
02357 dimension_type col,
02358 Congruence_System& sys);
02359
02361
02366 template <typename M, typename R>
02367 static void reduce_reduced(M& sys, dimension_type dim,
02368 dimension_type pivot_index,
02369 dimension_type start, dimension_type end,
02370 Dimension_Kinds& dim_kinds,
02371 bool generators = true);
02372
02374
02375 static void multiply_grid(const Coefficient& multiplier,
02376 Congruence& cg, Congruence_System& dest,
02377 const dimension_type num_rows,
02378 const dimension_type num_dims);
02379
02381
02382 static void multiply_grid(const Coefficient& multiplier, Grid_Generator& gen,
02383 Grid_Generator_System& dest, const dimension_type num_rows,
02384 const dimension_type num_dims);
02385
02390 static bool lower_triangular(const Congruence_System& sys,
02391 const Dimension_Kinds& dim_kinds);
02392
02397 static bool upper_triangular(const Grid_Generator_System& sys,
02398 const Dimension_Kinds& dim_kinds);
02399
02400 #ifndef NDEBUG
02402
02410 template <typename M, typename R>
02411 static bool rows_are_zero(M& system,
02412 dimension_type first,
02413 dimension_type last,
02414 dimension_type row_size);
02415 #endif
02416
02418
02420
02421 protected:
02422 void throw_runtime_error(const char* method) const;
02423 void throw_invalid_argument(const char* method, const char* reason) const;
02424
02425 void throw_dimension_incompatible(const char* method,
02426 const char* other_name,
02427 dimension_type other_dim) const;
02428 void throw_dimension_incompatible(const char* method,
02429 const char* gr_name,
02430 const Grid& gr) const;
02431 void throw_dimension_incompatible(const char* method,
02432 const char* e_name,
02433 const Linear_Expression& e) const;
02434 void throw_dimension_incompatible(const char* method,
02435 const char* cg_name,
02436 const Congruence& cg) const;
02437 void throw_dimension_incompatible(const char* method,
02438 const char* c_name,
02439 const Constraint& c) const;
02440 void throw_dimension_incompatible(const char* method,
02441 const char* g_name,
02442 const Grid_Generator& g) const;
02443 void throw_dimension_incompatible(const char* method,
02444 const char* cgs_name,
02445 const Congruence_System& cgs) const;
02446 void throw_dimension_incompatible(const char* method,
02447 const char* cs_name,
02448 const Constraint_System& cs) const;
02449 void throw_dimension_incompatible(const char* method,
02450 const char* gs_name,
02451 const Grid_Generator_System& gs) const;
02452 void throw_dimension_incompatible(const char* method,
02453 const char* var_name,
02454 const Variable var) const;
02455 void throw_dimension_incompatible(const char* method,
02456 dimension_type required_space_dim) const;
02457
02458
02459
02460 static void throw_space_dimension_overflow(const char* method,
02461 const char* reason);
02462
02463 void throw_invalid_generator(const char* method,
02464 const char* g_name) const;
02465 void throw_invalid_generators(const char* method,
02466 const char* gs_name) const;
02468
02469 };
02470
02471
02472 namespace std {
02473
02475
02476 void swap(Parma_Polyhedra_Library::Grid& x,
02477 Parma_Polyhedra_Library::Grid& y);
02478
02479 }
02480
02481 #include "Grid_Status.inlines.hh"
02482 #include "Grid.inlines.hh"
02483 #include "Grid.templates.hh"
02484
02485 #endif // !defined(PPL_Grid_defs_hh)