1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 2 3 /* 4 * Main authors: 5 * Guido Tack <guido.tack@monash.edu> 6 */ 7 8 /* This Source Code Form is subject to the terms of the Mozilla Public 9 * License, v. 2.0. If a copy of the MPL was not distributed with this 10 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */ 11 12 #pragma once 13 14 #include <minizinc/astexception.hh> 15 #include <minizinc/model.hh> 16 17 namespace MiniZinc { 18 19 /// Exception thrown for errors during flattening 20 class FlatteningError : public LocationException { 21 public: 22 FlatteningError(EnvI& env, const Location& loc, const std::string& msg); ~FlatteningError()23 ~FlatteningError() throw() override {} what() const24 const char* what() const throw() override { return "MiniZinc: flattening error"; } 25 }; 26 27 /// Options for the flattener 28 struct FlatteningOptions { 29 /// Keep output in resulting flat model 30 bool keepOutputInFzn; 31 /// Verbose output during flattening 32 bool verbose; 33 /// Only use paths for variables introduced by file 0 (the MiniZinc model) 34 bool onlyToplevelPaths; 35 /// Construct and collect mzn_paths for expressions and VarDeclI during flattening 36 bool collectMznPaths; 37 /// Do not apply domain changes but insert them as constraints (useful for debugging) 38 bool recordDomainChanges; 39 /// Only range domains for old linearization. Set from redefs to true if not here 40 bool onlyRangeDomains; 41 /// Allow the use of Half Reifications 42 bool enableHalfReification; 43 /// Timeout for flattening in milliseconds (0 means no timeout) 44 unsigned long long int timeout; 45 /// Create standard, DZN or JSON output 46 enum OutputMode { OUTPUT_ITEM, OUTPUT_DZN, OUTPUT_JSON, OUTPUT_CHECKER } outputMode; 47 /// Output objective value (only for DZN and JSON mode) 48 bool outputObjective; 49 /// Output original output item as string (only for DZN and JSON mode) 50 bool outputOutputItem; 51 /// Model is being compiled with a solution checker 52 bool hasChecker; 53 /// Output detailed timing information for flattening 54 bool detailedTiming; 55 /// Default constructor FlatteningOptionsMiniZinc::FlatteningOptions56 FlatteningOptions() 57 : keepOutputInFzn(false), 58 verbose(false), 59 onlyToplevelPaths(false), 60 collectMznPaths(false), 61 recordDomainChanges(false), 62 onlyRangeDomains(false), 63 enableHalfReification(true), 64 timeout(0), 65 outputMode(OUTPUT_ITEM), 66 outputObjective(false), 67 outputOutputItem(false), 68 detailedTiming(false) {} 69 }; 70 71 class Pass { 72 public: Pass()73 Pass(){}; 74 virtual Env* run(Env* env, std::ostream& log) = 0; ~Pass()75 virtual ~Pass(){}; 76 }; 77 78 /// Flatten model in environment \a e 79 void flatten(Env& e, FlatteningOptions opt = FlatteningOptions()); 80 81 /// Translate model in environment \a e into old FlatZinc syntax 82 void oldflatzinc(Env& e); 83 84 /// Populate FlatZinc output model 85 void populate_output(Env& e); 86 87 /// Statistics on flat models 88 struct FlatModelStatistics { 89 /// Number of integer variables 90 int n_int_vars; // NOLINT(readability-identifier-naming) 91 /// Number of bool variables 92 int n_bool_vars; // NOLINT(readability-identifier-naming) 93 /// Number of float variables 94 int n_float_vars; // NOLINT(readability-identifier-naming) 95 /// Number of set variables 96 int n_set_vars; // NOLINT(readability-identifier-naming) 97 /// Number of bool constraints 98 int n_bool_ct; // NOLINT(readability-identifier-naming) 99 /// Number of integer constraints 100 int n_int_ct; // NOLINT(readability-identifier-naming) 101 /// Number of float constraints 102 int n_float_ct; // NOLINT(readability-identifier-naming) 103 /// Number of set constraints 104 int n_set_ct; // NOLINT(readability-identifier-naming) 105 /// Number of reified constraints evaluated 106 int n_reif_ct; // NOLINT(readability-identifier-naming) 107 /// Number of half-reified constraints evaluated 108 int n_imp_ct; // NOLINT(readability-identifier-naming) 109 /// Number of implications eliminated using path compression 110 int n_imp_del; // NOLINT(readability-identifier-naming) 111 /// Number of linear expressions eliminated using path compression 112 int n_lin_del; // NOLINT(readability-identifier-naming) 113 /// Constructor FlatModelStatisticsMiniZinc::FlatModelStatistics114 FlatModelStatistics() 115 : n_int_vars(0), 116 n_bool_vars(0), 117 n_float_vars(0), 118 n_set_vars(0), 119 n_bool_ct(0), 120 n_int_ct(0), 121 n_float_ct(0), 122 n_set_ct(0), 123 n_reif_ct(0), 124 n_imp_ct(0), 125 n_imp_del(0), 126 n_lin_del(0) {} 127 }; 128 129 /// Compute statistics for flat model in \a m 130 FlatModelStatistics statistics(Env& m); 131 132 } // namespace MiniZinc 133