A set of benchmarks to compare a new prototype MiniZinc implementation
dekker.one
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#ifndef __MINIZINC_SOLVER_HH__
13#define __MINIZINC_SOLVER_HH__
14
15#include <minizinc/exception.hh>
16#include <minizinc/flattener.hh>
17#include <minizinc/solver_config.hh>
18#include <minizinc/solver_instance_base.hh>
19
20#include <iostream>
21#include <memory>
22#include <string>
23#include <vector>
24
25namespace MiniZinc {
26
27class SolverInitialiser {
28public:
29 SolverInitialiser(void);
30};
31
32class SolverFactory;
33
34/// SolverRegistry is a storage for all SolverFactories in linked modules
35class SolverRegistry {
36public:
37 void addSolverFactory(SolverFactory*);
38 void removeSolverFactory(SolverFactory*);
39 typedef std::vector<SolverFactory*> SFStorage;
40 const SFStorage& getSolverFactories() const { return sfstorage; }
41
42private:
43 SFStorage sfstorage;
44}; // SolverRegistry
45
46/// this function returns the global SolverRegistry object
47SolverRegistry* getGlobalSolverRegistry();
48
49/// Representation of flags that can be passed to solvers
50class MZNFZNSolverFlag {
51public:
52 /// The type of the solver flag
53 enum FlagType { FT_ARG, FT_NOARG } t;
54 /// The name of the solver flag
55 std::string n;
56
57protected:
58 MZNFZNSolverFlag(const FlagType& t0, const std::string& n0) : t(t0), n(n0) {}
59
60public:
61 /// Create flag that has an argument
62 static MZNFZNSolverFlag arg(const std::string& n) { return MZNFZNSolverFlag(FT_ARG, n); }
63 /// Create flag that has no argument
64 static MZNFZNSolverFlag noarg(const std::string& n) { return MZNFZNSolverFlag(FT_NOARG, n); }
65 /// Create solver flag from standard flag
66 static MZNFZNSolverFlag std(const std::string& n);
67 /// Create solver flag from extra flag with name \a n and type \a t
68 static MZNFZNSolverFlag extra(const std::string& n, const std::string& t);
69};
70
71/// SolverFactory's descendants create, store and destroy SolverInstances
72/// A SolverFactory stores all Instances itself and upon module exit,
73/// destroys them and de-registers itself from the global SolverRegistry
74/// An instance of SolverFactory's descendant can be created directly
75/// or by one of the specialized createF_...() functions
76class SolverFactory {
77protected:
78 /// doCreateSI should be implemented to actually allocate a SolverInstance using new()
79 virtual SolverInstanceBase* doCreateSI(std::ostream&, SolverInstanceBase::Options* opt) = 0;
80 typedef std::vector<std::unique_ptr<SolverInstanceBase>> SIStorage;
81 SIStorage sistorage;
82
83protected:
84 SolverFactory() { getGlobalSolverRegistry()->addSolverFactory(this); }
85
86public:
87 virtual ~SolverFactory() { getGlobalSolverRegistry()->removeSolverFactory(this); }
88
89public:
90 /// Create solver-specific options object
91 virtual SolverInstanceBase::Options* createOptions(void) = 0;
92 /// Function createSI also adds each SI to the local storage
93 SolverInstanceBase* createSI(std::ostream& log, SolverInstanceBase::Options* opt);
94 /// also providing a manual destroy function.
95 /// there is no need to call it upon overall finish - that is taken care of
96 void destroySI(SolverInstanceBase* pSI);
97
98public:
99 /// Process an item in the command line.
100 /// Leaving this now like this because this seems simpler.
101 /// We can also pass options internally between modules in this way
102 /// and it only needs 1 format
103 virtual bool processOption(SolverInstanceBase::Options* opt, int& i,
104 std::vector<std::string>& argv) {
105 return false;
106 }
107
108 virtual std::string getDescription(SolverInstanceBase::Options* opt = NULL) = 0;
109 virtual std::string getVersion(SolverInstanceBase::Options* opt = NULL) = 0;
110 virtual std::string getId(void) = 0;
111 virtual void printHelp(std::ostream&) {}
112}; // SolverFactory
113
114// Class MznSolver coordinates flattening and solving.
115class MznSolver {
116private:
117 SolverInitialiser _solver_init;
118 enum OptionStatus { OPTION_OK, OPTION_ERROR, OPTION_FINISH };
119 /// Solver configurations
120 SolverConfigs solver_configs;
121 Constraint* output = nullptr;
122 std::vector<BytecodeProc> bs;
123 std::vector<std::string> data_files;
124 Env in_out_defs;
125 SolverInstanceBase* si = 0;
126 SolverInstanceBase::Options* si_opt = 0;
127 SolverFactory* sf = 0;
128 bool is_mzn2fzn = 0;
129
130 std::string executable_name;
131 std::string file;
132 std::string solver_str;
133 std::ostream& os;
134 std::ostream& log;
135 SolverInstance::Status interpreter_status = SolverInstance::UNKNOWN;
136 // Incremental interface
137 std::vector<std::pair<Variable*, size_t>> def_stack = {{nullptr, 0}};
138 double flatten_time = 0;
139
140public:
141 bool output_dict = false;
142 Interpreter* interpreter = nullptr;
143 Solns2Out s2out;
144 // name -> <code, nargs>
145 std::unordered_map<std::string, std::pair<int, int>> resolve_call;
146
147 /// global options
148 bool flag_verbose = false;
149 bool flag_statistics = false;
150 bool flag_compiler_verbose = false;
151 bool flag_compiler_statistics = false;
152 bool flag_is_solns2out = false;
153 int flag_overall_time_limit = 0;
154
155public:
156 MznSolver(std::vector<std::string> args = {});
157 ~MznSolver();
158
159 std::pair<SolverInstance::Status, std::string> run();
160 OptionStatus processOptions(std::vector<std::string>& argv);
161 SolverFactory* getSF() {
162 assert(sf);
163 return sf;
164 }
165 SolverInstanceBase::Options* getSI_OPT() {
166 assert(si_opt);
167 return si_opt;
168 }
169 bool get_flag_verbose() { return flag_verbose; /*getFlt()->get_flag_verbose();*/ }
170 void printUsage();
171 std::string printSolution(SolverInstance::Status);
172
173 void pushToSolver();
174 void popFromSolver();
175 std::pair<SolverInstance::Status, std::string> solve();
176
177private:
178 void addDefinitions();
179 Val eval_val(EnvI& env, Expression* e);
180 void printHelp(const std::string& selectedSolver = std::string());
181 /// Flatten model
182 void flatten(const std::string& filename = std::string(),
183 const std::string& modelName = std::string("stdin"));
184 size_t getNSolvers() { return getGlobalSolverRegistry()->getSolverFactories().size(); }
185 /// If building a flattening exe only.
186 bool ifMzn2Fzn();
187 bool ifSolns2out();
188 void addSolverInterface();
189 void addSolverInterface(SolverFactory* sf);
190 void printStatistics();
191
192 SolverInstance::Status getFltStatus() { return interpreter_status; }
193 SolverInstanceBase* getSI() {
194 assert(si);
195 return si;
196 }
197 bool get_flag_statistics() { return flag_statistics; }
198};
199
200} // namespace MiniZinc
201
202#endif