Clingo
Loading...
Searching...
No Matches
literal.hh
1#pragma once
2
3#include <clingo/core/core.hh>
4
5#include <clingo/ground/base.hh>
6#include <clingo/ground/instantiator.hh>
7#include <clingo/ground/script.hh>
8#include <clingo/ground/term.hh>
9
10#include <clingo/util/ordered_map.hh>
11
12#include <memory_resource>
13#include <utility>
14
15namespace CppClingo::Ground {
16
19
21enum class VarSelectMode : uint8_t {
22 depend = 1,
23 provide = 2,
24 all = 3,
25};
26
27class Lit;
29using ULit = std::unique_ptr<Lit>;
31using ULitVec = std::vector<ULit>;
32
34class Lit {
35 public:
37 virtual ~Lit() = default;
38
40 void vars(VariableSet &vars, VarSelectMode mode) const { do_vars(vars, mode); }
41
46 [[nodiscard]] auto domain() const -> bool { return do_domain(); }
50 [[nodiscard]] auto single_pass() const -> bool { return do_single_pass(); }
52 [[nodiscard]] auto matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
53 std::vector<bool> const &bound) -> std::pair<UMatcher, std::optional<size_t>> {
54 return do_matcher(mbr, type, bound);
55 }
61 [[nodiscard]] auto score(std::vector<bool> const &bound, double estimate) const -> double {
62 return do_score(bound, estimate);
63 }
68 [[nodiscard]] auto domain_size(EstimateSelector sel) const -> std::optional<double> { return do_domain_size(sel); }
69
74 [[nodiscard]] auto output(EvalContext const &ctx, OutputLit &out) const -> bool { return do_output(ctx, out); }
75
77 [[nodiscard]] auto copy() const -> ULit { return do_copy(); }
78
80 [[nodiscard]] auto hash() const -> size_t { return do_hash(); }
81
83 friend auto operator==(Lit const &a, Lit const &b) -> bool { return a.do_equal_to(b); }
85 friend auto operator<=>(Lit const &a, Lit const &b) -> std::weak_ordering { return a.do_compare_to(b); }
87 friend auto operator<<(std::ostream &out, Lit const &lit) -> std::ostream & {
88 lit.do_print(out);
89 return out;
90 }
91
92 private:
93 virtual void do_vars(VariableSet &vars, VarSelectMode mode) const = 0;
94 [[nodiscard]] virtual auto do_domain() const -> bool = 0;
95 [[nodiscard]] virtual auto do_single_pass() const -> bool { return false; }
96 [[nodiscard]] virtual auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
97 std::vector<bool> const &bound)
98 -> std::pair<UMatcher, std::optional<size_t>> = 0;
99 [[nodiscard]] virtual auto do_score(std::vector<bool> const &bound, double estimate) const -> double = 0;
100 [[nodiscard]] virtual auto do_domain_size(EstimateSelector sel) const -> std::optional<double> = 0;
101 virtual void do_print(std::ostream &out) const = 0;
102 virtual auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool = 0;
103 [[nodiscard]] virtual auto do_copy() const -> ULit = 0;
104 [[nodiscard]] virtual auto do_hash() const -> size_t = 0;
105 [[nodiscard]] virtual auto do_equal_to(Lit const &other) const -> bool = 0;
106 [[nodiscard]] virtual auto do_compare_to(Lit const &other) const -> std::weak_ordering = 0;
107};
108
110class LitComparison : public Lit {
111 public:
113 LitComparison(UTerm lhs, Relation cmp, UTerm rhs) : lhs_{std::move(lhs)}, rhs_{std::move(rhs)}, cmp_{cmp} {}
114
115 private:
116 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
117 [[nodiscard]] auto do_domain() const -> bool override;
118 [[nodiscard]] auto do_single_pass() const -> bool override;
119 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
120 std::vector<bool> const &bound)
121 -> std::pair<UMatcher, std::optional<size_t>> override;
122 [[nodiscard]] auto do_score(std::vector<bool> const &bound, [[maybe_unused]] double estimate) const
123 -> double override;
124 [[nodiscard]] auto do_domain_size(EstimateSelector sel) const -> std::optional<double> override;
125
126 void do_print(std::ostream &out) const override;
127 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
128
129 [[nodiscard]] auto do_copy() const -> ULit override;
130
131 [[nodiscard]] auto do_hash() const -> size_t override;
132 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
133 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
134
135 UTerm lhs_;
136 UTerm rhs_;
137 Relation cmp_;
138};
139
141class LitExternal : public Lit {
142 public:
145 : ctx_{&ctx}, loc_{std::move(loc)}, name_{name}, lhs_{std::move(lhs)}, args_{std::move(args)} {}
146
147 private:
148 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
149 [[nodiscard]] auto do_domain() const -> bool override;
150 [[nodiscard]] auto do_single_pass() const -> bool override;
151 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
152 std::vector<bool> const &bound)
153 -> std::pair<UMatcher, std::optional<size_t>> override;
154 [[nodiscard]] auto do_score(std::vector<bool> const &bound, [[maybe_unused]] double estimate) const
155 -> double override;
156 [[nodiscard]] auto do_domain_size(EstimateSelector sel) const -> std::optional<double> override;
157
158 void do_print(std::ostream &out) const override;
159 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
160
161 [[nodiscard]] auto do_copy() const -> ULit override;
162
163 [[nodiscard]] auto do_hash() const -> size_t override;
164 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
165 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
166
167 ScriptCallback *ctx_;
168 Location loc_;
169 String name_;
170 UTerm lhs_;
171 UTermVec args_;
172};
173
175class LitInterval : public Lit {
176 public:
178 LitInterval(UTerm lhs, UTerm lower, UTerm upper)
179 : lhs_{std::move(lhs)}, lower_{std::move(lower)}, upper_{std::move(upper)} {}
180
181 private:
182 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
183 [[nodiscard]] auto do_domain() const -> bool override;
184 [[nodiscard]] auto do_single_pass() const -> bool override;
185 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
186 std::vector<bool> const &bound)
187 -> std::pair<UMatcher, std::optional<size_t>> override;
188 [[nodiscard]] auto do_score(std::vector<bool> const &bound, [[maybe_unused]] double estimate) const
189 -> double override;
190 [[nodiscard]] auto do_domain_size(EstimateSelector sel) const -> std::optional<double> override;
191
192 void do_print(std::ostream &out) const override;
193 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
194
195 [[nodiscard]] auto do_copy() const -> ULit override;
196
197 [[nodiscard]] auto do_hash() const -> size_t override;
198 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
199 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
200
201 UTerm lhs_;
202 UTerm lower_;
203 UTerm upper_;
204};
205
207constexpr auto stratified_index = std::numeric_limits<size_t>::max();
208
210class LitSymbolic : public Lit {
211 public:
213 LitSymbolic(AtomBase &base, Sign sign, UTerm atom, size_t index, bool domain)
214 : base_{&base}, atom_{std::move(atom)}, index_{index}, sign_{sign}, domain_{domain} {}
215
216 private:
217 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
218 [[nodiscard]] auto do_domain() const -> bool override;
219 [[nodiscard]] auto do_single_pass() const -> bool override;
220 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
221 std::vector<bool> const &bound)
222 -> std::pair<UMatcher, std::optional<size_t>> override;
223 [[nodiscard]] auto do_score(std::vector<bool> const &bound, double estimate) const -> double override;
224 [[nodiscard]] auto do_domain_size(EstimateSelector sel) const -> std::optional<double> override;
225
226 void do_print(std::ostream &out) const override;
227 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
228
229 [[nodiscard]] auto do_copy() const -> ULit override;
230
231 [[nodiscard]] auto do_hash() const -> size_t override;
232 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
233 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
234
235 AtomBase *base_;
236 UTerm atom_;
240 size_t index_;
241 size_t offset_ = 0;
242 Symbol symbol_;
243 Sign sign_;
245 bool domain_;
246};
247
250using AtomSimple = std::optional<std::tuple<Ground::UTerm, AtomBase &, std::vector<size_t>>>;
251
255class LitProject : public Lit {
256 public:
258 LitProject(ProjectState &state, Sign sign, UTerm atom, UTerm p_atom, size_t index, bool domain)
259 : state_{&state}, atom_{std::move(atom)}, p_atom_{std::move(p_atom)}, index_{index}, sign_{sign},
260 domain_{domain} {}
261
262 private:
263 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
264 [[nodiscard]] auto do_domain() const -> bool override;
265 [[nodiscard]] auto do_single_pass() const -> bool override;
266 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
267 std::vector<bool> const &bound)
268 -> std::pair<UMatcher, std::optional<size_t>> override;
269 [[nodiscard]] auto do_score(std::vector<bool> const &bound, double estimate) const -> double override;
270 [[nodiscard]] auto do_domain_size(EstimateSelector sel) const -> std::optional<double> override;
271 void do_print(std::ostream &out) const override;
272 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
273
274 [[nodiscard]] auto do_copy() const -> ULit override;
275
276 [[nodiscard]] auto do_hash() const -> size_t override;
277 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
278 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
279
280 ProjectState *state_;
281 UTerm atom_;
282 UTerm p_atom_;
283 size_t index_;
284 size_t offset_ = 0;
285 Symbol symbol_;
286 Sign sign_;
287 bool domain_;
288};
289
291class LitTuple : public Lit {
292 public:
294 LitTuple(VariableVec vars, SymbolVec &syms) : vars_{std::move(vars)}, syms_{&syms} {
295 assert(vars_.size() == syms_->size());
296 }
297
298 private:
299 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
300 [[nodiscard]] auto do_domain() const -> bool override;
301 [[nodiscard]] auto do_single_pass() const -> bool override;
302 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
303 std::vector<bool> const &bound)
304 -> std::pair<UMatcher, std::optional<size_t>> override;
305 [[nodiscard]] auto do_score([[maybe_unused]] std::vector<bool> const &bound, [[maybe_unused]] double estimate) const
306 -> double override;
307 [[nodiscard]] auto do_domain_size(EstimateSelector sel) const -> std::optional<double> override;
308 void do_print(std::ostream &out) const override;
309 auto do_output([[maybe_unused]] EvalContext const &ctx, OutputLit &out) const -> bool override;
310 [[nodiscard]] auto do_copy() const -> ULit override;
311 [[nodiscard]] auto do_hash() const -> size_t override;
312 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
313 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
314
315 VariableVec vars_;
316 SymbolVec *syms_;
317};
318
320class LitCheck : public Lit {
321 private:
322 [[nodiscard]] virtual auto do_check(EvalContext const &ctx) -> bool = 0;
323
324 [[nodiscard]] auto do_domain() const -> bool override;
325 [[nodiscard]] auto do_single_pass() const -> bool override;
326 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
327 std::vector<bool> const &bound)
328 -> std::pair<UMatcher, std::optional<size_t>> override;
329 [[nodiscard]] auto do_score(std::vector<bool> const &bound, [[maybe_unused]] double estimate) const
330 -> double override;
331 [[nodiscard]] auto do_domain_size(EstimateSelector sel) const -> std::optional<double> override;
332
333 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
334
335 [[nodiscard]] auto do_hash() const -> size_t override;
336 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
337 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
338};
339
341class LitBool : public LitCheck {
342 public:
344 LitBool(bool value) : value_{value} {}
345
346 private:
347 [[nodiscard]] auto do_check(EvalContext const &ctx) -> bool override;
348 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
349 void do_print(std::ostream &out) const override;
350 [[nodiscard]] auto do_copy() const -> ULit override;
351
352 bool value_;
353};
354
358class LitFactCheck : public LitCheck {
359 public:
361 LitFactCheck(AtomBase &base, Term const &atom, Symbol &target) : base_{&base}, atom_{&atom}, target_{&target} {}
362
363 private:
364 [[nodiscard]] auto do_check(EvalContext const &ctx) -> bool override;
365 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
366 void do_print(std::ostream &out) const override;
367 [[nodiscard]] auto do_copy() const -> ULit override;
368
369 AtomBase *base_;
370 Term const *atom_;
371 Symbol *target_;
372};
373
375class LitFailCheck : public LitCheck {
376 public:
381 LitFailCheck(UTermVec terms) : terms_{std::move(terms)} {}
382
383 private:
384 [[nodiscard]] auto do_check(EvalContext const &ctx) -> bool override;
385 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
386 void do_print(std::ostream &out) const override;
387 [[nodiscard]] auto do_copy() const -> ULit override;
388
389 UTermVec terms_;
390};
391
396using BaseVec = std::vector<std::tuple<std::tuple<String, size_t, bool>, AtomBase *, std::vector<size_t>>>;
397
399class LitSimpleAggr : public Lit {
400 public:
402 LitSimpleAggr(UTerm lhs, Relation cmp, AggregateFunction fun, std::vector<UTermVec> tuples)
403 : lhs_{std::move(lhs)}, tuples_{std::move(tuples)}, fun_{fun}, cmp_{cmp} {}
404
405 private:
406 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
407 [[nodiscard]] auto do_domain() const -> bool override;
408 [[nodiscard]] auto do_single_pass() const -> bool override;
409 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
410 std::vector<bool> const &bound)
411 -> std::pair<UMatcher, std::optional<size_t>> override;
412 [[nodiscard]] auto do_score(std::vector<bool> const &bound, [[maybe_unused]] double estimate) const
413 -> double override;
414 [[nodiscard]] auto do_domain_size(EstimateSelector sel) const -> std::optional<double> override;
415
416 void do_print(std::ostream &out) const override;
417 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
418
419 [[nodiscard]] auto do_copy() const -> ULit override;
420
421 [[nodiscard]] auto do_hash() const -> size_t override;
422 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
423 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
424
425 UTerm lhs_;
426 std::vector<UTermVec> tuples_;
428 Relation cmp_;
429};
430
432
433} // namespace CppClingo::Ground
An atom base used to store derivable atoms and associated state.
Definition base.hh:212
Context object to capture state used during instantiation.
Definition instantiator.hh:41
A literal representing a Boolean.
Definition literal.hh:341
LitBool(bool value)
Construct the literal.
Definition literal.hh:344
A literal ensuring that a list of terms evaluates.
Definition literal.hh:320
A literal representing a comparison.
Definition literal.hh:110
LitComparison(UTerm lhs, Relation cmp, UTerm rhs)
Construct the literal.
Definition literal.hh:113
A literal representing a comparison.
Definition literal.hh:141
LitExternal(ScriptCallback &ctx, Location loc, String name, UTerm lhs, UTermVec args)
Construct the literal.
Definition literal.hh:144
Simple literal that discards whenever it matches to a fact.
Definition literal.hh:358
LitFactCheck(AtomBase &base, Term const &atom, Symbol &target)
Construct the literal.
Definition literal.hh:361
A literal ensuring that a list of terms evaluates.
Definition literal.hh:375
LitFailCheck(UTermVec terms)
Construct the literal.
Definition literal.hh:381
A literal representing an interval assignment.
Definition literal.hh:175
LitInterval(UTerm lhs, UTerm lower, UTerm upper)
Construct the literal.
Definition literal.hh:178
A literal similar to a symbolic literal.
Definition literal.hh:255
LitProject(ProjectState &state, Sign sign, UTerm atom, UTerm p_atom, size_t index, bool domain)
Construct the literal.
Definition literal.hh:258
An aggregate literal without conditions.
Definition literal.hh:399
LitSimpleAggr(UTerm lhs, Relation cmp, AggregateFunction fun, std::vector< UTermVec > tuples)
Construct the literal.
Definition literal.hh:402
A symbolic literal.
Definition literal.hh:210
LitSymbolic(AtomBase &base, Sign sign, UTerm atom, size_t index, bool domain)
Construct the literal.
Definition literal.hh:213
An auxiliary literal binding variables to the given symbols upon first match.
Definition literal.hh:291
LitTuple(VariableVec vars, SymbolVec &syms)
Construct the literal.
Definition literal.hh:294
The base class for groundable literals.
Definition literal.hh:34
void vars(VariableSet &vars, VarSelectMode mode) const
Get the variables in the predicate.
Definition literal.hh:40
auto copy() const -> ULit
Copy the literal.
Definition literal.hh:77
virtual ~Lit()=default
Destroy the literal.
auto domain() const -> bool
Returns true if matching literals are always fact.
Definition literal.hh:46
auto domain_size(EstimateSelector sel) const -> std::optional< double >
The size of the literal's domain.
Definition literal.hh:68
friend auto operator<<(std::ostream &out, Lit const &lit) -> std::ostream &
Print the literal.
Definition literal.hh:87
auto output(EvalContext const &ctx, OutputLit &out) const -> bool
Output the literal.
Definition literal.hh:74
auto hash() const -> size_t
Compute a hash for the literal.
Definition literal.hh:80
friend auto operator==(Lit const &a, Lit const &b) -> bool
Compare two literals.
Definition literal.hh:83
auto matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type, std::vector< bool > const &bound) -> std::pair< UMatcher, std::optional< size_t > >
Returns true if the base of the literal is complete at the time of grounding.
Definition literal.hh:52
friend auto operator<=>(Lit const &a, Lit const &b) -> std::weak_ordering
Compare two literals.
Definition literal.hh:85
auto score(std::vector< bool > const &bound, double estimate) const -> double
Compute a score used to order rule bodies.
Definition literal.hh:61
auto single_pass() const -> bool
Returns true if the literal can be grounded in a single pass.
Definition literal.hh:50
The state capturing the base of a projection.
Definition base.hh:368
Interface to call functions during parsing/grounding.
Definition script.hh:28
Term interface.
Definition term.hh:68
The Location of an expression in an input source.
Definition location.hh:44
Interface to output literals.
Definition output.hh:61
Reference to a string stored in a symbol store.
Definition symbol.hh:18
Variant-like class to store symbols stored in a symbol store.
Definition symbol.hh:225
std::vector< Symbol > SymbolVec
A vector of symbols.
Definition symbol.hh:220
EstimateSelector
Selector for which estimates to consider.
Definition core.hh:204
Relation
Enumeration of supported relations.
Definition core.hh:35
Sign
Enumeration of signs (default negation).
Definition core.hh:16
AggregateFunction
Enumeration of aggregate functions.
Definition core.hh:87
@ max
The #min function.
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
@ lit
Conditional literals derived during grounding.
MatcherType
Enumeration of matcher types.
Definition instantiator.hh:54
std::unique_ptr< Matcher > UMatcher
A unique pointer to a matcher.
Definition instantiator.hh:106
std::unique_ptr< Lit > ULit
A unique pointer holding a literal.
Definition literal.hh:29
std::optional< std::tuple< Ground::UTerm, AtomBase &, std::vector< size_t > > > AtomSimple
Represents a simple head literal which is either represented by a symbol term or #false captured by s...
Definition literal.hh:250
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:396
std::vector< ULit > ULitVec
A vector of literals.
Definition literal.hh:31
constexpr auto stratified_index
Marker for stratified literals.
Definition literal.hh:207
@ depend
Get variables a literal depends on.
@ all
Get all variables in a literal.
@ provide
Get variables provided by a literal.
std::unique_ptr< Term > UTerm
A unique pointer holding a term.
Definition term.hh:34
std::vector< UTerm > UTermVec
A vector of terms.
Definition term.hh:36