Clingo
Loading...
Searching...
No Matches
control.hh
1#pragma once
2
3#include <clingo/backend.hh>
4#include <clingo/base.hh>
5#include <clingo/config.hh>
6#include <clingo/core.hh>
7#include <clingo/ground.hh>
8#include <clingo/observe.hh>
9#include <clingo/profile.hh>
10#include <clingo/propagate.hh>
11#include <clingo/solve.hh>
12#include <clingo/stats.hh>
13#include <clingo/symbol.hh>
14
15#include <clingo/control.h>
16
17#include <cassert>
18#include <optional>
19#include <span>
20
21namespace Clingo {
22
23namespace AST {
24
25class Program;
26auto c_cast(Program const &x) -> clingo_program_t *;
27
28} // namespace AST
29
30namespace Detail {
31
32void join(clingo_control_t *ctx, clingo_program_t const *prg);
33
34} // namespace Detail
35
40
44class ConstMap {
45 public:
47 using key_type = std::string_view;
51 using value_type = std::pair<key_type, mapped_type>;
53 using size_type = std::size_t;
55 using difference_type = std::ptrdiff_t;
59 using pointer = Detail::ArrowProxy<value_type>;
61 using iterator = Detail::RandomAccessIterator<ConstMap>;
62
66 explicit ConstMap(clingo_const_map_t const *map) : map_{map} {}
67
72 [[nodiscard]] auto contains(key_type name) const -> bool {
73 return Detail::call<clingo_const_map_find>(map_, name.data(), name.size(), nullptr);
74 }
75
80 [[nodiscard]] auto operator[](key_type name) const -> mapped_type {
81 clingo_symbol_t sym = 0;
82 bool found = false;
83 Detail::handle_error(clingo_const_map_find(map_, name.data(), name.size(), &sym, &found));
84 return found ? Symbol{sym, true} : throw std::out_of_range{"key not found"};
85 }
86
91 [[nodiscard]] auto at(size_t index) const -> value_type {
92 clingo_string_t name;
93 clingo_symbol_t sym = 0;
94 Detail::handle_error(clingo_const_map_at(map_, index, &name, &sym));
95 return {{name.data, name.size}, Symbol{sym, true}};
96 }
97
101 [[nodiscard]] auto size() const -> size_type { return Detail::call<clingo_const_map_size>(map_); }
102
106 [[nodiscard]] auto begin() const -> iterator { return iterator{*this, 0}; }
107
111 [[nodiscard]] auto end() const -> iterator { return iterator{*this, size()}; }
112
113 private:
114 clingo_const_map_t const *map_;
115};
116
126
138
147
149enum class DiscardType {
150 minimize = clingo_discard_type_e::minimize,
151 project = clingo_discard_type_e::project,
152};
153
159class Control {
160 public:
166 using Context = std::function<SymbolVector(std::string_view, SymbolSpan)>;
167
172 explicit Control(Library const &lib, StringList arguments) : Clingo::Control{lib, StringSpan{arguments}} {}
173
175 explicit Control(Library const &lib, StringSpan arguments = {}) {
176 auto cstrs = Detail::transform(arguments, [](auto const &x) { return clingo_string_t{x.data(), x.size()}; });
177 ctl_.reset(Detail::call<clingo_control_new>(c_cast(lib), cstrs.data(), arguments.size()), false);
178 }
179
186 explicit Control(clingo_control_t *rep, bool acquire) : ctl_{rep, acquire} {}
187
192 [[nodiscard]] friend auto c_cast(Control const &ctl) -> clingo_control_t * { return ctl.ctl_.get(); }
193
197 [[nodiscard]] auto mode() const -> ControlMode {
198 return static_cast<ControlMode>(Detail::call<clingo_control_mode>(ctl_.get()));
199 }
200
209 void write_aspif(std::string_view path, WriteAspifFlags flags = WriteAspifFlags::none) const {
210 Detail::handle_error(clingo_control_write_aspif(ctl_.get(), path.data(), path.size(),
211 static_cast<clingo_write_aspif_mode_t>(flags)));
212 }
213
222 void parse_files(StringSpan files) const {
223 auto cfiles = Detail::transform(files, [](auto const &x) { return clingo_string_t{x.data(), x.size()}; });
224 Detail::handle_error(clingo_control_parse_files(ctl_.get(), cfiles.data(), cfiles.size()));
225 }
226
235 void parse_files(StringList files) const { parse_files(StringSpan{files.begin(), files.end()}); }
236
240 void parse_string(std::string_view program) const {
241 Detail::handle_error(clingo_control_parse_string(ctl_.get(), program.data(), program.size()));
242 }
243
252 void ground(std::optional<PartSpan> parts = std::nullopt, Context ctx = nullptr) const {
253 auto [default_parts, c_parts] = c_parts_(parts);
255 []([[maybe_unused]] char const *name, [[maybe_unused]] size_t name_size,
256 [[maybe_unused]] size_t arguments_size, [[maybe_unused]] void *data, bool *result) -> bool {
257 CLINGO_TRY {
258 *result = true;
259 }
260 CLINGO_CATCH;
261 },
262 []([[maybe_unused]] clingo_lib_t *lib, [[maybe_unused]] clingo_location_t const *location, char const *name,
263 size_t name_size, clingo_symbol_t const *arguments, size_t arguments_size, void *data,
264 clingo_symbol_callback_t symbol_callback, void *symbol_callback_data) -> bool {
265 CLINGO_TRY {
266 auto &cb = *static_cast<std::function<SymbolVector(std::string_view, SymbolSpan)> *>(data);
267 auto syms = cb({name, name_size}, {cpp_cast(arguments), arguments_size});
268 auto const *c_syms = c_cast(syms.data());
269 return symbol_callback(c_syms, syms.size(), symbol_callback_data);
270 }
271 CLINGO_CATCH;
272 },
273 nullptr,
274 nullptr,
275 };
276
277 Detail::handle_error(
278 clingo_control_ground(ctl_.get(), c_parts.data(), c_parts.size(), ctx ? &handler : nullptr, &ctx));
279 }
280
289 void ground(std::initializer_list<Part> parts, Context ctx = nullptr) const {
290 ground(PartSpan{parts}, std::move(ctx));
291 }
292
306 template <Detail::UserData<GroundEventHandler> Handler = std::nullptr_t>
307 [[nodiscard]] auto start_ground(std::optional<PartSpan> parts = std::nullopt, Handler &&handler = nullptr) const
308 -> GroundHandle {
309 auto [default_parts, c_parts] = c_parts_(parts);
310 using UserData = Detail::UserDataTraits<Handler>;
311 auto user_data = UserData::create(std::forward<Handler>(handler));
312 clingo_ground_event_handler_t const *c_handler_ptr = nullptr;
313 if constexpr (UserData::has_data) {
314 if (UserData::has_value(user_data)) {
315 static constexpr auto c_handler = clingo_ground_event_handler_t{
316 [](char const *name, size_t name_size, size_t arguments_size, void *data, bool *result) -> bool {
317 CLINGO_TRY {
318 *result = UserData::cast(data)->callable(std::string_view{name, name_size}, arguments_size);
319 }
320 CLINGO_CATCH;
321 },
322 []([[maybe_unused]] clingo_lib_t *lib, clingo_location_t const *location, char const *name,
323 size_t name_size, clingo_symbol_t const *arguments, size_t arguments_size, void *data,
324 clingo_symbol_callback_t symbol_callback, void *symbol_callback_data) -> bool {
325 CLINGO_TRY {
326 Location loc{location};
327 auto syms = UserData::cast(data)->call(loc, {name, name_size},
328 {cpp_cast(arguments), arguments_size});
329 auto const *c_syms = c_cast(syms.data());
330 return symbol_callback(c_syms, syms.size(), symbol_callback_data);
331 }
332 CLINGO_CATCH;
333 },
334 [](clingo_ground_result_t result, void *data) {
335 UserData::cast(data)->finish(static_cast<GroundResult>(result));
336 },
337 [](void *data) { UserData::free(data); },
338 };
339 c_handler_ptr = &c_handler;
340 }
341 }
342 clingo_ground_handle_t *handle = nullptr;
343 Detail::handle_error(clingo_control_start_ground(ctl_.get(), c_parts.data(), c_parts.size(), c_handler_ptr,
344 UserData::release(user_data), &handle));
345 return GroundHandle{handle};
346 }
347
349 template <Detail::UserData<GroundEventHandler> Handler = std::nullptr_t>
350 [[nodiscard]] auto start_ground(std::initializer_list<Part> parts, Handler &&handler = nullptr) const
351 -> GroundHandle {
352 return start_ground(PartSpan{parts}, std::forward<Handler>(handler));
353 }
354
358 [[nodiscard]] auto base() const -> Base { return Base{Detail::call<clingo_control_base>(ctl_.get())}; }
359
363 [[nodiscard]] auto stats() const -> ConstStats {
364 auto const *stats = Detail::call<clingo_control_stats>(ctl_.get());
365 auto key = Detail::call<clingo_stats_root>(stats);
366 return ConstStats{stats, key};
367 }
368
375 auto profile() -> std::vector<ProfileNode> {
376 struct Builder {
377 static auto internal(size_t depth, char const *key, size_t key_size, bool nested, void *data) -> bool {
378 CLINGO_TRY {
379 auto *self = static_cast<Builder *>(data);
380 assert(depth <= self->stack.size());
381 self->stack.resize(depth);
382 auto node = ProfileNodeInternal{std::string{key, key_size}, nested};
383 if (self->stack.empty()) {
384 self->roots.emplace_back(std::move(node));
385 self->stack.emplace_back(&self->roots.back());
386 } else {
387 auto &children = std::get<ProfileNodeInternal>(*self->stack.back()).children;
388 children.emplace_back(std::move(node));
389 self->stack.emplace_back(&children.back());
390 }
391 }
392 CLINGO_CATCH;
393 }
394 static auto leaf(size_t depth, clingo_profile_data_t *values, clingo_profile_type_t type, void *data)
395 -> bool {
396 CLINGO_TRY {
397 auto *self = static_cast<Builder *>(data);
398 assert(depth <= self->stack.size());
399 self->stack.resize(depth);
400 auto node = ProfileNodeLeaf{static_cast<ProfileType>(type), values->matches, values->instances,
401 values->time_instantiate, values->time_propagate};
402 if (self->stack.empty()) {
403 self->roots.emplace_back(node);
404 } else {
405 std::get<ProfileNodeInternal>(*self->stack.back()).children.emplace_back(node);
406 }
407 }
408 CLINGO_CATCH;
409 }
410
411 std::vector<ProfileNode *> stack;
412 std::vector<ProfileNode> roots;
413 } builder;
414
415 auto visitor = clingo_profile_visitor_t{&Builder::internal, &Builder::leaf};
416 clingo_control_profile(ctl_.get(), &visitor, &builder);
417 return std::move(builder.roots);
418 }
419
425 template <Detail::UserData<SolveEventHandler> Handler = std::nullptr_t>
426 [[nodiscard]] auto solve(ProgramLiteralSpan assumptions = {}, Handler &&handler = nullptr) const -> SolveResult {
427 return solve_(std::forward<Handler>(handler), assumptions, SolveFlags::empty).get();
428 }
429
431 template <Detail::UserData<SolveEventHandler> Handler = std::nullptr_t>
432 [[nodiscard]] auto solve(std::initializer_list<ProgramLiteral> assumptions, Handler &&handler = nullptr) const
433 -> SolveResult {
434 return solve_(std::forward<Handler>(handler), ProgramLiteralSpan{assumptions}, SolveFlags::empty).get();
435 }
436
447 template <Detail::UserData<SolveEventHandler> Handler = std::nullptr_t>
448 [[nodiscard]] auto start_solve(ProgramLiteralSpan assumptions = {}, SolveFlags flags = SolveFlags::yield,
449 Handler &&handler = nullptr) const -> SolveHandle {
450 return solve_(std::forward<Handler>(handler), assumptions, flags);
451 }
452
454 template <Detail::UserData<SolveEventHandler> Handler = std::nullptr_t>
455 [[nodiscard]] auto start_solve(std::initializer_list<ProgramLiteral> assumptions,
456 SolveFlags flags = SolveFlags::yield, Handler &&handler = nullptr) const
457 -> SolveHandle {
458 return solve_(std::forward<Handler>(handler), ProgramLiteralSpan{assumptions}, flags);
459 }
460
465 void main() const { Detail::handle_error(clingo_control_main(ctl_.get())); }
466
470 void interrupt() const { clingo_control_interrupt(ctl_.get()); }
471
475 void discard(DiscardType type) const {
476 Detail::handle_error(clingo_control_discard(ctl_.get(), static_cast<clingo_discard_type_t>(type)));
477 }
478
485 [[nodiscard]] auto buffer() const -> std::string_view {
486 auto [data, size] = Detail::call<clingo_control_buffer>(ctl_.get());
487 return {data, size};
488 }
489
496 [[nodiscard]] auto parts() const -> std::optional<PartVector> {
497 clingo_part_t const *parts = nullptr;
498 size_t size = 0;
499 bool has_value = false;
500 Detail::handle_error(clingo_control_get_parts(ctl_.get(), &parts, &size, &has_value));
501 if (has_value) {
502 return Detail::transform(std::span{parts, size}, [](auto const &part) {
503 auto params = std::span{cpp_cast(part.params), part.params_size};
504 return Part{{part.name, part.name_size}, {params.begin(), params.end()}};
505 });
506 }
507 return std::nullopt;
508 }
509
513 void parts(PartList parts) const { this->parts(std::span{parts.begin(), parts.end()}); }
514
520 void parts(std::optional<PartSpan> parts) const {
521 if (parts) {
522 auto cparts = Detail::transform(*parts, [](auto const &part) {
523 return clingo_part_t{part.name.data(), part.name.size(), c_cast(part.params.data()),
524 part.params.size()};
525 });
526 Detail::handle_error(clingo_control_set_parts(ctl_.get(), cparts.data(), cparts.size(), true));
527 } else {
528 Detail::handle_error(clingo_control_set_parts(ctl_.get(), nullptr, 0, true));
529 }
530 }
531
535 [[nodiscard]] auto config() const -> Config {
536 auto *config = Detail::call<clingo_control_config>(ctl_.get());
537 auto key = Detail::call<clingo_config_root>(config);
538 return Config{config, key};
539 }
540
544 [[nodiscard]] auto const_map() const -> ConstMap {
545 return ConstMap{Detail::call<clingo_control_const_map>(ctl_.get())};
546 }
547
552 void observe(Observer &obs, bool preprocess = true) const { obs.observe(ctl_.get(), preprocess); }
553
557 [[nodiscard]] auto backend() const -> ProgramBackend {
558 return ProgramBackend{Detail::call<clingo_control_backend>(ctl_.get())};
559 }
560
568 template <Detail::UserData<Propagator, false> P> auto register_propagator(P &&propagator) const -> decltype(auto) {
569 using UserData = Detail::UserDataTraits<P>;
570 auto user_data = UserData::create(std::forward<P>(propagator));
571 if (!UserData::has_value(user_data)) {
572 throw std::invalid_argument{"propagator cannot be null"};
573 }
574 auto &res = *UserData::get(user_data);
575
576 static constexpr auto decide = []() {
577 if constexpr (std::is_base_of_v<Heuristic, typename UserData::ValueType>) {
578 return [](clingo_assignment_t const *assignment, clingo_literal_t fallback, void *data,
579 clingo_literal_t *decision) -> bool {
580 CLINGO_TRY {
581 *decision = UserData::cast(data)->decide(Assignment{assignment}, fallback);
582 }
583 CLINGO_CATCH;
584 };
585 } else {
586 return nullptr;
587 }
588 };
589
590 static constexpr auto c_propagator = clingo_propagator_t{
591 [](clingo_assignment_t const *assignment, clingo_propagate_init_t *init, void *data) -> bool {
592 CLINGO_TRY {
593 UserData::cast(data)->init(Assignment{assignment}, PropagateInit{init});
594 }
595 CLINGO_CATCH;
596 },
597 [](clingo_assignment_t const *assignment, clingo_propagate_control_t *control, void *data) {
598 CLINGO_TRY {
599 UserData::cast(data)->attach(Assignment{assignment}, PropagateControl{control});
600 }
601 CLINGO_CATCH;
602 },
603 [](clingo_assignment_t const *assignment, clingo_propagate_control_t *control,
604 clingo_literal_t const *changes, size_t size, void *data) -> bool {
605 CLINGO_TRY {
606 UserData::cast(data)->propagate(Assignment{assignment}, PropagateControl{control},
607 SolverLiteralSpan{changes, size});
608 }
609 CLINGO_CATCH;
610 },
611 [](clingo_assignment_t const *assignment, clingo_literal_t const *changes, size_t size, void *data) {
612 try {
613 UserData::cast(data)->undo(Assignment{assignment}, SolverLiteralSpan{changes, size});
614 } catch (std::exception const &e) {
615 fprintf(stderr, "panic: %s\n", e.what());
616 std::terminate();
617 }
618 },
619 [](clingo_assignment_t const *assignment, clingo_propagate_control_t *control, void *data) -> bool {
620 CLINGO_TRY {
621 UserData::cast(data)->check(Assignment{assignment}, PropagateControl{control});
622 }
623 CLINGO_CATCH;
624 },
625 decide(),
626 [](void *data) { UserData::free(data); },
627 };
628
629 Detail::handle_error(
630 clingo_control_register_propagator(ctl_.get(), &c_propagator, UserData::release(user_data)));
631 return res;
632 }
633
637 void join(AST::Program const &prg) const { Detail::join(ctl_.get(), c_cast(prg)); }
638
639 private:
640 friend class Detail::intrusive_handle<Control, clingo_control_t>;
641
642 static auto acquire(clingo_control_t *ptr) { clingo_control_acquire(ptr); }
643
644 static auto release(clingo_control_t *ptr) { clingo_control_release(ptr); }
645
646 template <Detail::UserData<SolveEventHandler> Handler = std::nullptr_t>
647 [[nodiscard]] auto solve_(Handler &&handler, ProgramLiteralSpan const &assumptions, SolveFlags flags) const
648 -> SolveHandle {
649 using UserData = Detail::UserDataTraits<Handler>;
650 auto user_data = UserData::create(std::forward<Handler>(handler));
651 clingo_solve_event_handler_t const *c_handler_ptr = nullptr;
652 if constexpr (UserData::has_data) {
653 if (UserData::has_value(user_data)) {
654 static constexpr auto c_solve_event_handler = clingo_solve_event_handler_t{
655 [](clingo_model_t *model, void *data, bool *goon) -> bool {
656 CLINGO_TRY {
657 auto *hnd = UserData::cast(data);
658 assert(hnd != nullptr);
659 auto mdl = Model{model};
660 *goon = hnd->model(mdl);
661 return true;
662 }
663 CLINGO_CATCH;
664 },
665 [](int64_t const *values, size_t size, void *data) -> bool {
666 CLINGO_TRY {
667 auto *hnd = UserData::cast(data);
668 assert(hnd != nullptr);
669 hnd->unsat({values, size});
670 }
671 CLINGO_CATCH;
672 },
673 [](clingo_stats_t *stats, void *data) -> bool {
674 CLINGO_TRY {
675 auto *hnd = UserData::cast(data);
676 assert(hnd != nullptr);
677 std::string_view user_step = "user_step";
678 std::string_view user_accu = "user_accu";
679 uint64_t root = Detail::call<clingo_stats_root>(stats);
680 uint64_t step = Detail::call<clingo_stats_map_add_subkey>(
681 stats, root, user_step.data(), user_step.size(), clingo_stats_type_map);
682 uint64_t accu = Detail::call<clingo_stats_map_add_subkey>(
683 stats, root, user_accu.data(), user_accu.size(), clingo_stats_type_map);
684 hnd->stats(Stats{stats, step}, Stats{stats, accu});
685 }
686 CLINGO_CATCH;
687 },
688 [](clingo_solve_result_bitset_t result, void *data) -> void {
689 auto *hnd = UserData::cast(data);
690 assert(hnd != nullptr);
691 hnd->finish(static_cast<SolveResult>(result));
692 },
693 [](void *data) { UserData::free(data); },
694 };
695 c_handler_ptr = &c_solve_event_handler;
696 }
697 }
698
699 clingo_solve_handle_t *res = nullptr;
700 Detail::handle_error(clingo_control_solve(ctl_.get(), static_cast<clingo_solve_mode_bitset_t>(flags),
701 assumptions.data(), assumptions.size(), c_handler_ptr,
702 UserData::release(user_data), &res));
703 return SolveHandle{res};
704 }
705
713 [[nodiscard]] auto c_parts_(std::optional<PartSpan> parts = std::nullopt) const
714 -> std::pair<std::optional<PartVector>, std::vector<clingo_part_t>> {
715 auto res = std::pair<std::optional<PartVector>, std::vector<clingo_part_t>>{};
716 auto &[default_parts, c_parts] = res;
717 if (!parts) {
718 parts = default_parts = this->parts();
719 }
720 if (!parts) {
721 static auto default_part = Part{"base", {}};
722 parts = PartSpan{&default_part, 1};
723 }
724 assert(parts);
725 c_parts.reserve(parts->size());
726 for (auto const &part : *parts) {
727 c_parts.emplace_back(part.name.data(), part.name.size(), c_cast(part.params.data()), part.params.size());
728 }
729 return res;
730 }
731
732 Detail::intrusive_handle<Control, clingo_control_t> ctl_;
733};
734
736
737} // namespace Clingo
A program to add statements to.
Definition ast.hh:812
Represents a (partial) assignment of a particular solver.
Definition propagate.hh:140
A base that maps signatures to atom bases, and captures term and theory bases.
Definition base.hh:607
Class modeling a mutable configuration entry.
Definition config.hh:138
Class to providing a view on the const directives in a logic program.
Definition control.hh:44
auto operator[](key_type name) const -> mapped_type
Get the value of for the given key.
Definition control.hh:80
std::ptrdiff_t difference_type
The difference type.
Definition control.hh:55
std::size_t size_type
The size type.
Definition control.hh:53
Detail::RandomAccessIterator< ConstMap > iterator
The iterator type.
Definition control.hh:61
value_type reference
The reference type.
Definition control.hh:57
auto contains(key_type name) const -> bool
Check if the map contains the given key.
Definition control.hh:72
std::string_view key_type
The key type.
Definition control.hh:47
auto at(size_t index) const -> value_type
Get the key value pair at the given index.
Definition control.hh:91
std::pair< key_type, mapped_type > value_type
The value type.
Definition control.hh:51
Detail::ArrowProxy< value_type > pointer
The pointer type.
Definition control.hh:59
auto begin() const -> iterator
Get an iterator to the beginning of the map.
Definition control.hh:106
ConstMap(clingo_const_map_t const *map)
Construct from the underlying C representation.
Definition control.hh:66
auto end() const -> iterator
Get an iterator to the end of the map.
Definition control.hh:111
auto size() const -> size_type
Get the size of the map.
Definition control.hh:101
Class modeling an immutable view on a statistics entry.
Definition stats.hh:29
The main control class for grounding and solving logic programs.
Definition control.hh:159
auto start_ground(std::optional< PartSpan > parts=std::nullopt, Handler &&handler=nullptr) const -> GroundHandle
Ground the logic program with the given parameters.
Definition control.hh:307
auto config() const -> Config
Get the configuration of the control object.
Definition control.hh:535
void discard(DiscardType type) const
Discard the statements of the given types.
Definition control.hh:475
void parts(std::optional< PartSpan > parts) const
Set the parts to ground.
Definition control.hh:520
void observe(Observer &obs, bool preprocess=true) const
Inspect the current ground program held by the control object.
Definition control.hh:552
auto base() const -> Base
Get the base of the program.
Definition control.hh:358
void write_aspif(std::string_view path, WriteAspifFlags flags=WriteAspifFlags::none) const
Write the current program to an ASPIF file.
Definition control.hh:209
Control(Library const &lib, StringSpan arguments={})
Constructs a control object with the given library and arguments.
Definition control.hh:175
auto stats() const -> ConstStats
Get the statistics of the control object.
Definition control.hh:363
void ground(std::initializer_list< Part > parts, Context ctx=nullptr) const
Ground the control object with the given parts.
Definition control.hh:289
auto start_ground(std::initializer_list< Part > parts, Handler &&handler=nullptr) const -> GroundHandle
Ground the logic program with the given parameters.
Definition control.hh:350
auto parts() const -> std::optional< PartVector >
Get the parts to ground.
Definition control.hh:496
auto const_map() const -> ConstMap
Get the constant map of the control object.
Definition control.hh:544
auto start_solve(std::initializer_list< ProgramLiteral > assumptions, SolveFlags flags=SolveFlags::yield, Handler &&handler=nullptr) const -> SolveHandle
Start solving the grounded program with the given assumptions and flags.
Definition control.hh:455
Control(clingo_control_t *rep, bool acquire)
Constructs a control object from an existing C representation.
Definition control.hh:186
void parts(PartList parts) const
Set the parts to ground.
Definition control.hh:513
auto start_solve(ProgramLiteralSpan assumptions={}, SolveFlags flags=SolveFlags::yield, Handler &&handler=nullptr) const -> SolveHandle
Start solving the grounded program with the given assumptions and flags.
Definition control.hh:448
void interrupt() const
Interrupt the current solve operation.
Definition control.hh:470
void parse_files(StringSpan files) const
Parse files with the given paths.
Definition control.hh:222
auto solve(std::initializer_list< ProgramLiteral > assumptions, Handler &&handler=nullptr) const -> SolveResult
Solve the grounded program with the given assumptions.
Definition control.hh:432
friend auto c_cast(Control const &ctl) -> clingo_control_t *
Cast to the C representation of the control object.
Definition control.hh:192
auto solve(ProgramLiteralSpan assumptions={}, Handler &&handler=nullptr) const -> SolveResult
Solve the grounded program with the given assumptions.
Definition control.hh:426
auto backend() const -> ProgramBackend
Get the backend of the control object.
Definition control.hh:557
auto buffer() const -> std::string_view
Get the text buffer of the control object.
Definition control.hh:485
void main() const
Run the default ground and solve flow.
Definition control.hh:465
Control(Library const &lib, StringList arguments)
Constructs a control object with the given library and arguments.
Definition control.hh:172
void parse_files(StringList files) const
Parse files with the given paths.
Definition control.hh:235
auto register_propagator(P &&propagator) const -> decltype(auto)
Register a propagator with the control object.
Definition control.hh:568
void join(AST::Program const &prg) const
Join the given non-ground program to the current control object.
Definition control.hh:637
void ground(std::optional< PartSpan > parts=std::nullopt, Context ctx=nullptr) const
Ground the logic program with the given parameters.
Definition control.hh:252
auto mode() const -> ControlMode
Get the control mode.
Definition control.hh:197
std::function< SymbolVector(std::string_view, SymbolSpan)> Context
Callbock for injecting symbols into the grounding process.
Definition control.hh:166
auto profile() -> std::vector< ProfileNode >
Obtain the profiling data of the control object.
Definition control.hh:375
void parse_string(std::string_view program) const
Parse a logic program from a string.
Definition control.hh:240
Class to control a running ground call.
Definition ground.hh:83
The main library class for managing global information and logging.
Definition core.hh:564
Class representing a range in a file.
Definition core.hh:749
Observer interface to inspect the current ground program.
Definition observe.hh:15
Program backend to add atoms and statements.
Definition backend.hh:146
Class to control a user-defined propagator.
Definition propagate.hh:311
Object to initialize a user-defined propagator before each solving step.
Definition propagate.hh:434
Class to control a running search.
Definition solve.hh:329
Class to capture the result of solve calls.
Definition solve.hh:16
Class modeling a symbol in Clingo.
Definition symbol.hh:68
struct clingo_program clingo_program_t
Object to store.
Definition ast.h:496
unsigned clingo_discard_type_t
Corresponding type to clingo_discard_type_e.
Definition control.h:222
CLINGO_VISIBILITY_DEFAULT bool clingo_const_map_find(clingo_const_map_t const *map, char const *name, size_t name_size, clingo_symbol_t *symbol, bool *found)
Get the constant with the given name.
int clingo_mode_t
The corresponding type to clingo_mode_e.
Definition control.h:45
CLINGO_VISIBILITY_DEFAULT bool clingo_control_parse_string(clingo_control_t *control, char const *program, size_t size)
Extend the logic program with the given non-ground logic program in string form.
CLINGO_VISIBILITY_DEFAULT bool clingo_control_get_parts(clingo_control_t *control, clingo_part_t const **parts, size_t *size, bool *has_value)
Get the program parts to ground.
CLINGO_VISIBILITY_DEFAULT bool clingo_control_discard(clingo_control_t *control, clingo_discard_type_t type)
Discard the statements of the given types.
CLINGO_VISIBILITY_DEFAULT bool clingo_const_map_at(clingo_const_map_t const *map, size_t index, clingo_string_t *name, clingo_symbol_t *symbol)
Get the name and value of the contstant at the given index.
struct clingo_const_map clingo_const_map_t
A map from constantns to their values.
Definition control.h:48
CLINGO_VISIBILITY_DEFAULT void clingo_control_acquire(clingo_control_t *control)
Increment the reference count of the given control object.
CLINGO_VISIBILITY_DEFAULT bool clingo_control_parse_files(clingo_control_t *control, clingo_string_t const *files, size_t size)
Extend the logic program with a program in a file.
CLINGO_VISIBILITY_DEFAULT void clingo_control_interrupt(clingo_control_t *control)
Interrupt the running search.
CLINGO_VISIBILITY_DEFAULT bool clingo_control_main(clingo_control_t *control)
Execute the default ground and solve flow after parsing.
CLINGO_VISIBILITY_DEFAULT bool clingo_control_set_parts(clingo_control_t *control, clingo_part_t const *parts, size_t size, bool has_value)
Set the program parts to ground.
CLINGO_VISIBILITY_DEFAULT void clingo_control_release(clingo_control_t *control)
Decrement the reference count of the given control object and destroy if zero.
CLINGO_VISIBILITY_DEFAULT bool clingo_control_ground(clingo_control_t *control, clingo_part_t const *parts, size_t size, clingo_ground_event_handler_t const *handler, void *data)
Ground the selected parts of the current (non-ground) logic program.
CLINGO_VISIBILITY_DEFAULT bool clingo_control_start_ground(clingo_control_t *control, clingo_part_t const *parts, size_t size, clingo_ground_event_handler_t const *handler, void *data, clingo_ground_handle_t **handle)
Start grounding a program asynchronously.
@ clingo_mode_ground
parse, rewrite, ground
Definition control.h:41
@ clingo_mode_parse
parse only
Definition control.h:39
@ clingo_mode_rewrite
parse and rewrite
Definition control.h:40
@ clingo_mode_solve
parse, rewrite, ground, and solve
Definition control.h:42
struct clingo_lib clingo_lib_t
A library object storing global information.
Definition core.h:171
struct clingo_location clingo_location_t
Represents a source code location marking its beginning and end.
Definition core.h:354
int32_t clingo_literal_t
Signed integer type used for aspif and solver literals.
Definition core.h:73
struct clingo_ground_handle clingo_ground_handle_t
Handle to an asynchronous ground call.
Definition ground.h:136
unsigned clingo_ground_result_t
Corresponding type to clingo_ground_result_e.
Definition ground.h:59
struct clingo_model clingo_model_t
Object representing a model.
Definition model.h:43
unsigned clingo_write_aspif_mode_t
Corresponding type to clingo_write_aspif_mode_e.
Definition observe.h:30
CLINGO_VISIBILITY_DEFAULT bool clingo_control_write_aspif(clingo_control_t *control, char const *path, size_t size, clingo_write_aspif_mode_t mode)
Write the current logic program in aspif format to a file.
@ clingo_write_aspif_mode_preamble_auto
Write preamble for newly created files.
Definition observe.h:24
@ clingo_write_aspif_mode_symbols
Whether to write symbols in a structured format.
Definition observe.h:27
@ clingo_write_aspif_mode_preamble
Write preamble.
Definition observe.h:23
@ clingo_write_aspif_mode_preprocess
Whether to preprocess the program before writing.
Definition observe.h:26
@ clingo_write_aspif_mode_append
Append to an existing file (or create it).
Definition observe.h:25
CLINGO_VISIBILITY_DEFAULT bool clingo_control_profile(clingo_control_t const *control, clingo_profile_visitor_t const *visit, void *data)
Visit the profiling data of a control object.
int clingo_profile_type_t
Corresponding type to clingo_profile_type_e.
Definition profile.h:36
CLINGO_VISIBILITY_DEFAULT bool clingo_control_register_propagator(clingo_control_t *control, clingo_propagator_t const *propagator, void *data)
Register a custom propagator with the control object.
struct clingo_propagate_control clingo_propagate_control_t
This object can be used to add clauses and propagate literals while solving.
Definition propagate.h:242
struct clingo_assignment clingo_assignment_t
Represents a (partial) assignment of a particular solver.
Definition propagate.h:46
struct clingo_propagate_init clingo_propagate_init_t
Object to initialize a user-defined propagator before each solving step.
Definition propagate.h:255
struct clingo_solve_handle clingo_solve_handle_t
Search handle to a solve call.
Definition solve.h:112
unsigned clingo_solve_result_bitset_t
Corresponding type to clingo_solve_result_e.
Definition solve.h:61
CLINGO_VISIBILITY_DEFAULT bool clingo_control_solve(clingo_control_t *control, clingo_solve_mode_bitset_t mode, clingo_literal_t const *assumptions, size_t assumptions_size, clingo_solve_event_handler_t const *handler, void *data, clingo_solve_handle_t **handle)
Solve the currently grounded logic program enumerating its models.
unsigned clingo_solve_mode_bitset_t
Corresponding type to clingo_solve_mode_e.
Definition solve.h:71
@ clingo_solve_mode_yield
Yield models in calls to clingo_solve_handle_model.
Definition solve.h:67
@ clingo_solve_mode_async
Enable non-blocking search.
Definition solve.h:66
struct clingo_statistic clingo_stats_t
Handle for the solver stats.
Definition stats.h:59
@ clingo_stats_type_map
the entry is a map
Definition stats.h:53
bool(* clingo_symbol_callback_t)(clingo_symbol_t const *symbols, size_t symbols_size, void *data)
Callback function to inject symbols.
Definition symbol.h:60
uint64_t clingo_symbol_t
Type to represent a symbol.
Definition symbol.h:51
SolveResult
The solve result.
Definition solver.hh:304
@ model
The model represents a stable model.
@ map
The configuration entry is a map of configurations.
SolveFlags
Enumeration of the flags for solving a logic program.
Definition control.hh:140
DiscardType
Enumeration of the types of statements that can be discarded.
Definition control.hh:149
WriteAspifFlags
Enumeration of the flags for writing ASPIF files.
Definition control.hh:128
ControlMode
Enumeration of the control modes.
Definition control.hh:120
@ async
Asynchronously solve in the background.
@ yield
Yield models as they are found.
@ empty
Standard event-based solving.
@ project
Discard project statements.
@ minimize
Discard minimize statements.
@ preamble_auto
Write preamble for newly created files.
@ preamble
Write preamble.
@ symbols
Whether to write symbols in a structured format.
@ append
Append to an existing file (or create it).
@ preprocess
Whether to preprocess the program before writing.
@ parse
Parse only.
@ ground
Parse, rewrite, ground.
@ rewrite
Parse and rewrite.
@ solve
Parse, rewrite, ground, and solve.
std::span< std::string_view const > StringSpan
A span of string views.
Definition core.hh:516
std::initializer_list< std::string_view const > StringList
A list of string views.
Definition core.hh:518
std::span< SolverLiteral const > SolverLiteralSpan
A span of solver literals.
Definition core.hh:494
std::span< ProgramLiteral const > ProgramLiteralSpan
A span of program literals.
Definition core.hh:487
@ init
Modify the initial VSIDS score of an atom.
@ release
No longer treat an atom as external.
std::vector< Part > PartVector
A vector of program parts.
Definition ground.hh:35
std::span< Part const > PartSpan
A span of program parts.
Definition ground.hh:31
GroundResult
Enumeration of the results of a grounding process.
Definition ground.hh:38
std::initializer_list< Part > PartList
An initializer list of program parts.
Definition ground.hh:33
ProfileType
Enumeration of the types of profiling data.
Definition profile.hh:18
@ accu
Indicate accumulated profiling data.
@ step
Indicate per step profiling data.
std::vector< Symbol > SymbolVector
A vector of symbols.
Definition symbol.hh:42
std::span< Symbol const > SymbolSpan
A span of symbols, which is a view on a contiguous sequence of symbols.
Definition symbol.hh:38
auto cpp_cast(clingo_symbol_t const *sym) -> Symbol const *
Cast a C symbol to its C++ representation.
Definition symbol.hh:52
#define CLINGO_ENABLE_BITSET_ENUM(E,...)
Opt-in macro for enabling bit operations for a given enum type.
Definition enum.hh:18
A program part to provide inputs to program directives.
Definition ground.hh:16
std::string name
The name of the part.
Definition ground.hh:26
Class to hold profiling data for an expression in a logic program.
Definition profile.hh:49
std::vector< ProfileNode > children
The children of the profile node.
Definition profile.hh:61
Class to hold profiling data for an expression in a logic program.
Definition profile.hh:24
The ground event handler interface.
Definition ground.h:62
Struct used to specify the program parts that have to be grounded.
Definition ground.h:44
char const * name
name of the program part
Definition ground.h:45
Per node performance statistics gathered while grounding a logic program.
Definition profile.h:39
uint64_t time_propagate
The time in nanoseconds spent propagating.
Definition profile.h:47
uint64_t time_instantiate
The time in nanoseconds spent instantiating.
Definition profile.h:45
uint64_t matches
The number of matches produced by the instantiator.
Definition profile.h:41
uint64_t instances
The number of instances produced by the instantiator.
Definition profile.h:43
Visitor for profiling data.
Definition profile.h:51
An instance of this struct has to be registered with a solver to implement a custom propagator.
Definition propagate.h:493
The solve event handler interface.
Definition solve.h:74
Struct to capture strings that are not null-terminated.
Definition core.h:86
char const * data
pointer to the beginning of the string
Definition core.h:87