1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 2 3 /* 4 * Main authors: 5 * Guido Tack <guido.tack@monash.edu> 6 * Gleb Belov <gleb.belov@monash.edu> 7 */ 8 9 /* This Source Code Form is subject to the terms of the Mozilla Public 10 * License, v. 2.0. If a copy of the MPL was not distributed with this 11 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */ 12 13 #pragma once 14 15 #include <minizinc/astexception.hh> 16 #include <minizinc/builtins.hh> 17 #include <minizinc/file_utils.hh> 18 #include <minizinc/flatten.hh> 19 #include <minizinc/flatten_internal.hh> // temp., TODO 20 #include <minizinc/model.hh> 21 #include <minizinc/optimize.hh> 22 #include <minizinc/parser.hh> 23 #include <minizinc/solver_instance.hh> 24 #include <minizinc/typecheck.hh> 25 #include <minizinc/utils.hh> 26 27 #include <ctime> 28 #include <iomanip> 29 #include <memory> 30 #include <set> 31 #include <string> 32 #include <unordered_map> 33 #include <vector> 34 35 namespace MiniZinc { 36 37 /// Class handling fzn solver's output 38 /// could facilitate exhange of raw/final outputs in a portfolio 39 class Solns2Out { 40 protected: 41 std::unique_ptr<Env> _envGuard; 42 Env* _env = nullptr; 43 Model* _outputModel = nullptr; 44 45 typedef std::pair<VarDecl*, KeepAlive> DE; 46 ManagedASTStringMap<DE> _declmap; 47 Expression* _outputExpr = nullptr; 48 std::string _checkerModel; 49 std::string _statisticsCheckerModel; 50 bool _fNewSol2Print = false; // should be set for evalOutput to work 51 52 public: 53 std::string solution; 54 std::string comments; 55 int nLinesIgnore = 0; 56 57 struct Options { 58 std::string flagOutputFile; 59 bool flagOutputComments = true; 60 bool flagOutputFlush = true; 61 bool flagOutputTime = false; 62 int flagIgnoreLines = 0; 63 bool flagUnique = true; 64 bool flagCanonicalize = false; 65 bool flagStandaloneSolns2Out = false; 66 std::string flagOutputNoncanonical; 67 std::string flagOutputRaw; 68 int flagNumberOutput = -1; 69 /// Default values, also used for input 70 const char* const solutionSeparatorDef = "----------"; 71 const char* const unsatisfiableMsgDef = "=====UNSATISFIABLE====="; 72 const char* const unboundedMsgDef = "=====UNBOUNDED====="; 73 const char* const unsatorunbndMsgDef = "=====UNSATorUNBOUNDED====="; 74 const char* const unknownMsgDef = "=====UNKNOWN====="; 75 const char* const errorMsgDef = "=====ERROR====="; 76 const char* const searchCompleteMsgDef = "=========="; 77 /// Output values 78 std::string solutionSeparator = solutionSeparatorDef; 79 std::string solutionComma; 80 std::string unsatisfiableMsg = unsatisfiableMsgDef; 81 std::string unboundedMsg = unboundedMsgDef; 82 std::string unsatorunbndMsg = unsatorunbndMsgDef; 83 std::string unknownMsg = unknownMsgDef; 84 std::string errorMsg = errorMsgDef; 85 std::string searchCompleteMsg = searchCompleteMsgDef; 86 } opt; 87 88 struct Statistics { 89 unsigned long long nSolns = 0; 90 unsigned long long nFails = 0; 91 unsigned long long nNodes = 0; 92 } stats; 93 94 ~Solns2Out(); 95 Solns2Out(std::ostream& os, std::ostream& log, std::string stdlibDir); 96 97 bool processOption(int& i, std::vector<std::string>& argv, 98 const std::string& workingDir = std::string()); 99 static void printHelp(std::ostream& os); 100 101 /// The output model (~.ozn) can be passed in 1 way in this base class: 102 /// passing Env* containing output() 103 bool initFromEnv(Env* pE); 104 105 /// Then, variable assignments can be passed either as text 106 /// or put directly into envi()->output() ( latter done externally 107 /// by e.g. SolverInstance::assignSolutionToOutput() ) 108 /// In the 1st case, (part of) the assignment text is passed as follows, 109 /// original end-of-lines need to be there as well 110 bool feedRawDataChunk(const char* data); 111 112 SolverInstance::Status status = SolverInstance::UNKNOWN; 113 bool fStatusPrinted = false; 114 /// Should be called when entering new solution into the output model. 115 /// Default assignSolutionToOutput() does it by using findOutputVar(). 116 void declNewOutput(); 117 118 /// This can be used by assignSolutionToOutput() 119 DE& findOutputVar(const ASTString& name); 120 121 /// In the other case, 122 /// the evaluation procedures print output/status to os 123 /// returning false means need to stop (error/ too many solutions) 124 /// Solution validation here TODO 125 /// Note that --canonicalize delays output 126 /// until ... exit, eof, ?? TODO 127 /// These functions should only be called explicitly 128 /// from SolverInstance 129 bool evalOutput(const std::string& s_ExtraInfo = ""); 130 /// This means the solver exits 131 bool evalStatus(SolverInstance::Status status); 132 133 void printStatistics(std::ostream& os); 134 getEnv() const135 Env* getEnv() const { return _env; } getModel() const136 Model* getModel() const { 137 assert(getEnv()->output()); 138 return getEnv()->output(); 139 } 140 /// Get the primary output stream 141 /// First call restores stdout 142 std::ostream& getOutput(); 143 /// Get the secondary output stream 144 std::ostream& getLog(); 145 146 private: 147 Timer _starttime; 148 149 std::unique_ptr<std::ostream> _outStream; // file output 150 std::unique_ptr<std::ostream> _outStreamNonCanon; 151 std::unique_ptr<std::ostream> _outStreamRaw; 152 std::set<std::string> _sSolsCanon; 153 std::string _linePart; // non-finished line from last chunk 154 155 /// Initialise from ozn file 156 void initFromOzn(const std::string& filename); 157 158 protected: 159 std::ostream& _os; 160 std::ostream& _log; 161 std::vector<std::string> _includePaths; 162 std::string _stdlibDir; 163 164 // Basically open output 165 void init(); 166 std::map<std::string, SolverInstance::Status> _mapInputStatus; 167 void createInputMap(); 168 void restoreDefaults(); 169 /// Parsing fznsolver's complete raw text output 170 void parseAssignments(std::string& solution); 171 /// Checking solution against checker model 172 void checkSolution(std::ostream& os); 173 void checkStatistics(std::ostream& os); 174 bool evalOutputInternal(std::ostream& fout); 175 bool evalOutputFinalInternal(bool flag_flush); 176 bool evalStatusMsg(SolverInstance::Status status); 177 }; 178 179 // Passthrough Solns2Out class 180 class Solns2Log { 181 private: 182 std::ostream& _log; 183 std::ostream& _errLog; 184 185 public: Solns2Log(std::ostream & log,std::ostream & errLog)186 Solns2Log(std::ostream& log, std::ostream& errLog) : _log(log), _errLog(errLog) {} feedRawDataChunk(const char * data)187 bool feedRawDataChunk(const char* data) { 188 _log << data << std::flush; 189 return true; 190 } getLog()191 std::ostream& getLog() { return _errLog; } 192 }; 193 194 } // namespace MiniZinc 195