Clingo
Loading...
Searching...
No Matches
head_aggregate.hh
1#pragma once
2
3#include <clingo/ground/literal.hh>
4#include <clingo/ground/matcher.hh>
5#include <clingo/ground/statement.hh>
6
7#include <clingo/util/small_vector.hh>
8
9#include <memory_resource>
10#include <ostream>
11
12namespace CppClingo::Ground {
13
14// Outline:
15// - A :- B.
16// - atoms A are gathered in the aggregate domain
17// (on lower priority than the elements)
18// - there is no need to enqueue the aggregate
19// - propagation only derives heads
20// - element accumulation is independent
21// - accu :- A, E.
22// - gathers aggregate elements
23// - enqueues aggregate A for propagation
24// - propagate
25// - if A can be derived, propagate heads of aggregate elements
26// - output
27// - it might happen that there are aggregates that have not been derived
28// - they are currently output as is but their heads are not propagated
29// - in principle, one could stop grounding if such an aggregate has a true body
30// - classes
31// - AtomHdAggr (to collect head aggregates)
32// - BaseHdAggr (the base for grounding)
33// - StateHdAggr (to gather state for grounding/output)
34// - StmHdAggr (to derive atoms A)
35// - StmHdAggrElem (to accumulate elements)
36// - LitHdAggr (to be used in StmHdAggrElem)
37
40
47 public:
52 using Bound = std::variant<std::pair<Number, Number>, std::pair<Symbol, Symbol>>;
53
55 AtomHdAggr(AggregateFunction fun) : bound_{init_(fun)} {}
56
59
64 auto propagate(GuardVec const &guards, Symbol const *vals) -> bool;
65
67 auto enqueue() -> bool;
71 void dequeue();
72
74 void add_elem(size_t idx);
76 [[nodiscard]] auto elems() const -> std::span<size_t const>;
78 [[nodiscard]] auto todo() -> std::span<size_t const>;
79
81 [[nodiscard]] auto uid() const -> std::optional<size_t>;
83 void uid(size_t uid);
84
85 private:
86 static auto init_(AggregateFunction fun) -> Bound;
87
88 std::vector<size_t> elems_;
89 std::variant<std::pair<Number, Number>, std::pair<Symbol, Symbol>> bound_;
90 size_t propagated_ = 0;
91 size_t uid_ = invalid_offset;
92 bool enqueued_ = false;
93 bool matched_ = false;
94};
95
97class BaseHdAggr : public BaseImpl<Symbol const *, BaseHdAggr> {
98 public:
102
104 BaseHdAggr(size_t size) : atoms_{0, size, size} {}
105
107 auto add(Symbol const *sym, AggregateFunction fun) -> std::pair<AtomMap::iterator, bool>;
108
110 [[nodiscard]] auto size() const -> size_t;
111
115 [[nodiscard]] auto index(Symbol const *sym) const -> size_t;
117 [[nodiscard]] auto nth(size_t i) const -> AtomMap::const_iterator;
119 [[nodiscard]] auto nth(size_t i) -> AtomMap::iterator;
120
122 [[nodiscard]] auto atoms() -> AtomMap &;
123
124 private:
125 AtomMap atoms_;
126};
127
128// Note: this could as well be a small container class
129class StmHdAggrElem;
130
132class StateHdAggr : public State {
133 public:
134 class AtomKey;
139 private:
140 struct priv_tag {};
141
142 public:
144 ElementKey(priv_tag tag, EvalContext const &ctx, AggregateFunction fun, size_t atom_idx, StmHdAggrElem &elem,
145 bool &res);
147 ElementKey(ElementKey const &other) = delete;
149 [[nodiscard]] static auto construct(auto &mbr, EvalContext const &ctx, AggregateFunction fun, size_t atom_idx,
150 StmHdAggrElem &elem) -> bool;
151
153 void mark_fact() const;
155 [[nodiscard]] auto fact() const -> bool;
156
158 [[nodiscard]] auto size() const -> size_t;
160 [[nodiscard]] auto span() const -> SymbolSpan;
162 [[nodiscard]] auto hash() const -> size_t;
164 friend auto operator==(ElementKey const &a, ElementKey const &b) -> bool;
165
166 private:
167 // Note that these two could be combined to save a little bit of memory.
168 mutable size_t n_;
169 size_t atom_idx_;
170 // NOLINTBEGIN
171 CLINGO_IGNORE_ZERO_SIZED_ARRAY_B
172 Symbol syms_[0];
173 CLINGO_IGNORE_ZERO_SIZED_ARRAY_E
174 // NOLINTEND
175 };
176
183 using ElementMap = Util::ordered_map<ElementKey *, Util::small_vector<std::tuple<Symbol, size_t, size_t>, 1>>;
184
186 StateHdAggr(std::pmr::monotonic_buffer_resource &mbr, BaseVec bases, VariableVec global, GuardVec guards,
187 AggregateFunction fun, size_t index, bool single_pass_body)
188 : base_{global.size()}, global_{std::move(global)}, guards_{std::move(guards)}, bases_{std::move(bases)},
189 mbr_{&mbr}, index_{index}, fun_{fun}, single_pass_body_{single_pass_body} {}
190
192 [[nodiscard]] auto global() const -> VariableVec const &;
194 [[nodiscard]] auto symbols() -> SymbolVec &;
196 [[nodiscard]] auto guards() const -> GuardVec const &;
198 [[nodiscard]] auto fun() const -> AggregateFunction;
201 [[nodiscard]] auto single_pass_body() const -> bool;
203 [[nodiscard]] auto index() const -> size_t;
207 [[nodiscard]] auto indices() const -> std::vector<size_t>;
208
210 void enqueue(Queue &queue);
211
213 void propagate(OutputStm &out, Queue &queue);
214
216 auto insert_atom(EvalContext const &ctx) -> std::optional<std::pair<AtomMap::iterator, bool>>;
217
219 void insert_elem(EvalContext const &ctx, AtomMap::iterator it, StmHdAggrElem &elem);
220
222 void print(std::ostream &out, bool print_index);
223
225 void output(Logger &log, SymbolStore &store, OutputStm &out) override;
226
228 [[nodiscard]] auto base() -> BaseHdAggr &;
229
230 private:
232 void enqueue_(AtomMap::iterator it);
233
237 auto atom_index_(AtomMap::iterator it) -> size_t;
238
239 BaseHdAggr base_;
240 ElementMap tuples_;
241 VariableVec global_;
242 SymbolVec symbols_;
243 GuardVec guards_;
244 BaseVec bases_;
245 std::vector<size_t> queue_;
246 std::pmr::monotonic_buffer_resource *mbr_;
247 AtomKey *atom_key_ = nullptr;
248 size_t index_;
250 bool single_pass_body_;
251};
252
254class StmHdAggr : public Stm {
255 public:
257 StmHdAggr(StateHdAggr &state, Ground::ULitVec body, size_t priority)
258 : state_{&state}, body_{std::move(body)}, priority_{priority} {}
259
260 private:
261 // Stm interface
262 void do_print(std::ostream &out) const override;
263
264 [[nodiscard]] auto do_body() const -> ULitVec const & override;
265 [[nodiscard]] auto do_important() const -> VariableSet override;
266
267 // InstanceCallback interface
268 void do_print_head(std::ostream &out) const override;
269 void do_init(size_t gen) override;
270 [[nodiscard]] auto do_report(EvalContext const &ctx) -> bool override;
271 void do_propagate(SymbolStore &store, OutputStm &out, Queue &queue) override;
272 [[nodiscard]] auto do_priority() const -> size_t override;
273
274 StateHdAggr *state_;
275 ULitVec body_;
276 size_t priority_;
277};
278
280class StmHdAggrElem : public Stm {
281 public:
283 StmHdAggrElem(StateHdAggr &state, std::optional<std::pair<UTerm, AtomBase *>> head, Location loc_weight,
284 UTermVec tuple, ULitVec body)
285 : loc_weight_{std::move(loc_weight)}, state_{&state}, head_{head ? std::move(head->first) : nullptr},
286 base_{head ? head->second : nullptr}, tuple_{std::move(tuple)}, body_{std::move(body)} {}
287
288 private:
289 friend class StateHdAggr;
290 friend class StateHdAggr::ElementKey;
291
292 [[nodiscard]] auto do_body() const -> ULitVec const & override;
293 [[nodiscard]] auto do_important() const -> VariableSet override;
294 void do_init(size_t gen) override;
295 [[nodiscard]] auto do_report(EvalContext const &ctx) -> bool override;
296 void do_propagate(SymbolStore &store, OutputStm &out, Queue &queue) override;
297 [[nodiscard]] auto do_priority() const -> size_t override;
298 void do_print_head(std::ostream &out) const override;
299 void do_print(std::ostream &out) const override;
300
301 auto get_cond_(EvalContext const &ctx) -> std::pair<size_t, bool>;
302
303 Location loc_weight_;
304 StateHdAggr *state_;
305 StateHdAggr::ElementKey *elem_key_ = nullptr;
306 UTerm head_;
307 AtomBase *base_;
308 UTermVec tuple_;
309 ULitVec body_;
310 bool logged_ = false;
311};
312
315 public:
317 using Key = Symbol const *;
318
320 MatchHdAggr(StateHdAggr &state) : state_{&state} {
321 eval_.reserve(state_->global().size() + state_->guards().size());
322 }
323
325 [[nodiscard]] auto vars() const -> VariableSet;
326
328 [[nodiscard]] auto signature(VariableSet const &bound, VariableSet const &bind) const -> VariableVec;
329
331 [[nodiscard]] auto match(EvalContext const &ctx, Symbol const *sym) const -> bool;
332
334 [[nodiscard]] auto eval(EvalContext const &ctx) const -> std::optional<Symbol const *>;
335
337 friend auto operator<<(std::ostream &out, MatchHdAggr const &m) -> std::ostream &;
338
340 [[nodiscard]] auto state() const -> StateHdAggr &;
341
342 private:
343 std::vector<Symbol> mutable eval_;
344 StateHdAggr *state_;
345};
346
348class LitHdAggr : public Lit, private MatchHdAggr {
349 public:
352
353 private:
354 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
355
356 [[nodiscard]] auto do_domain() const -> bool override;
357
359 [[nodiscard]] auto do_single_pass() const -> bool override;
360
361 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
362 std::vector<bool> const &bound)
363 -> std::pair<UMatcher, std::optional<size_t>> override;
364
365 [[nodiscard]] auto do_score(std::vector<bool> const &bound) const -> double override;
366
367 void do_print(std::ostream &out) const override;
368
369 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
370
371 [[nodiscard]] auto do_copy() const -> ULit override;
372
373 [[nodiscard]] auto do_hash() const -> size_t override;
374
375 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
376
377 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
378
379 size_t offset_ = invalid_offset;
380};
381
383
384} // namespace CppClingo::Ground
An atom base used to store derivable atoms and associated state.
Definition base.hh:212
Extensible ground representation of head aggregates.
Definition head_aggregate.hh:46
auto enqueue() -> bool
Enqueue the atom for propagation.
auto propagate(GuardVec const &guards, Symbol const *vals) -> bool
Check if the aggregate matches the guards.
auto uid() const -> std::optional< size_t >
Get the unique id of the aggregate.
auto todo() -> std::span< size_t const >
Get the aggregate elements to propagate.
void dequeue()
Dequeue the atom after propagation.
std::variant< std::pair< Number, Number >, std::pair< Symbol, Symbol > > Bound
The lower and upper bound for the value an aggregate can take.
Definition head_aggregate.hh:52
void accumulate(AggregateFunction fun, SymbolSpan tup, bool fact)
Accumulate a tuple.
auto elems() const -> std::span< size_t const >
Get the aggregate elements.
AtomHdAggr(AggregateFunction fun)
Initialize for the given aggregate function.
Definition head_aggregate.hh:55
void add_elem(size_t idx)
Add a new element.
The base capturing derived head aggregate atoms.
Definition head_aggregate.hh:97
Util::ordered_map< Symbol const *, AtomHdAggr, Util::array_hash, Util::array_equal_to > AtomMap
Map containing the atoms.
Definition head_aggregate.hh:101
BaseHdAggr(size_t size)
Construct an empty base.
Definition head_aggregate.hh:104
auto add(Symbol const *sym, AggregateFunction fun) -> std::pair< AtomMap::iterator, bool >
Add an atom to the current generation.
auto size() const -> size_t
Get the number of derived atoms.
The base implementation of an atom base.
Definition base.hh:148
auto contains(Key const &sym, MatcherType type) const -> std::optional< size_t >
Check if the base contains the given atom with in the given generation.
Definition base.hh:160
Context object to capture state used during instantiation.
Definition instantiator.hh:35
Literal representing an aggregate.
Definition head_aggregate.hh:348
LitHdAggr(StateHdAggr &state)
Construct the aggregate literal.
Definition head_aggregate.hh:351
The base class for groundable literals.
Definition literal.hh:34
A term like object used to match head aggregates.
Definition head_aggregate.hh:314
MatchHdAggr(StateHdAggr &state)
Construct the matcher.
Definition head_aggregate.hh:320
Symbol const * Key
The key to match against.
Definition head_aggregate.hh:317
auto vars() const -> VariableSet
Get the variables of the matcher.
A queue to process instantiators.
Definition instantiator.hh:206
Keys for aggregate elements storing their tuple and their aggregate index.
Definition head_aggregate.hh:138
ElementKey(ElementKey const &other)=delete
Prevent copying and moving.
auto fact() const -> bool
Check if is fact.
static auto construct(auto &mbr, EvalContext const &ctx, AggregateFunction fun, size_t atom_idx, StmHdAggrElem &elem) -> bool
Construct an element key evaluating the given tuple.
ElementKey(priv_tag tag, EvalContext const &ctx, AggregateFunction fun, size_t atom_idx, StmHdAggrElem &elem, bool &res)
Private constructor.
State storing all necessary information to ground head aggregates.
Definition head_aggregate.hh:132
auto guards() const -> GuardVec const &
Get the non-ground guards of the aggregate.
Util::ordered_map< ElementKey *, Util::small_vector< std::tuple< Symbol, size_t, size_t >, 1 > > ElementMap
A map from tuples to their head atoms and conditions.
Definition head_aggregate.hh:183
auto global() const -> VariableVec const &
Get the global variables in the aggregate.
BaseHdAggr::AtomMap AtomMap
A map from global variables (including the guards) to the aggregate representation.
Definition head_aggregate.hh:178
Class to store state for grounding.
Definition base.hh:438
Gather aggregate elements.
Definition head_aggregate.hh:280
StmHdAggrElem(StateHdAggr &state, std::optional< std::pair< UTerm, AtomBase * > > head, Location loc_weight, UTermVec tuple, ULitVec body)
Construct the statement.
Definition head_aggregate.hh:283
A statement deriving head aggregate atoms to trigger grounding of elements.
Definition head_aggregate.hh:254
StmHdAggr(StateHdAggr &state, Ground::ULitVec body, size_t priority)
Construct the statement.
Definition head_aggregate.hh:257
Base class for groundable statements.
Definition statement.hh:17
The Location of an expression in an input source.
Definition location.hh:44
Simple logger to report message to stderr or via a callback.
Definition logger.hh:63
An arbitrary precision integer.
Definition number.hh:27
Interface to output literals.
Definition output.hh:61
Interface to output statements.
Definition output.hh:90
A store for symbols.
Definition symbol.hh:454
Variant-like class to store symbols stored in a symbol store.
Definition symbol.hh:225
std::span< Symbol const > SymbolSpan
A span of symbols.
Definition symbol.hh:218
std::vector< Symbol > SymbolVec
A vector of symbols.
Definition symbol.hh:220
AggregateFunction
Enumeration of aggregate functions.
Definition core.hh:87
VariableSet::values_container_type VariableVec
A vector of variables.
Definition base.hh:21
Util::ordered_set< size_t > VariableSet
A set of variables.
Definition base.hh:19
@ fact
Indicates that the atom is derived by a fact.
MatcherType
Enumeration of matcher types.
Definition instantiator.hh:48
std::unique_ptr< Matcher > UMatcher
A unique pointer to a matcher.
Definition instantiator.hh:100
std::unique_ptr< Lit > ULit
A unique pointer holding a literal.
Definition literal.hh:29
VarSelectMode
Available variable selection modes.
Definition literal.hh:21
std::vector< std::tuple< std::tuple< String, size_t, bool >, AtomBase *, std::vector< size_t > > > BaseVec
A vector of signatures, bases, and indices.
Definition literal.hh:372
std::vector< ULit > ULitVec
A vector of literals.
Definition literal.hh:31
std::vector< std::pair< Relation, UTerm > > GuardVec
A vector of guards.
Definition term.hh:37
std::unique_ptr< Term > UTerm
A unique pointer holding a term.
Definition term.hh:33
std::vector< UTerm > UTermVec
A vector of terms.
Definition term.hh:35
tsl::ordered_map< Key, T, Hash, KeyEqual, Allocator, ValueTypeContainer, IndexType > ordered_map
Alias for ordered maps.
Definition ordered_map.hh:16