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 1
00027
00028 #include "Grid.types.hh"
00029 #include "globals.defs.hh"
00030 #include "Variable.defs.hh"
00031 #include "Variables_Set.types.hh"
00032 #include "Linear_Expression.defs.hh"
00033 #include "Constraint.defs.hh"
00034 #include "Constraint_System.defs.hh"
00035 #include "Constraint_System.inlines.hh"
00036 #include "Congruence_System.defs.hh"
00037 #include "Congruence_System.inlines.hh"
00038 #include "Grid_Generator_System.defs.hh"
00039 #include "Grid_Generator_System.inlines.hh"
00040 #include "Grid_Generator.types.hh"
00041 #include "Poly_Con_Relation.defs.hh"
00042 #include "Poly_Gen_Relation.defs.hh"
00043 #include "Grid_Certificate.types.hh"
00044 #include "Box.types.hh"
00045 #include "Polyhedron.defs.hh"
00046 #include "Polyhedron.types.hh"
00047 #include "Polyhedron.inlines.hh"
00048 #include "BD_Shape.types.hh"
00049 #include "Octagonal_Shape.types.hh"
00050 #include <vector>
00051 #include <iosfwd>
00052
00053 namespace Parma_Polyhedra_Library {
00054
00055 namespace IO_Operators {
00056
00058
00066 std::ostream&
00067 operator<<(std::ostream& s, const Grid& gr);
00068
00069 }
00070
00079 bool operator==(const Grid& x, const Grid& y);
00080
00089 bool operator!=(const Grid& x, const Grid& y);
00090
00091 }
00092
00093
00095
00352 class Parma_Polyhedra_Library::Grid {
00353 public:
00355 typedef Coefficient coefficient_type;
00356
00358 static dimension_type max_space_dimension();
00359
00364 static bool can_recycle_congruence_systems();
00365
00370 static bool can_recycle_constraint_systems();
00371
00373
00384 explicit Grid(dimension_type num_dimensions = 0,
00385 Degenerate_Element kind = UNIVERSE);
00386
00388
00398 explicit Grid(const Congruence_System& cgs);
00399
00401
00416 Grid(Congruence_System& cgs, Recycle_Input dummy);
00417
00419
00432 explicit Grid(const Constraint_System& cs);
00433
00435
00453 Grid(Constraint_System& cs, Recycle_Input dummy);
00454
00456
00469 explicit Grid(const Grid_Generator_System& const_gs);
00470
00472
00489 Grid(Grid_Generator_System& gs, Recycle_Input dummy);
00490
00492
00507 template <typename Interval>
00508 explicit Grid(const Box<Interval>& box,
00509 Complexity_Class complexity = ANY_COMPLEXITY);
00510
00512
00527 template <typename U>
00528 explicit Grid(const BD_Shape<U>& bd,
00529 Complexity_Class complexity = ANY_COMPLEXITY);
00530
00532
00547 template <typename U>
00548 explicit Grid(const Octagonal_Shape<U>& os,
00549 Complexity_Class complexity = ANY_COMPLEXITY);
00550
00552
00619 template <typename Box>
00620 Grid(const Box& box, From_Covering_Box dummy);
00621
00640 explicit Grid(const Polyhedron& ph,
00641 Complexity_Class complexity = ANY_COMPLEXITY);
00642
00644
00647 Grid(const Grid& y,
00648 Complexity_Class complexity = ANY_COMPLEXITY);
00649
00654 Grid& operator=(const Grid& y);
00655
00657
00658
00660 dimension_type space_dimension() const;
00661
00666 dimension_type affine_dimension() const;
00667
00672 Constraint_System constraints() const;
00673
00678 Constraint_System minimized_constraints() const;
00679
00681 const Congruence_System& congruences() const;
00682
00684 const Congruence_System& minimized_congruences() const;
00685
00687 const Grid_Generator_System& grid_generators() const;
00688
00690 const Grid_Generator_System& minimized_grid_generators() const;
00691
00693
00694
00695
00696
00697
00698
00699
00700 Poly_Con_Relation relation_with(const Congruence& cg) const;
00701
00703
00704
00705
00706
00707
00708 Poly_Gen_Relation
00709 relation_with(const Grid_Generator& g) const;
00710
00712
00713
00714
00715
00716
00717 Poly_Gen_Relation
00718 relation_with(const Generator& g) const;
00719
00721
00722
00723
00724
00725
00726
00727
00728 Poly_Con_Relation relation_with(const Constraint& c) const;
00729
00731 bool is_empty() const;
00732
00734 bool is_universe() const;
00735
00742 bool is_topologically_closed() const;
00743
00751 bool is_disjoint_from(const Grid& y) const;
00752
00754
00759 bool is_discrete() const;
00760
00762 bool is_bounded() const;
00763
00768 bool contains_integer_point() const;
00769
00777 bool constrains(Variable var) const;
00778
00780
00786 bool bounds_from_above(const Linear_Expression& expr) const;
00787
00789
00795 bool bounds_from_below(const Linear_Expression& expr) const;
00796
00824 bool maximize(const Linear_Expression& expr,
00825 Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const;
00826
00858 bool maximize(const Linear_Expression& expr,
00859 Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
00860 Generator& point) const;
00861
00889 bool minimize(const Linear_Expression& expr,
00890 Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const;
00891
00923 bool minimize(const Linear_Expression& expr,
00924 Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
00925 Generator& point) const;
00926
00928
00932 bool contains(const Grid& y) const;
00933
00941 bool strictly_contains(const Grid& y) const;
00942
00944
00970 template <typename Interval>
00971 void get_covering_box(Box<Interval>& box) const;
00972
00974
00990 bool OK(bool check_not_empty = false) const;
00991
00993
00995
00996
00998
01003 void add_congruence(const Congruence& cg);
01004
01018 bool add_congruence_and_minimize(const Congruence& c);
01019
01028 void add_grid_generator(const Grid_Generator& g);
01029
01044 bool add_grid_generator_and_minimize(const Grid_Generator& g);
01045
01047
01055 void add_congruences(const Congruence_System& cgs);
01056
01058
01070 void add_recycled_congruences(Congruence_System& cgs);
01071
01089 bool add_congruences_and_minimize(const Congruence_System& cgs);
01090
01112 bool add_recycled_congruences_and_minimize(Congruence_System& cgs);
01113
01115
01123 void add_constraint(const Constraint& c);
01124
01141 bool add_constraint_and_minimize(const Constraint& c);
01142
01154 void add_constraints(const Constraint_System& cs);
01155
01172 bool add_constraints_and_minimize(const Constraint_System& cs);
01173
01190 void add_recycled_constraints(Constraint_System& cs);
01191
01213 bool add_recycled_constraints_and_minimize(Constraint_System& cs);
01214
01216
01223 void refine_with_congruence(const Congruence& cg);
01224
01226
01233 void refine_with_congruences(const Congruence_System& cgs);
01234
01236
01244 void refine_with_constraint(const Constraint& c);
01245
01247
01254 void refine_with_constraints(const Constraint_System& cs);
01255
01269 void add_grid_generators(const Grid_Generator_System& gs);
01270
01286 void add_recycled_grid_generators(Grid_Generator_System& gs);
01287
01307 bool add_grid_generators_and_minimize(const Grid_Generator_System& gs);
01308
01330 bool add_recycled_grid_generators_and_minimize(Grid_Generator_System& gs);
01331
01342 void unconstrain(Variable var);
01343
01356 void unconstrain(const Variables_Set& to_be_unconstrained);
01357
01364 void intersection_assign(const Grid& y);
01365
01379 bool intersection_assign_and_minimize(const Grid& y);
01380
01387 void upper_bound_assign(const Grid& y);
01388
01402 bool upper_bound_assign_and_minimize(const Grid& y);
01403
01412 bool upper_bound_assign_if_exact(const Grid& y);
01413
01424 void difference_assign(const Grid& y);
01425
01435 bool simplify_using_context_assign(const Grid& y);
01436
01498 void affine_image(Variable var,
01499 const Linear_Expression& expr,
01500 Coefficient_traits::const_reference denominator
01501 = Coefficient_one());
01502
01562 void affine_preimage(Variable var,
01563 const Linear_Expression& expr,
01564 Coefficient_traits::const_reference denominator
01565 = Coefficient_one());
01566
01597 void
01598 generalized_affine_image(Variable var,
01599 Relation_Symbol relsym,
01600 const Linear_Expression& expr,
01601 Coefficient_traits::const_reference denominator
01602 = Coefficient_one(),
01603 Coefficient_traits::const_reference modulus
01604 = Coefficient_zero());
01605
01636 void
01637 generalized_affine_preimage(Variable var,
01638 Relation_Symbol relsym,
01639 const Linear_Expression& expr,
01640 Coefficient_traits::const_reference denominator
01641 = Coefficient_one(),
01642 Coefficient_traits::const_reference modulus
01643 = Coefficient_zero());
01644
01669 void
01670 generalized_affine_image(const Linear_Expression& lhs,
01671 Relation_Symbol relsym,
01672 const Linear_Expression& rhs,
01673 Coefficient_traits::const_reference modulus
01674 = Coefficient_zero());
01675
01700 void
01701 generalized_affine_preimage(const Linear_Expression& lhs,
01702 Relation_Symbol relsym,
01703 const Linear_Expression& rhs,
01704 Coefficient_traits::const_reference modulus
01705 = Coefficient_zero());
01706
01733 void bounded_affine_image(Variable var,
01734 const Linear_Expression& lb_expr,
01735 const Linear_Expression& ub_expr,
01736 Coefficient_traits::const_reference denominator
01737 = Coefficient_one());
01738
01765 void bounded_affine_preimage(Variable var,
01766 const Linear_Expression& lb_expr,
01767 const Linear_Expression& ub_expr,
01768 Coefficient_traits::const_reference denominator
01769 = Coefficient_one());
01770
01778 void time_elapse_assign(const Grid& y);
01779
01781 void topological_closure_assign();
01782
01798 void congruence_widening_assign(const Grid& y, unsigned* tp = NULL);
01799
01815 void generator_widening_assign(const Grid& y, unsigned* tp = NULL);
01816
01836 void widening_assign(const Grid& y, unsigned* tp = NULL);
01837
01858 void limited_congruence_extrapolation_assign(const Grid& y,
01859 const Congruence_System& cgs,
01860 unsigned* tp = NULL);
01861
01882 void limited_generator_extrapolation_assign(const Grid& y,
01883 const Congruence_System& cgs,
01884 unsigned* tp = NULL);
01885
01905 void limited_extrapolation_assign(const Grid& y,
01906 const Congruence_System& cgs,
01907 unsigned* tp = NULL);
01908
01910
01912
01913
01939 void add_space_dimensions_and_embed(dimension_type m);
01940
01966 void add_space_dimensions_and_project(dimension_type m);
01967
01976 void concatenate_assign(const Grid& y);
01977
01979
01988 void remove_space_dimensions(const Variables_Set& to_be_removed);
01989
01998 void remove_higher_space_dimensions(dimension_type new_dimension);
01999
02047 template <typename Partial_Function>
02048 void map_space_dimensions(const Partial_Function& pfunc);
02049
02051
02072 void expand_space_dimension(Variable var, dimension_type m);
02073
02075
02097 void fold_space_dimensions(const Variables_Set& to_be_folded, Variable var);
02098
02100
02101 friend bool operator==(const Grid& x, const Grid& y);
02102
02103 friend class Parma_Polyhedra_Library::Grid_Certificate;
02104
02105 template <typename Interval> friend class Parma_Polyhedra_Library::Box;
02106
02108
02109
02111 ~Grid();
02112
02117 void swap(Grid& y);
02118
02119 PPL_OUTPUT_DECLARATIONS
02120
02121 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
02122
02127 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
02128 bool ascii_load(std::istream& s);
02129
02131 memory_size_type total_memory_in_bytes() const;
02132
02134 memory_size_type external_memory_in_bytes() const;
02135
02142 int32_t hash_code() const;
02143
02145
02146 private:
02147
02149 Congruence_System con_sys;
02150
02152 Grid_Generator_System gen_sys;
02153
02154 #define PPL_IN_Grid_CLASS
02155 #include "Grid_Status.idefs.hh"
02156 #undef PPL_IN_Grid_CLASS
02157
02159 Status status;
02160
02162 dimension_type space_dim;
02163
02164 enum Dimension_Kind {
02165 PARAMETER,
02166 LINE,
02167 GEN_VIRTUAL,
02168 PROPER_CONGRUENCE = PARAMETER,
02169 CON_VIRTUAL = LINE,
02170 EQUALITY = GEN_VIRTUAL
02171 };
02172
02173 typedef std::vector<Dimension_Kind> Dimension_Kinds;
02174
02175
02176
02177
02178
02179
02180
02181 Dimension_Kinds dim_kinds;
02182
02184
02191 void construct(dimension_type num_dimensions, Degenerate_Element kind);
02192
02194
02201 void construct(Congruence_System& cgs);
02202
02204
02211 void construct(Grid_Generator_System& ggs);
02212
02214
02215
02217
02221 bool marked_empty() const;
02222
02224 bool congruences_are_up_to_date() const;
02225
02227 bool generators_are_up_to_date() const;
02228
02230 bool congruences_are_minimized() const;
02231
02233 bool generators_are_minimized() const;
02234
02236
02238
02239
02244 void set_zero_dim_univ();
02245
02250 void set_empty();
02251
02253 void set_congruences_up_to_date();
02254
02256 void set_generators_up_to_date();
02257
02259 void set_congruences_minimized();
02260
02262 void set_generators_minimized();
02263
02265
02267
02268
02270 void clear_empty();
02271
02273 void clear_congruences_up_to_date();
02274
02276 void clear_generators_up_to_date();
02277
02279 void clear_congruences_minimized();
02280
02282 void clear_generators_minimized();
02283
02285
02287
02288
02290 void update_congruences() const;
02291
02293
02301 bool update_generators() const;
02302
02304
02306
02307
02309
02317 bool minimize() const;
02318
02320
02321 enum Three_Valued_Boolean {
02322 TVB_TRUE,
02323 TVB_FALSE,
02324 TVB_DONT_KNOW
02325 };
02326
02328 Three_Valued_Boolean quick_equivalence_test(const Grid& y) const;
02329
02331 bool is_included_in(const Grid& y) const;
02332
02334
02351 bool bounds(const Linear_Expression& expr, const char* method_call) const;
02352
02354
02385 bool max_min(const Linear_Expression& expr,
02386 const char* method_call,
02387 Coefficient& ext_n, Coefficient& ext_d, bool& included,
02388 Generator* point = NULL) const;
02389
02397 void add_congruence_no_check(const Congruence& cg);
02398
02412 void add_constraint_no_check(const Constraint& c);
02413
02425 void refine_no_check(const Constraint& c);
02426
02428
02429
02431 void select_wider_congruences(const Grid& y,
02432 Congruence_System& selected_cgs) const;
02433
02435 void select_wider_generators(const Grid& y,
02436 Grid_Generator_System& widened_ggs) const;
02437
02439
02441
02454 void add_space_dimensions(Congruence_System& cgs,
02455 Grid_Generator_System& gs,
02456 dimension_type dims);
02457
02459
02472 void add_space_dimensions(Grid_Generator_System& gs,
02473 Congruence_System& cgs,
02474 dimension_type dims);
02475
02477
02478
02480
02497 static void
02498 normalize_divisors(Grid_Generator_System& sys,
02499 Coefficient& divisor,
02500 const Grid_Generator* first_point = NULL);
02501
02503
02511 static void
02512 normalize_divisors(Grid_Generator_System& sys);
02513
02515
02531 static void normalize_divisors(Grid_Generator_System& sys,
02532 Grid_Generator_System& gen_sys);
02533
02538 static void conversion(Congruence_System& source,
02539 Grid_Generator_System& dest,
02540 Dimension_Kinds& dim_kinds);
02541
02546 static void conversion(Grid_Generator_System& source,
02547 Congruence_System& dest,
02548 Dimension_Kinds& dim_kinds);
02549
02551
02555 static bool simplify(Congruence_System& cgs,
02556 Dimension_Kinds& dim_kinds);
02557
02559
02562 static void simplify(Grid_Generator_System& gs,
02563 Dimension_Kinds& dim_kinds);
02564
02566
02570
02571 static void reduce_line_with_line(Grid_Generator& row,
02572 Grid_Generator& pivot,
02573 dimension_type col);
02574
02576
02581
02582 static void reduce_equality_with_equality(Congruence& row,
02583 const Congruence& pivot,
02584 dimension_type col);
02585
02587
02594
02595 template <typename R>
02596 static void reduce_pc_with_pc(R& row,
02597 R& pivot,
02598 dimension_type col,
02599 dimension_type start,
02600 dimension_type end);
02601
02603
02608
02609 static void reduce_parameter_with_line(Grid_Generator& row,
02610 const Grid_Generator& pivot,
02611 dimension_type col,
02612 Grid_Generator_System& sys);
02613
02615
02620
02621 static void reduce_congruence_with_equality(Congruence& row,
02622 const Congruence& pivot,
02623 dimension_type col,
02624 Congruence_System& sys);
02625
02626 #ifdef STRONG_REDUCTION
02628
02633 template <typename M, typename R>
02634 static void reduce_reduced(M& sys, dimension_type dim,
02635 dimension_type pivot_index,
02636 dimension_type start, dimension_type end,
02637 const Dimension_Kinds& dim_kinds,
02638 bool generators = true);
02639 #endif
02640
02642
02643 static void multiply_grid(const Coefficient& multiplier,
02644 Congruence& cg, Congruence_System& dest,
02645 dimension_type num_rows,
02646 dimension_type num_dims);
02647
02649
02650 static void multiply_grid(const Coefficient& multiplier,
02651 Grid_Generator& gen,
02652 Grid_Generator_System& dest,
02653 dimension_type num_rows,
02654 dimension_type num_dims);
02655
02660 static bool lower_triangular(const Congruence_System& sys,
02661 const Dimension_Kinds& dim_kinds);
02662
02667 static bool upper_triangular(const Grid_Generator_System& sys,
02668 const Dimension_Kinds& dim_kinds);
02669
02670 #ifndef NDEBUG
02672
02680 template <typename M, typename R>
02681 static bool rows_are_zero(M& system,
02682 dimension_type first,
02683 dimension_type last,
02684 dimension_type row_size);
02685 #endif
02686
02688
02690
02691 protected:
02692 void throw_runtime_error(const char* method) const;
02693 void throw_invalid_argument(const char* method, const char* reason) const;
02694
02695 void throw_dimension_incompatible(const char* method,
02696 const char* other_name,
02697 dimension_type other_dim) const;
02698 void throw_dimension_incompatible(const char* method,
02699 const char* gr_name,
02700 const Grid& gr) const;
02701 void throw_dimension_incompatible(const char* method,
02702 const char* e_name,
02703 const Linear_Expression& e) const;
02704 void throw_dimension_incompatible(const char* method,
02705 const char* cg_name,
02706 const Congruence& cg) const;
02707 void throw_dimension_incompatible(const char* method,
02708 const char* c_name,
02709 const Constraint& c) const;
02710 void throw_dimension_incompatible(const char* method,
02711 const char* g_name,
02712 const Grid_Generator& g) const;
02713 void throw_dimension_incompatible(const char* method,
02714 const char* g_name,
02715 const Generator& g) const;
02716 void throw_dimension_incompatible(const char* method,
02717 const char* cgs_name,
02718 const Congruence_System& cgs) const;
02719 void throw_dimension_incompatible(const char* method,
02720 const char* cs_name,
02721 const Constraint_System& cs) const;
02722 void throw_dimension_incompatible(const char* method,
02723 const char* gs_name,
02724 const Grid_Generator_System& gs) const;
02725 void throw_dimension_incompatible(const char* method,
02726 const char* var_name,
02727 Variable var) const;
02728 void throw_dimension_incompatible(const char* method,
02729 dimension_type required_space_dim) const;
02730
02731
02732
02733 static void throw_space_dimension_overflow(const char* method,
02734 const char* reason);
02735
02736 void throw_invalid_constraint(const char* method,
02737 const char* c_name) const;
02738 void throw_invalid_constraints(const char* method,
02739 const char* cs_name) const;
02740 void throw_invalid_generator(const char* method,
02741 const char* g_name) const;
02742 void throw_invalid_generators(const char* method,
02743 const char* gs_name) const;
02745
02746 };
02747
02748
02749 namespace std {
02750
02752
02753 void swap(Parma_Polyhedra_Library::Grid& x,
02754 Parma_Polyhedra_Library::Grid& y);
02755
02756 }
02757
02758 #include "Grid_Status.inlines.hh"
02759 #include "Grid.inlines.hh"
02760 #include "Grid.templates.hh"
02761
02762 #endif // !defined(PPL_Grid_defs_hh)