Clingo
Loading...
Searching...
No Matches
term.hh
1#pragma once
2
3#include <clingo/ground/instantiator.hh>
4
5#include <clingo/core/core.hh>
6#include <clingo/core/location.hh>
7#include <clingo/core/logger.hh>
8#include <clingo/core/symbol.hh>
9
10#include <clingo/util/enum.hh>
11#include <clingo/util/ordered_set.hh>
12#include <clingo/util/unordered_map.hh>
13
14namespace CppClingo::Ground {
15
18
20using VariableSet = Util::ordered_set<size_t>;
22using VariableVec = VariableSet::values_container_type;
23
25enum class RenameMode : uint8_t {
26 rename_vars,
27 rename_projection,
28 drop_projection,
29};
30
31class Term;
33using UTerm = std::unique_ptr<Term>;
35using UTermVec = std::vector<UTerm>;
37using GuardVec = std::vector<std::pair<Relation, UTerm>>;
38
40template <class T>
41 requires requires(T x) {
42 { x.copy() } -> std::convertible_to<std::unique_ptr<T>>;
43 }
44auto copy_uvec(std::vector<std::unique_ptr<T>> const &vec) {
45 std::vector<std::unique_ptr<T>> res;
46 res.reserve(vec.size());
47 for (auto const &x : vec) {
48 res.emplace_back(x->copy());
49 }
50 return res;
51}
53template <class T>
54 requires requires(T x) {
55 { x.copy() } -> std::convertible_to<std::unique_ptr<T>>;
56 }
57auto copy_uvec(std::vector<std::vector<std::unique_ptr<T>>> const &vec) {
58 std::vector<std::vector<std::unique_ptr<T>>> res;
59 res.reserve(vec.size());
60 for (auto const &x : vec) {
61 res.emplace_back(copy_uvec(x));
62 }
63 return res;
64}
65
67class Term {
68 public:
70 using Key = Symbol;
71
73 virtual ~Term() = default;
75 [[nodiscard]] auto score(double size, std::vector<bool> const &bound) const -> double {
76 return do_score(size, bound);
77 }
82 [[nodiscard]] auto match(EvalContext const &ctx, Symbol sym) const -> bool { return do_match(ctx, sym); }
86 [[nodiscard]] auto eval(EvalContext const &ctx) const -> std::optional<Symbol> { return do_eval(ctx); }
91 [[nodiscard]] auto rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const -> UTerm {
92 return do_rename(store, mode, name, vars);
93 }
95 [[nodiscard]] auto rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm { return do_rename(vars); }
97 void vars(VariableSet &vars, bool provide = false) const { do_vars(vars, provide); }
99 [[nodiscard]] auto copy() const -> UTerm { return do_copy(); }
101 [[nodiscard]] auto hash() const -> size_t { return do_hash(); }
102
107 [[nodiscard]] auto signature(VariableSet const &bound, VariableSet const &bind) const
108 -> std::pair<UTerm, VariableVec> {
109 auto names = Util::unordered_map<size_t, size_t>{};
110 names.reserve(bind.size() + bound.size());
111 auto sig_term = rename(names);
112 auto sig_lookup = std::vector<size_t>{};
113 sig_lookup.reserve(bound.size());
114 for (auto const &var : bound) {
115 sig_lookup.emplace_back(names[var]);
116 }
117 return {std::move(sig_term), std::move(sig_lookup)};
118 }
120 [[nodiscard]] auto vars() const -> VariableSet {
121 VariableSet set;
122 vars(set);
123 return set;
124 }
125
127 friend auto operator==(Term const &a, Term const &b) -> bool { return a.do_equal_to(b); }
129 friend auto operator<=>(Term const &a, Term const &b) -> std::strong_ordering { return a.do_compare_to(b); }
131 friend auto operator<<(std::ostream &out, Term const &term) -> std::ostream & {
132 term.do_print(out);
133 return out;
134 }
135
136 private:
137 [[nodiscard]] virtual auto do_score(double size, std::vector<bool> const &bound) const -> double = 0;
138 [[nodiscard]] virtual auto do_match(EvalContext const &ctx, Symbol sym) const -> bool = 0;
139 [[nodiscard]] virtual auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> = 0;
140 [[nodiscard]] virtual auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
141 -> UTerm = 0;
142 [[nodiscard]] virtual auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm = 0;
143 virtual void do_vars(VariableSet &vars, bool provide) const = 0;
144 virtual void do_print(std::ostream &out) const = 0;
145 [[nodiscard]] virtual auto do_copy() const -> UTerm = 0;
146 [[nodiscard]] virtual auto do_hash() const -> size_t = 0;
147 [[nodiscard]] virtual auto do_equal_to(Term const &other) const -> bool = 0;
148 [[nodiscard]] virtual auto do_compare_to(Term const &other) const -> std::strong_ordering = 0;
149};
150
152class TermProjection : public Term {
153 public:
155 TermProjection() = default;
156
157 private:
158 [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
159 [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
160 [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
161 [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
162 -> UTerm override;
163 [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
164 void do_vars(VariableSet &vars, bool provide) const override;
165 void do_print(std::ostream &out) const override;
166 [[nodiscard]] auto do_copy() const -> UTerm override;
167 [[nodiscard]] auto do_hash() const -> size_t override;
168 [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
169 [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
170};
171
173class TermSymbol : public Term {
174 public:
176 TermSymbol(Symbol sym) : sym_{sym} {}
177
179 [[nodiscard]] auto symbol() const -> Symbol const & { return *sym_; }
180
181 private:
182 [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
183 [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
184 [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
185 [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
186 -> UTerm override;
187 [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
188 void do_vars(VariableSet &vars, bool provide) const override;
189 void do_print(std::ostream &out) const override;
190 [[nodiscard]] auto do_copy() const -> UTerm override;
191 [[nodiscard]] auto do_hash() const -> size_t override;
192 [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
193 [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
194
195 SharedSymbol sym_;
196};
197
199class TermVariable : public Term {
200 public:
202 TermVariable(size_t var) : var_{var} {}
203
204 private:
205 [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
206 [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
207 [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
208 [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
209 -> UTerm override;
210 [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
211 void do_vars(VariableSet &vars, bool provide) const override;
212 void do_print(std::ostream &out) const override;
213 [[nodiscard]] auto do_copy() const -> UTerm override;
214 [[nodiscard]] auto do_hash() const -> size_t override;
215 [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
216 [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
217
218 size_t var_;
219};
220
222class TermLinear : public Term {
223 public:
225 TermLinear(Location loc, Number m, size_t var, Number n)
226 : loc_{std::move(loc)}, m_{std::move(m)}, n_{std::move(n)}, var_{var} {}
227
228 private:
229 [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
230 [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
231 [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
232 [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
233 -> UTerm override;
234 [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
235 void do_vars(VariableSet &vars, bool provide) const override;
236 void do_print(std::ostream &out) const override;
237 [[nodiscard]] auto do_copy() const -> UTerm override;
238 [[nodiscard]] auto do_hash() const -> size_t override;
239 [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
240 [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
241
242 Location loc_;
243 Number m_;
244 Number n_;
245 size_t var_;
246 mutable bool logged_ = false;
247};
248
250enum class UnaryOperator : uint8_t {
251 minus = 0,
252 negate = 1,
253 abs = 2,
254};
255
257class TermUnary : public Term {
258 public:
260 TermUnary(UnaryOperator op, Location loc_rhs, UTerm rhs)
261 : loc_rhs_{std::move(loc_rhs)}, rhs_{std::move(rhs)}, op_{op} {}
262
263 private:
264 [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
265 [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
266 [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
267 [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
268 -> UTerm override;
269 [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
270 void do_vars(VariableSet &vars, bool provide) const override;
271 void do_print(std::ostream &out) const override;
272 [[nodiscard]] auto do_copy() const -> UTerm override;
273 [[nodiscard]] auto do_hash() const -> size_t override;
274 [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
275 [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
276
277 Location loc_rhs_;
278 UTerm rhs_;
279 UnaryOperator op_;
280 mutable bool logged_ = false;
281};
282
284enum class BinaryOperator : uint8_t {
285 and_,
286 div,
287 minus,
288 mod,
289 times,
290 or_,
291 plus,
292 pow,
293 xor_,
294};
295
297class TermBinary : public Term {
298 public:
300 TermBinary(Location loc_lhs, UTerm lhs, BinaryOperator op, Location loc_rhs, UTerm rhs)
301 : loc_lhs_{std::move(loc_lhs)}, loc_rhs_{std::move(loc_rhs)}, lhs_{std::move(lhs)}, rhs_{std::move(rhs)},
302 op_{op} {}
303
304 private:
305 [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
306 [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
307 [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
308 [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
309 -> UTerm override;
310 [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
311 void do_vars(VariableSet &vars, bool provide) const override;
312 void do_print(std::ostream &out) const override;
313 [[nodiscard]] auto do_copy() const -> UTerm override;
314 [[nodiscard]] auto do_hash() const -> size_t override;
315 [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
316 [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
317
318 Location loc_lhs_;
319 Location loc_rhs_;
320 UTerm lhs_;
321 UTerm rhs_;
322 BinaryOperator op_;
323 mutable bool logged_ = false;
324};
325
327class TermTuple : public Term {
328 public:
330 TermTuple(UTermVec args) : args_{std::move(args)} { eval_.reserve(args_.size()); }
331
332 private:
333 [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
334 [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
335 [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
336 [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
337 -> UTerm override;
338 [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
339 void do_vars(VariableSet &vars, bool provide) const override;
340 void do_print(std::ostream &out) const override;
341 [[nodiscard]] auto do_copy() const -> UTerm override;
342 [[nodiscard]] auto do_hash() const -> size_t override;
343 [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
344 [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
345
346 UTermVec args_;
347 std::vector<Symbol> mutable eval_;
348};
349
351class TermFunction : public Term {
352 public:
354 TermFunction(String name, UTermVec args) : name_{name}, args_{std::move(args)} { eval_.reserve(args_.size()); }
355
356 private:
357 [[nodiscard]] auto do_score(double size, std::vector<bool> const &bound) const -> double override;
358 [[nodiscard]] auto do_match(EvalContext const &ctx, Symbol sym) const -> bool override;
359 [[nodiscard]] auto do_eval(EvalContext const &ctx) const -> std::optional<Symbol> override;
360 [[nodiscard]] auto do_rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const
361 -> UTerm override;
362 [[nodiscard]] auto do_rename(Util::unordered_map<size_t, size_t> &vars) const -> UTerm override;
363 void do_vars(VariableSet &vars, bool provide) const override;
364 void do_print(std::ostream &out) const override;
365 [[nodiscard]] auto do_copy() const -> UTerm override;
366 [[nodiscard]] auto do_hash() const -> size_t override;
367 [[nodiscard]] auto do_equal_to(Term const &other) const -> bool override;
368 [[nodiscard]] auto do_compare_to(Term const &other) const -> std::strong_ordering override;
369
370 SharedString name_;
371 UTermVec args_;
372 std::vector<Symbol> mutable eval_;
373};
374
376template <class... T>
377inline auto expect(EvalContext const &ctx, Location const &loc, bool &logged, T &&...args) -> bool {
378 if (!logged && ctx.log().check(MessageCode::info_operation_undefined)) {
379 logged = true;
380 (CppClingo::Report(ctx.log(), MessageCode::info_operation_undefined, loc).out()
381 << ... << std::forward<T>(args));
382 }
383 return false;
384}
385
387
388} // namespace CppClingo::Ground
CppClingo::Ground::EvalContext
Context object to capture state used during instantiation.
Definition instantiator.hh:35
CppClingo::Ground::TermBinary
A term capturing a binary term.
Definition term.hh:297
CppClingo::Ground::TermBinary::TermBinary
TermBinary(Location loc_lhs, UTerm lhs, BinaryOperator op, Location loc_rhs, UTerm rhs)
Construct the term.
Definition term.hh:300
CppClingo::Ground::TermFunction
A term capturing a tuple.
Definition term.hh:351
CppClingo::Ground::TermFunction::TermFunction
TermFunction(String name, UTermVec args)
Construct the term.
Definition term.hh:354
CppClingo::Ground::TermLinear
A term capturing a linear term.
Definition term.hh:222
CppClingo::Ground::TermLinear::TermLinear
TermLinear(Location loc, Number m, size_t var, Number n)
Construct the term.
Definition term.hh:225
CppClingo::Ground::TermProjection
A term capturing a projection.
Definition term.hh:152
CppClingo::Ground::TermProjection::TermProjection
TermProjection()=default
Construct the term.
CppClingo::Ground::TermSymbol
A term capturing a symbol.
Definition term.hh:173
CppClingo::Ground::TermSymbol::symbol
auto symbol() const -> Symbol const &
Get the symbol of the term.
Definition term.hh:179
CppClingo::Ground::TermSymbol::TermSymbol
TermSymbol(Symbol sym)
Construct the term.
Definition term.hh:176
CppClingo::Ground::TermTuple
A term capturing a tuple.
Definition term.hh:327
CppClingo::Ground::TermTuple::TermTuple
TermTuple(UTermVec args)
Construct the term.
Definition term.hh:330
CppClingo::Ground::TermUnary
A term capturing a unary term.
Definition term.hh:257
CppClingo::Ground::TermUnary::TermUnary
TermUnary(UnaryOperator op, Location loc_rhs, UTerm rhs)
Construct the term.
Definition term.hh:260
CppClingo::Ground::TermVariable
A term capturing a variable.
Definition term.hh:199
CppClingo::Ground::TermVariable::TermVariable
TermVariable(size_t var)
Construct the term.
Definition term.hh:202
CppClingo::Ground::Term
Term interface.
Definition term.hh:67
CppClingo::Ground::Term::score
auto score(double size, std::vector< bool > const &bound) const -> double
Compute an estimate how often the term can match size symbols given the bound variables.
Definition term.hh:75
CppClingo::Ground::Term::signature
auto signature(VariableSet const &bound, VariableSet const &bind) const -> std::pair< UTerm, VariableVec >
Compute a signature of the term.
Definition term.hh:107
CppClingo::Ground::Term::eval
auto eval(EvalContext const &ctx) const -> std::optional< Symbol >
Evaluates a term w.r.t.
Definition term.hh:86
CppClingo::Ground::Term::operator<<
friend auto operator<<(std::ostream &out, Term const &term) -> std::ostream &
Print the term.
Definition term.hh:131
CppClingo::Ground::Term::copy
auto copy() const -> UTerm
Create a copy of the term.
Definition term.hh:99
CppClingo::Ground::Term::vars
auto vars() const -> VariableSet
Collect all variables in the term.
Definition term.hh:120
CppClingo::Ground::Term::~Term
virtual ~Term()=default
Destructor.
CppClingo::Ground::Term::match
auto match(EvalContext const &ctx, Symbol sym) const -> bool
Match a term with the given symbol.
Definition term.hh:82
CppClingo::Ground::Term::rename
auto rename(SymbolStore &store, RenameMode mode, String const *name, size_t *vars) const -> UTerm
Create a copy of the term renaming/replacing parts of it.
Definition term.hh:91
CppClingo::Ground::Term::vars
void vars(VariableSet &vars, bool provide=false) const
Collect all variables in the term.
Definition term.hh:97
CppClingo::Ground::Term::operator==
friend auto operator==(Term const &a, Term const &b) -> bool
Compare two terms.
Definition term.hh:127
CppClingo::Ground::Term::hash
auto hash() const -> size_t
Compute a hash for the term.
Definition term.hh:101
CppClingo::Ground::Term::rename
auto rename(Util::unordered_map< size_t, size_t > &vars) const -> UTerm
Create a copy of the term renaming variables in order of occurrence.
Definition term.hh:95
CppClingo::Ground::Term::operator<=>
friend auto operator<=>(Term const &a, Term const &b) -> std::strong_ordering
Compare two terms.
Definition term.hh:129
CppClingo::Location
The Location of an expression in an input source.
Definition location.hh:44
CppClingo::Number
An arbitrary precision integer.
Definition number.hh:27
CppClingo::Report
Helper class to ease logging.
Definition logger.hh:106
CppClingo::Report::out
auto out() -> std::ostringstream &
Get message sink.
Definition logger.hh:117
CppClingo::SharedString
Class managing the lifetime of a String.
Definition symbol.hh:93
CppClingo::SharedSymbol
Class managing the lifetime of a Symbol.
Definition symbol.hh:306
CppClingo::String
Reference to a string stored in a symbol store.
Definition symbol.hh:18
CppClingo::SymbolStore
A store for symbols.
Definition symbol.hh:454
CppClingo::Symbol
Variant-like class to store symbols stored in a symbol store.
Definition symbol.hh:225
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::VarSelectMode::provide
@ provide
Get variables provided by a literal.
CppClingo::Ground::copy_uvec
auto copy_uvec(std::vector< std::unique_ptr< T > > const &vec)
Helper to copy vectors with copyable elements.
Definition term.hh:44
CppClingo::Ground::GuardVec
std::vector< std::pair< Relation, UTerm > > GuardVec
A vector of guards.
Definition term.hh:37
CppClingo::Ground::BinaryOperator
BinaryOperator
Available binary operations.
Definition term.hh:284
CppClingo::Ground::UTerm
std::unique_ptr< Term > UTerm
A unique pointer holding a term.
Definition term.hh:33
CppClingo::Ground::UnaryOperator
UnaryOperator
Available unary operations.
Definition term.hh:250
CppClingo::Ground::RenameMode
RenameMode
Modes determining how to handle variables in terms.
Definition term.hh:25
CppClingo::Ground::UTermVec
std::vector< UTerm > UTermVec
A vector of terms.
Definition term.hh:35
CppClingo::Ground::UnaryOperator::negate
@ negate
The bitwise negation operation.
CppClingo::Ground::UnaryOperator::minus
@ minus
The unary arithmetic minus operation.
CppClingo::Ground::UnaryOperator::abs
@ abs
The arithmetic absolute operation.
CppClingo::Ground::RenameMode::rename_vars
@ rename_vars
Successively rename variables in order of traversal.
CppClingo::Ground::RenameMode::drop_projection
@ drop_projection
Drop projections from tuples and functions.
CppClingo::Ground::RenameMode::rename_projection
@ rename_projection
Successively introduce variables for projections in order of traversal.
CppClingo::Util::unordered_map
tsl::hopscotch_map< Key, T, Hash, KeyEqual, Allocator, NeighborhoodSize, StoreHash, GrowthPolicy > unordered_map
Alias for unordered maps.
Definition unordered_map.hh:17