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 }
57 [[nodiscard]] auto score(std::vector<bool> const &bound) const -> double { return do_score(bound); }
58
63 [[nodiscard]] auto output(EvalContext const &ctx, OutputLit &out) const -> bool { return do_output(ctx, out); }
64
66 [[nodiscard]] auto copy() const -> ULit { return do_copy(); }
67
69 [[nodiscard]] auto hash() const -> size_t { return do_hash(); }
70
72 friend auto operator==(Lit const &a, Lit const &b) -> bool { return a.do_equal_to(b); }
74 friend auto operator<=>(Lit const &a, Lit const &b) -> std::weak_ordering { return a.do_compare_to(b); }
76 friend auto operator<<(std::ostream &out, Lit const &lit) -> std::ostream & {
77 lit.do_print(out);
78 return out;
79 }
80
81 private:
82 virtual void do_vars(VariableSet &vars, VarSelectMode mode) const = 0;
83 [[nodiscard]] virtual auto do_domain() const -> bool = 0;
84 [[nodiscard]] virtual auto do_single_pass() const -> bool { return false; }
85 [[nodiscard]] virtual auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
86 std::vector<bool> const &bound)
87 -> std::pair<UMatcher, std::optional<size_t>> = 0;
88 [[nodiscard]] virtual auto do_score(std::vector<bool> const &bound) const -> double = 0;
89 virtual void do_print(std::ostream &out) const = 0;
90 virtual auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool = 0;
91 [[nodiscard]] virtual auto do_copy() const -> ULit = 0;
92 [[nodiscard]] virtual auto do_hash() const -> size_t = 0;
93 [[nodiscard]] virtual auto do_equal_to(Lit const &other) const -> bool = 0;
94 [[nodiscard]] virtual auto do_compare_to(Lit const &other) const -> std::weak_ordering = 0;
95};
96
98class LitComparison : public Lit {
99 public:
101 LitComparison(UTerm lhs, Relation cmp, UTerm rhs) : lhs_{std::move(lhs)}, rhs_{std::move(rhs)}, cmp_{cmp} {}
102
103 private:
104 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
105 [[nodiscard]] auto do_domain() const -> bool override;
106 [[nodiscard]] auto do_single_pass() const -> bool override;
107 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
108 std::vector<bool> const &bound)
109 -> std::pair<UMatcher, std::optional<size_t>> override;
110 [[nodiscard]] auto do_score(std::vector<bool> const &bound) const -> double override;
111
112 void do_print(std::ostream &out) const override;
113 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
114
115 [[nodiscard]] auto do_copy() const -> ULit override;
116
117 [[nodiscard]] auto do_hash() const -> size_t override;
118 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
119 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
120
121 UTerm lhs_;
122 UTerm rhs_;
123 Relation cmp_;
124};
125
127class LitExternal : public Lit {
128 public:
130 LitExternal(ScriptCallback &ctx, Location loc, String name, UTerm lhs, UTermVec args)
131 : ctx_{&ctx}, loc_{std::move(loc)}, name_{name}, lhs_{std::move(lhs)}, args_{std::move(args)} {}
132
133 private:
134 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
135 [[nodiscard]] auto do_domain() const -> bool override;
136 [[nodiscard]] auto do_single_pass() const -> bool override;
137 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
138 std::vector<bool> const &bound)
139 -> std::pair<UMatcher, std::optional<size_t>> override;
140 [[nodiscard]] auto do_score(std::vector<bool> const &bound) const -> double override;
141
142 void do_print(std::ostream &out) const override;
143 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
144
145 [[nodiscard]] auto do_copy() const -> ULit override;
146
147 [[nodiscard]] auto do_hash() const -> size_t override;
148 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
149 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
150
151 ScriptCallback *ctx_;
152 Location loc_;
153 String name_;
154 UTerm lhs_;
155 UTermVec args_;
156};
157
159class LitInterval : public Lit {
160 public:
162 LitInterval(UTerm lhs, UTerm lower, UTerm upper)
163 : lhs_{std::move(lhs)}, lower_{std::move(lower)}, upper_{std::move(upper)} {}
164
165 private:
166 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
167 [[nodiscard]] auto do_domain() const -> bool override;
168 [[nodiscard]] auto do_single_pass() const -> bool override;
169 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
170 std::vector<bool> const &bound)
171 -> std::pair<UMatcher, std::optional<size_t>> override;
172 [[nodiscard]] auto do_score(std::vector<bool> const &bound) const -> double override;
173
174 void do_print(std::ostream &out) const override;
175 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
176
177 [[nodiscard]] auto do_copy() const -> ULit override;
178
179 [[nodiscard]] auto do_hash() const -> size_t override;
180 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
181 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
182
183 UTerm lhs_;
184 UTerm lower_;
185 UTerm upper_;
186};
187
189constexpr auto stratified_index = std::numeric_limits<size_t>::max();
190
192class LitSymbolic : public Lit {
193 public:
195 LitSymbolic(AtomBase &base, Sign sign, UTerm atom, size_t index, bool domain)
196 : base_{&base}, atom_{std::move(atom)}, index_{index}, sign_{sign}, domain_{domain} {}
197
198 private:
199 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
200 [[nodiscard]] auto do_domain() const -> bool override;
201 [[nodiscard]] auto do_single_pass() const -> bool override;
202 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
203 std::vector<bool> const &bound)
204 -> std::pair<UMatcher, std::optional<size_t>> override;
205 [[nodiscard]] auto do_score(std::vector<bool> const &bound) const -> double override;
206
207 void do_print(std::ostream &out) const override;
208 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
209
210 [[nodiscard]] auto do_copy() const -> ULit override;
211
212 [[nodiscard]] auto do_hash() const -> size_t override;
213 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
214 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
215
216 AtomBase *base_;
217 UTerm atom_;
221 size_t index_;
222 size_t offset_ = 0;
223 Symbol symbol_;
224 Sign sign_;
226 bool domain_;
227};
228
231using AtomSimple = std::optional<std::tuple<Ground::UTerm, AtomBase &, std::vector<size_t>>>;
232
236class LitProject : public Lit {
237 public:
239 LitProject(ProjectState &state, Sign sign, UTerm atom, UTerm p_atom, size_t index, bool domain)
240 : state_{&state}, atom_{std::move(atom)}, p_atom_{std::move(p_atom)}, index_{index}, sign_{sign},
241 domain_{domain} {}
242
243 private:
244 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
245 [[nodiscard]] auto do_domain() const -> bool override;
246 [[nodiscard]] auto do_single_pass() const -> bool override;
247 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
248 std::vector<bool> const &bound)
249 -> std::pair<UMatcher, std::optional<size_t>> override;
250 [[nodiscard]] auto do_score(std::vector<bool> const &bound) const -> double override;
251 void do_print(std::ostream &out) const override;
252 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
253
254 [[nodiscard]] auto do_copy() const -> ULit override;
255
256 [[nodiscard]] auto do_hash() const -> size_t override;
257 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
258 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
259
260 ProjectState *state_;
261 UTerm atom_;
262 UTerm p_atom_;
263 size_t index_;
264 size_t offset_ = 0;
265 Symbol symbol_;
266 Sign sign_;
267 bool domain_;
268};
269
271class LitTuple : public Lit {
272 public:
274 LitTuple(VariableVec vars, SymbolVec &syms) : vars_{std::move(vars)}, syms_{&syms} {
275 assert(vars_.size() == syms_->size());
276 }
277
278 private:
279 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
280 [[nodiscard]] auto do_domain() const -> bool override;
281 [[nodiscard]] auto do_single_pass() const -> bool override;
282 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
283 std::vector<bool> const &bound)
284 -> std::pair<UMatcher, std::optional<size_t>> override;
285 [[nodiscard]] auto do_score([[maybe_unused]] std::vector<bool> const &bound) const -> double override;
286 void do_print(std::ostream &out) const override;
287 auto do_output([[maybe_unused]] EvalContext const &ctx, OutputLit &out) const -> bool override;
288 [[nodiscard]] auto do_copy() const -> ULit override;
289 [[nodiscard]] auto do_hash() const -> size_t override;
290 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
291 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
292
293 VariableVec vars_;
294 SymbolVec *syms_;
295};
296
298class LitCheck : public Lit {
299 private:
300 [[nodiscard]] virtual auto do_check(EvalContext const &ctx) -> bool = 0;
301
302 [[nodiscard]] auto do_domain() const -> bool override;
303 [[nodiscard]] auto do_single_pass() const -> bool override;
304 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
305 std::vector<bool> const &bound)
306 -> std::pair<UMatcher, std::optional<size_t>> override;
307 [[nodiscard]] auto do_score(std::vector<bool> const &bound) const -> double override;
308
309 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
310
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
317class LitBool : public LitCheck {
318 public:
320 LitBool(bool value) : value_{value} {}
321
322 private:
323 [[nodiscard]] auto do_check(EvalContext const &ctx) -> bool override;
324 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
325 void do_print(std::ostream &out) const override;
326 [[nodiscard]] auto do_copy() const -> ULit override;
327
328 bool value_;
329};
330
334class LitFactCheck : public LitCheck {
335 public:
337 LitFactCheck(AtomBase &base, Term const &atom, Symbol &target) : base_{&base}, atom_{&atom}, target_{&target} {}
338
339 private:
340 [[nodiscard]] auto do_check(EvalContext const &ctx) -> bool override;
341 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
342 void do_print(std::ostream &out) const override;
343 [[nodiscard]] auto do_copy() const -> ULit override;
344
345 AtomBase *base_;
346 Term const *atom_;
347 Symbol *target_;
348};
349
351class LitFailCheck : public LitCheck {
352 public:
357 LitFailCheck(UTermVec terms) : terms_{std::move(terms)} {}
358
359 private:
360 [[nodiscard]] auto do_check(EvalContext const &ctx) -> bool override;
361 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
362 void do_print(std::ostream &out) const override;
363 [[nodiscard]] auto do_copy() const -> ULit override;
364
365 UTermVec terms_;
366};
367
372using BaseVec = std::vector<std::tuple<std::tuple<String, size_t, bool>, AtomBase *, std::vector<size_t>>>;
373
375class LitSimpleAggr : public Lit {
376 public:
378 LitSimpleAggr(UTerm lhs, Relation cmp, AggregateFunction fun, std::vector<UTermVec> tuples)
379 : lhs_{std::move(lhs)}, tuples_{std::move(tuples)}, fun_{fun}, cmp_{cmp} {}
380
381 private:
382 void do_vars(VariableSet &vars, VarSelectMode mode) const override;
383 [[nodiscard]] auto do_domain() const -> bool override;
384 [[nodiscard]] auto do_single_pass() const -> bool override;
385 [[nodiscard]] auto do_matcher(std::pmr::monotonic_buffer_resource &mbr, MatcherType type,
386 std::vector<bool> const &bound)
387 -> std::pair<UMatcher, std::optional<size_t>> override;
388 [[nodiscard]] auto do_score(std::vector<bool> const &bound) const -> double override;
389
390 void do_print(std::ostream &out) const override;
391 auto do_output(EvalContext const &ctx, OutputLit &out) const -> bool override;
392
393 [[nodiscard]] auto do_copy() const -> ULit override;
394
395 [[nodiscard]] auto do_hash() const -> size_t override;
396 [[nodiscard]] auto do_equal_to(Lit const &other) const -> bool override;
397 [[nodiscard]] auto do_compare_to(Lit const &other) const -> std::weak_ordering override;
398
399 UTerm lhs_;
400 std::vector<UTermVec> tuples_;
401 AggregateFunction fun_;
402 Relation cmp_;
403};
404
406
407} // namespace CppClingo::Ground
CppClingo::Ground::AtomBase
An atom base used to store derivable atoms and associated state.
Definition base.hh:212
CppClingo::Ground::EvalContext
Context object to capture state used during instantiation.
Definition instantiator.hh:35
CppClingo::Ground::LitBool
A literal representing a Boolean.
Definition literal.hh:317
CppClingo::Ground::LitBool::LitBool
LitBool(bool value)
Construct the literal.
Definition literal.hh:320
CppClingo::Ground::LitCheck
A literal ensuring that a list of terms evaluates.
Definition literal.hh:298
CppClingo::Ground::LitComparison
A literal representing a comparison.
Definition literal.hh:98
CppClingo::Ground::LitComparison::LitComparison
LitComparison(UTerm lhs, Relation cmp, UTerm rhs)
Construct the literal.
Definition literal.hh:101
CppClingo::Ground::LitExternal
A literal representing a comparison.
Definition literal.hh:127
CppClingo::Ground::LitExternal::LitExternal
LitExternal(ScriptCallback &ctx, Location loc, String name, UTerm lhs, UTermVec args)
Construct the literal.
Definition literal.hh:130
CppClingo::Ground::LitFactCheck
Simple literal that discards whenever it matches to a fact.
Definition literal.hh:334
CppClingo::Ground::LitFactCheck::LitFactCheck
LitFactCheck(AtomBase &base, Term const &atom, Symbol &target)
Construct the literal.
Definition literal.hh:337
CppClingo::Ground::LitFailCheck
A literal ensuring that a list of terms evaluates.
Definition literal.hh:351
CppClingo::Ground::LitFailCheck::LitFailCheck
LitFailCheck(UTermVec terms)
Construct the literal.
Definition literal.hh:357
CppClingo::Ground::LitInterval
A literal representing an interval assignment.
Definition literal.hh:159
CppClingo::Ground::LitInterval::LitInterval
LitInterval(UTerm lhs, UTerm lower, UTerm upper)
Construct the literal.
Definition literal.hh:162
CppClingo::Ground::LitProject
A literal similar to a symbolic literal.
Definition literal.hh:236
CppClingo::Ground::LitProject::LitProject
LitProject(ProjectState &state, Sign sign, UTerm atom, UTerm p_atom, size_t index, bool domain)
Construct the literal.
Definition literal.hh:239
CppClingo::Ground::LitSimpleAggr
An aggregate literal without conditions.
Definition literal.hh:375
CppClingo::Ground::LitSimpleAggr::LitSimpleAggr
LitSimpleAggr(UTerm lhs, Relation cmp, AggregateFunction fun, std::vector< UTermVec > tuples)
Construct the literal.
Definition literal.hh:378
CppClingo::Ground::LitSymbolic
A symbolic literal.
Definition literal.hh:192
CppClingo::Ground::LitSymbolic::LitSymbolic
LitSymbolic(AtomBase &base, Sign sign, UTerm atom, size_t index, bool domain)
Construct the literal.
Definition literal.hh:195
CppClingo::Ground::LitTuple
An auxiliary literal binding variables to the given symbols upon first match.
Definition literal.hh:271
CppClingo::Ground::LitTuple::LitTuple
LitTuple(VariableVec vars, SymbolVec &syms)
Construct the literal.
Definition literal.hh:274
CppClingo::Ground::Lit
The base class for groundable literals.
Definition literal.hh:34
CppClingo::Ground::Lit::vars
void vars(VariableSet &vars, VarSelectMode mode) const
Get the variables in the predicate.
Definition literal.hh:40
CppClingo::Ground::Lit::copy
auto copy() const -> ULit
Copy the literal.
Definition literal.hh:66
CppClingo::Ground::Lit::~Lit
virtual ~Lit()=default
Destroy the literal.
CppClingo::Ground::Lit::score
auto score(std::vector< bool > const &bound) const -> double
Compute a score used to order rule bodies.
Definition literal.hh:57
CppClingo::Ground::Lit::domain
auto domain() const -> bool
Returns true if matching literals are always fact.
Definition literal.hh:46
CppClingo::Ground::Lit::operator<<
friend auto operator<<(std::ostream &out, Lit const &lit) -> std::ostream &
Print the literal.
Definition literal.hh:76
CppClingo::Ground::Lit::output
auto output(EvalContext const &ctx, OutputLit &out) const -> bool
Output the literal.
Definition literal.hh:63
CppClingo::Ground::Lit::hash
auto hash() const -> size_t
Compute a hash for the literal.
Definition literal.hh:69
CppClingo::Ground::Lit::operator==
friend auto operator==(Lit const &a, Lit const &b) -> bool
Compare two literals.
Definition literal.hh:72
CppClingo::Ground::Lit::matcher
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
CppClingo::Ground::Lit::operator<=>
friend auto operator<=>(Lit const &a, Lit const &b) -> std::weak_ordering
Compare two literals.
Definition literal.hh:74
CppClingo::Ground::Lit::single_pass
auto single_pass() const -> bool
Returns true if the literal can be grounded in a single pass.
Definition literal.hh:50
CppClingo::Ground::ProjectState
The state capturing the base of a projection.
Definition base.hh:368
CppClingo::Ground::ScriptCallback
Interface to call functions during parsing/grounding.
Definition script.hh:28
CppClingo::Ground::Term
Term interface.
Definition term.hh:67
CppClingo::Location
The Location of an expression in an input source.
Definition location.hh:44
CppClingo::OutputLit
Interface to output literals.
Definition output.hh:61
CppClingo::String
Reference to a string stored in a symbol store.
Definition symbol.hh:18
CppClingo::Symbol
Variant-like class to store symbols stored in a symbol store.
Definition symbol.hh:225
CppClingo::SymbolVec
std::vector< Symbol > SymbolVec
A vector of symbols.
Definition symbol.hh:220
CppClingo::Relation
Relation
Enumeration of supported relations.
Definition core.hh:35
CppClingo::Sign
Sign
Enumeration of signs (default negation).
Definition core.hh:16
CppClingo::AggregateFunction
AggregateFunction
Enumeration of aggregate functions.
Definition core.hh:87
CppClingo::AggregateFunction::max
@ max
The #min function.
CppClingo::Ground::VariableVec
VariableSet::values_container_type VariableVec
A vector of variables.
Definition base.hh:21
CppClingo::Ground::VariableSet
Util::ordered_set< size_t > VariableSet
A set of variables.
Definition base.hh:19
CppClingo::Ground::LitCondLitType::lit
@ lit
Conditional literals derived during grounding.
CppClingo::Ground::MatcherType
MatcherType
Enumeration of matcher types.
Definition instantiator.hh:48
CppClingo::Ground::UMatcher
std::unique_ptr< Matcher > UMatcher
A unique pointer to a matcher.
Definition instantiator.hh:100
CppClingo::Ground::ULit
std::unique_ptr< Lit > ULit
A unique pointer holding a literal.
Definition literal.hh:29
CppClingo::Ground::AtomSimple
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:231
CppClingo::Ground::VarSelectMode
VarSelectMode
Available variable selection modes.
Definition literal.hh:21
CppClingo::Ground::BaseVec
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
CppClingo::Ground::ULitVec
std::vector< ULit > ULitVec
A vector of literals.
Definition literal.hh:31
CppClingo::Ground::stratified_index
constexpr auto stratified_index
Marker for stratified literals.
Definition literal.hh:189
CppClingo::Ground::VarSelectMode::depend
@ depend
Get variables a literal depends on.
CppClingo::Ground::VarSelectMode::all
@ all
Get all variables in a literal.
CppClingo::Ground::VarSelectMode::provide
@ provide
Get variables provided by a literal.
CppClingo::Ground::UTerm
std::unique_ptr< Term > UTerm
A unique pointer holding a term.
Definition term.hh:33
CppClingo::Ground::UTermVec
std::vector< UTerm > UTermVec
A vector of terms.
Definition term.hh:35