1 // {{{ MIT License
2
3 // Copyright 2017 Roland Kaminski
4
5 // Permission is hereby granted, free of charge, to any person obtaining a copy
6 // of this software and associated documentation files (the "Software"), to
7 // deal in the Software without restriction, including without limitation the
8 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
9 // sell copies of the Software, and to permit persons to whom the Software is
10 // furnished to do so, subject to the following conditions:
11
12 // The above copyright notice and this permission notice shall be included in
13 // all copies or substantial portions of the Software.
14
15 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
20 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
21 // IN THE SOFTWARE.
22
23 // }}}
24
25 #ifndef CLINGO_CONTROL_HH
26 #define CLINGO_CONTROL_HH
27
28 #include <gringo/symbol.hh>
29 #include <gringo/types.hh>
30 #include <gringo/locatable.hh>
31 #include <gringo/backend.hh>
32 #include <gringo/logger.hh>
33 #include <gringo/output/literal.hh>
34 #include <potassco/clingo.h>
35 #include <clingo.h>
36
37 #define CLINGO_QUOTE_(name) #name
38 #define CLINGO_QUOTE(name) CLINGO_QUOTE_(name)
39 #ifdef CLINGO_BUILD_REVISION
40 # define CLINGO_VERSION_STRING CLINGO_VERSION " (" CLINGO_QUOTE(CLINGO_BUILD_REVISION) ")"
41 #else
42 # define CLINGO_VERSION_STRING CLINGO_VERSION
43 #endif
44
45 namespace Gringo {
46
47 // {{{1 declaration of SymbolicAtoms
48
49 using SymbolicAtoms = clingo_symbolic_atoms;
50 using SymbolicAtomIter = clingo_symbolic_atom_iterator_t;
51
52 } // namespace Gringo
53
54 struct clingo_symbolic_atoms {
55 virtual Gringo::Symbol atom(Gringo::SymbolicAtomIter it) const = 0;
56 virtual Potassco::Lit_t literal(Gringo::SymbolicAtomIter it) const = 0;
57 virtual bool fact(Gringo::SymbolicAtomIter it) const = 0;
58 virtual bool external(Gringo::SymbolicAtomIter it) const = 0;
59 virtual Gringo::SymbolicAtomIter next(Gringo::SymbolicAtomIter it) const = 0;
60 virtual bool valid(Gringo::SymbolicAtomIter it) const = 0;
61 virtual Gringo::SymbolicAtomIter begin(Gringo::Sig sig) const = 0;
62 virtual Gringo::SymbolicAtomIter begin() const = 0;
63 virtual Gringo::SymbolicAtomIter lookup(Gringo::Symbol atom) const = 0;
64 virtual bool eq(Gringo::SymbolicAtomIter it, Gringo::SymbolicAtomIter jt) const = 0;
65 virtual Gringo::SymbolicAtomIter end() const = 0;
66 virtual std::vector<Gringo::Sig> signatures() const = 0;
67 virtual size_t length() const = 0;
68 virtual ~clingo_symbolic_atoms() noexcept = default;
69 };
70
71 namespace Gringo {
72
73 // {{{1 declaration of SolveResult
74
75 class SolveResult {
76 public:
77 enum Satisfiabily : unsigned { Unknown=0, Satisfiable=1, Unsatisfiable=2 };
SolveResult(Satisfiabily status,bool exhausted,bool interrupted)78 SolveResult(Satisfiabily status, bool exhausted, bool interrupted)
79 : repr_(static_cast<unsigned>(status) | (exhausted << 2) | (interrupted << 3)) { }
SolveResult(unsigned repr)80 SolveResult(unsigned repr)
81 : repr_(repr) { }
satisfiable() const82 Satisfiabily satisfiable() const { return static_cast<Satisfiabily>(repr_ & 3); }
exhausted() const83 bool exhausted() const { return (repr_ >> 2) & 1; }
interrupted() const84 bool interrupted() const { return (repr_ >> 3) & 1; }
operator unsigned() const85 operator unsigned() const { return repr_; }
86 private:
87 unsigned repr_;
88 };
89
90 // {{{1 declaration of Model
91
92 enum class ModelType : clingo_model_type_t {
93 StableModel = clingo_model_type_stable_model,
94 BraveConsequences = clingo_model_type_brave_consequences,
95 CautiousConsequences = clingo_model_type_cautious_consequences
96 };
97 using Model = clingo_model;
98 using Int64Vec = std::vector<int64_t>;
99
100 } // namespace Gringo
101
102 using ShowType = clingo_show_type_bitset_t;
103 struct clingo_model {
104 using LitVec = std::vector<std::pair<Gringo::Symbol, bool>>;
105 virtual bool contains(Gringo::Symbol atom) const = 0;
106 virtual Gringo::SymSpan atoms(ShowType showset) const = 0;
107 virtual Gringo::Int64Vec optimization() const = 0;
108 virtual bool optimality_proven() const = 0;
109 virtual void addClause(Potassco::LitSpan const &lits) const = 0;
110 virtual uint64_t number() const = 0;
111 virtual Potassco::Id_t threadId() const = 0;
112 virtual Gringo::ModelType type() const = 0;
113 virtual bool isTrue(Potassco::Lit_t literal) const = 0;
114 virtual Gringo::SymbolicAtoms const &getDomain() const = 0;
115 virtual void add(Potassco::Span<Gringo::Symbol> symbols) = 0;
~clingo_modelclingo_model116 virtual ~clingo_model() { }
117 };
118
119 namespace Gringo {
120
121 // {{{1 declaration of SolveFuture
122
123 struct SolveEventHandler {
124 virtual bool on_model(Model &model);
125 virtual bool on_unsat(Potassco::Span<int64_t> optimization);
126 virtual void on_finish(SolveResult ret, Potassco::AbstractStatistics *step, Potassco::AbstractStatistics *accu);
127 virtual ~SolveEventHandler() = default;
128 };
129 using USolveEventHandler = std::unique_ptr<SolveEventHandler>;
on_model(Model &)130 inline bool SolveEventHandler::on_model(Model &) { return true; }
on_unsat(Potassco::Span<int64_t> optimization)131 inline bool SolveEventHandler::on_unsat(Potassco::Span<int64_t> optimization) { return true; }
on_finish(SolveResult,Potassco::AbstractStatistics *,Potassco::AbstractStatistics *)132 inline void SolveEventHandler::on_finish(SolveResult, Potassco::AbstractStatistics *, Potassco::AbstractStatistics *) { }
133
134 struct SolveFuture {
135 virtual SolveResult get() = 0;
136 virtual Model const *model() = 0;
137 virtual Potassco::LitSpan unsatCore() = 0;
138 virtual bool wait(double timeout) = 0;
139 virtual void cancel() = 0;
140 virtual void resume() = 0;
~SolveFutureGringo::SolveFuture141 virtual ~SolveFuture() { }
142 };
143 using USolveFuture = std::unique_ptr<SolveFuture>;
144
145 struct DefaultSolveFuture : SolveFuture {
DefaultSolveFutureGringo::DefaultSolveFuture146 DefaultSolveFuture(USolveEventHandler cb) : cb_(std::move(cb)) { }
getGringo::DefaultSolveFuture147 SolveResult get() override { resume(); return {SolveResult::Unknown, false, false}; }
modelGringo::DefaultSolveFuture148 Model const *model() override { resume(); return nullptr; }
unsatCoreGringo::DefaultSolveFuture149 Potassco::LitSpan unsatCore() override {
150 throw std::runtime_error("no core available");
151 }
waitGringo::DefaultSolveFuture152 bool wait(double) override { resume(); return true; }
cancelGringo::DefaultSolveFuture153 void cancel() override { resume(); }
resumeGringo::DefaultSolveFuture154 void resume() override {
155 if (!done_) {
156 done_ = true;
157 if (cb_) { cb_->on_finish({SolveResult::Unknown, false, false}, nullptr, nullptr); }
158 }
159 }
160
~DefaultSolveFutureGringo::DefaultSolveFuture161 ~DefaultSolveFuture() override { resume(); }
162 private:
163 USolveEventHandler cb_;
164 bool done_ = false;
165 };
166
167 // {{{1 declaration of ConfigProxy
168
169 struct ConfigProxy {
170 virtual bool hasSubKey(unsigned key, char const *name) const = 0;
171 virtual unsigned getSubKey(unsigned key, char const *name) const = 0;
172 virtual unsigned getArrKey(unsigned key, unsigned idx) const = 0;
173 virtual void getKeyInfo(unsigned key, int* nSubkeys = 0, int* arrLen = 0, const char** help = 0, int* nValues = 0) const = 0;
174 virtual const char* getSubKeyName(unsigned key, unsigned idx) const = 0;
175 virtual bool getKeyValue(unsigned key, std::string &value) const = 0;
176 virtual void setKeyValue(unsigned key, const char *val) = 0;
177 virtual unsigned getRootKey() const = 0;
~ConfigProxyGringo::ConfigProxy178 virtual ~ConfigProxy() { }
179 };
180
181 // {{{1 declaration of Propagator
182
183 using PropagateControl = clingo_propagate_control;
184 using PropagateInit = clingo_propagate_init;
185
186 } // namespace Gringo
187
188 struct clingo_propagate_init {
189 virtual Potassco::Lit_t addLiteral(bool freeze) = 0;
190 virtual bool addClause(Potassco::LitSpan lits) = 0;
191 virtual bool addWeightConstraint(Potassco::Lit_t lit, Potassco::WeightLitSpan lits, Potassco::Weight_t bound, int type, bool eq) = 0;
192 virtual void addMinimize(Potassco::Lit_t literal, Potassco::Weight_t weight, Potassco::Weight_t priority) = 0;
193 virtual bool propagate() = 0;
194 virtual Gringo::Output::DomainData const &theory() const = 0;
195 virtual Gringo::SymbolicAtoms const &getDomain() const = 0;
196 virtual Gringo::Lit_t mapLit(Gringo::Lit_t lit) const = 0;
197 virtual void addWatch(Gringo::Lit_t lit) = 0;
198 virtual void addWatch(uint32_t solverId, Gringo::Lit_t lit) = 0;
199 virtual void removeWatch(Gringo::Lit_t lit) = 0;
200 virtual void removeWatch(uint32_t solverId, Gringo::Lit_t lit) = 0;
201 virtual void freezeLiteral(Gringo::Lit_t lit) = 0;
202 virtual void enableHistory(bool b) = 0;
203 virtual Potassco::AbstractAssignment const &assignment() const = 0;
204 virtual int threads() const = 0;
205 virtual clingo_propagator_check_mode_t getCheckMode() const = 0;
206 virtual void setCheckMode(clingo_propagator_check_mode_t checkMode) = 0;
207 virtual ~clingo_propagate_init() noexcept = default;
208 };
209
210 namespace Gringo {
211
212 struct Propagator : Potassco::AbstractPropagator, Potassco::AbstractHeuristic {
213 virtual ~Propagator() noexcept = default;
214 virtual void init(Gringo::PropagateInit &init) = 0;
215 virtual bool hasHeuristic() const = 0;
216 };
217 using UProp = std::unique_ptr<Propagator>;
218
219 // {{{1 declaration of Control
220
221 using StringVec = std::vector<String>;
222 using Control = clingo_control;
223
224 } // namespace Gringo
225
226 struct clingo_control {
227 using Assumptions = Potassco::LitSpan;
228 using GroundVec = std::vector<std::pair<Gringo::String, Gringo::SymVec>>;
229 using NewControlFunc = Gringo::Control* (*)(int, char const **);
230 using FreeControlFunc = void (*)(Gringo::Control *);
231
232 virtual Gringo::ConfigProxy &getConf() = 0;
233 virtual Gringo::SymbolicAtoms const &getDomain() const = 0;
234
235 virtual void ground(GroundVec const &vec, Gringo::Context *context) = 0;
236 virtual Gringo::USolveFuture solve(Assumptions assumptions, clingo_solve_mode_bitset_t mode, Gringo::USolveEventHandler cb = nullptr) = 0;
237 virtual void interrupt() = 0;
238 virtual void *claspFacade() = 0;
239 virtual void add(std::string const &name, Gringo::StringVec const ¶ms, std::string const &part) = 0;
240 virtual void load(std::string const &filename) = 0;
241 virtual Gringo::Symbol getConst(std::string const &name) const = 0;
242 virtual bool blocked() = 0;
243 virtual void assignExternal(Potassco::Atom_t ext, Potassco::Value_t val) = 0;
244 virtual bool isConflicting() const noexcept = 0;
245 virtual Potassco::AbstractStatistics const *statistics() const = 0;
246 virtual void useEnumAssumption(bool enable) = 0;
247 virtual bool useEnumAssumption() const = 0;
248 virtual void cleanup() = 0;
249 virtual void enableCleanup(bool enable) = 0;
250 virtual bool enableCleanup() const = 0;
251 virtual Gringo::Output::DomainData const &theory() const = 0;
252 virtual void registerPropagator(Gringo::UProp p, bool sequential) = 0;
253 virtual void registerObserver(Gringo::UBackend program, bool replace) = 0;
254 virtual Potassco::Atom_t addProgramAtom() = 0;
255 virtual bool beginAddBackend() = 0;
256 virtual Gringo::Id_t addAtom(Gringo::Symbol sym) = 0;
257 virtual void addFact(Potassco::Atom_t uid) = 0;
258 virtual Gringo::Backend *getBackend() = 0;
259 virtual void endAddBackend() = 0;
260 virtual Gringo::Logger &logger() = 0;
261 virtual void beginAdd() = 0;
262 virtual void add(clingo_ast_t const &ast) = 0;
263 virtual void endAdd() = 0;
264 virtual ~clingo_control() noexcept = default;
265 };
266
267 namespace Gringo {
268
269 // }}}1
270
271 } // namespace Gringo
272
273 #endif // CLINGO_CONTROL_HH
274