1 // {{{ MIT License
2
3 // Copyright 2017 Roland Kaminski
4
5 // Permission is hereby granted, free of charge, to any person obtaining a copy
6 // of this software and associated documentation files (the "Software"), to
7 // deal in the Software without restriction, including without limitation the
8 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
9 // sell copies of the Software, and to permit persons to whom the Software is
10 // furnished to do so, subject to the following conditions:
11
12 // The above copyright notice and this permission notice shall be included in
13 // all copies or substantial portions of the Software.
14
15 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
20 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
21 // IN THE SOFTWARE.
22
23 // }}}
24
25 #ifndef _GRINGO_TERM_HH
26 #define _GRINGO_TERM_HH
27
28 #include <gringo/bug.hh>
29 #include <gringo/symbol.hh>
30 #include <gringo/printable.hh>
31 #include <gringo/hashable.hh>
32 #include <gringo/locatable.hh>
33 #include <gringo/comparable.hh>
34 #include <gringo/clonable.hh>
35 #include <gringo/utility.hh>
36 #include <gringo/logger.hh>
37 #include <memory>
38 #include <unordered_set>
39 #ifdef _MSC_VER
40 #pragma warning( push )
41 #pragma warning( disable : 4503 ) // decorated name length exceeded
42 #pragma warning( disable : 4521 ) // multiple copy constructors specified
43 #endif
44 namespace Gringo {
45
46 // {{{ declaration of UnOp and BinOp
47
48 enum class BinOp : int { XOR, OR, AND, ADD, SUB, MUL, DIV, MOD, POW };
49 enum class UnOp : int { NEG, NOT, ABS };
50
51 int eval(UnOp op, int x);
52 int eval(BinOp op, int x, int y);
53
54 std::ostream &operator<<(std::ostream &out, BinOp op);
55 std::ostream &operator<<(std::ostream &out, UnOp op);
56
57 // }}}
58
59 // {{{ declaration of Defines
60
61 struct Term;
62 using UTerm = std::unique_ptr<Term>;
63 class Defines {
64 public:
65 using DefMap = std::unordered_map<String, std::tuple<bool, Location, UTerm>>;
66
67 Defines();
68 Defines(Defines &&x);
69 //! Add a define.
70 //! Default defintions will not overwrite existing definitions and can be overwritten by other defines.
71 void add(Location const &loc, String name, UTerm &&value, bool defaultDef, Logger &log);
72 //! Evaluates layered definitions and checks for cycles.
73 void init(Logger &log);
74 bool empty() const;
75 void apply(Symbol x, Symbol &retVal, UTerm &retTerm, bool replace);
76 DefMap const &defs() const;
77 ~Defines();
78
79 private:
80 std::unordered_map<String, std::tuple<bool, Location, UTerm>> defs_;
81 };
82
83 // }}}
84
85 // {{{ declaration of GTerm
86
87 struct GRef;
88 struct GTerm;
89 struct GVarTerm;
90 struct GFunctionTerm;
91 struct GLinearTerm;
92 using UGTerm = std::unique_ptr<GTerm>;
93 using UGFunTerm = std::unique_ptr<GFunctionTerm>;
94 struct GTerm : Clonable<GTerm>, Printable, Hashable, Comparable<GTerm> {
95 using EvalResult = std::pair<bool, Symbol>;
96 virtual Sig sig() const = 0;
97 virtual EvalResult eval() const = 0;
98 virtual bool occurs(GRef &x) const = 0;
99 virtual void reset() = 0;
100 virtual bool match(Symbol const &x) = 0;
101 virtual bool unify(GTerm &x) = 0;
102 virtual bool unify(GFunctionTerm &x) = 0;
103 virtual bool unify(GLinearTerm &x) = 0;
104 virtual bool unify(GVarTerm &x) = 0;
~GTermGringo::GTerm105 virtual ~GTerm() { }
106 };
107 using UGTermVec = std::vector<UGTerm>;
108 using SGRef = std::shared_ptr<GRef>;
109
110 // }}}
111 // {{{ declaration of Term
112
113 struct LinearTerm;
114 struct VarTerm;
115 struct ValTerm;
116 using UTermVec = std::vector<UTerm>;
117 using UTermVecVec = std::vector<UTermVec>;
118 using VarTermVec = std::vector<std::reference_wrapper<VarTerm>>;
119 using VarTermBoundVec = std::vector<std::pair<VarTerm*,bool>>;
120 using VarTermSet = std::unordered_set<std::reference_wrapper<VarTerm>, value_hash<std::reference_wrapper<VarTerm>>, value_equal_to<std::reference_wrapper<VarTerm>>>;
121
122 struct AuxGen {
AuxGenGringo::AuxGen123 AuxGen()
124 : auxNum(std::make_shared<unsigned>(0)) { }
125 AuxGen(AuxGen const &) = default;
126 AuxGen(AuxGen &&) = default;
127 String uniqueName(char const *prefix);
128 UTerm uniqueVar(Location const &loc, unsigned level, const char *prefix);
129
130 std::shared_ptr<unsigned> auxNum;
131 };
132
133 struct SimplifyState {
134 //! Somewhat complex result type of simplify.
135 struct SimplifyRet;
136
137 //! Type that stores for each rewritten DotsTerm the associated variable and the lower and upper bound.
138 using DotsMap = std::vector<std::tuple<UTerm, UTerm, UTerm>>;
139 using ScriptMap = std::vector<std::tuple<UTerm, String, UTermVec>>;
SimplifyStateGringo::SimplifyState140 SimplifyState(SimplifyState &state)
141 : gen(state.gen)
142 , level(state.level + 1) { }
SimplifyStateGringo::SimplifyState143 SimplifyState() : level(0) { }
144 SimplifyState(SimplifyState const &) = delete;
145 SimplifyState(SimplifyState &&) = default;
146
147 std::unique_ptr<LinearTerm> createDots(Location const &loc, UTerm &&left, UTerm &&right);
148 SimplifyRet createScript(Location const &loc, String name, UTermVec &&args, bool arith);
149
150 DotsMap dots;
151 ScriptMap scripts;
152 AuxGen gen;
153 int level;
154 };
155
156 struct Term : public Printable, public Hashable, public Locatable, public Comparable<Term>, public Clonable<Term> {
157 //! Return value of Term::project (replace, projected, project).
158 //! replace: projected variables are stripped, null if untouched
159 //! projected: term with variables renamed, projected if null
160 //! project: term with variables renamed, never null
161 using ProjectRet = std::tuple<UTerm, UTerm, UTerm>;
162 using SVal = std::shared_ptr<Symbol>;
163 using VarSet = std::unordered_set<String>;
164 using RenameMap = std::unordered_map<String, std::pair<String, SVal>>;
165 using ReferenceMap = std::unordered_map<Term*, SGRef, value_hash<Term*>, value_equal_to<Term*>>;
166 using SimplifyRet = SimplifyState::SimplifyRet;
167 //! Type that stores for each rewritten arithmetic term (UnopTerm, BinopTerm, LuaTerm) the associated variable and the term itself.
168 //! The indices of the vector correspond to the level of the term.
169 using LevelMap = std::unordered_map<UTerm, UTerm, value_hash<UTerm>, value_equal_to<UTerm>>;
170 using ArithmeticsMap = std::vector<std::unique_ptr<LevelMap>>;
171 //! The invertibility of a term. This may either be
172 //! - CONSTANT for terms that do not contain variables,
173 //! - INVERTIBLE for invertible terms (e.g. -X, 1+X, f(X,Y+Z))
174 //! - NOT_INVERTIBLE for terms that are not invertible (e.g. arithmetic operations with two unknowns)
175 enum Invertibility { CONSTANT = 0, INVERTIBLE = 1, NOT_INVERTIBLE = 2 };
176 //! Whether the term contains a VarTerm.
177 virtual bool hasVar() const = 0;
178 virtual unsigned projectScore() const = 0;
179 //! Rename the outermost term.
180 //! \pre the term must either be a function term or value term holding an identifier.
181 //! \note unnecessary; can be deleted
182 virtual void rename(String name) = 0;
183 //! Removes all occurrences of PoolTerm instances.
184 //! Returns all unpooled incarnations of the term.
185 //! \note The term becomes unusable after the method returns.
186 //! \post The pool does not contain PoolTerm instances.
187 virtual void unpool(UTermVec &x) const = 0;
188 //! Removes all occurrences of DotsTerm instances, simplifies the term and sets the invertibility.
189 //! To reduce the number of cases in later algorithms moves invertible terms to the left:
190 //! - 1+X -> X+1
191 //! - (1+(1-X)) -> ((-X)+1)+1
192 //! Replaces undefined arithmetic operations with 0:
193 //! - f(X)+0 -> 0
194 //! \note The term is unusable if the method returned a non-zero replacement term.
195 //! \pre Must be called after unpool.
196 virtual SimplifyRet simplify(SimplifyState &state, bool positional, bool arithmetic, Logger &log) = 0;
197 //! Removes anonymous variables in projectable positions (in outermost function symbols) from a term.
198 //! The first element of the return value is a replacement term for the current term,
199 //! which might be null if the term does not have to be replace..
200 //! The second and third can be used to create a projection rule
201 //! where the second is the head and the third is the body element.
202 //! \pre Must be called after simplify.
203 //! \code{.cpp}
204 //! num = 0; sig = base; lit = q(X,_)
205 //! (lit', projected, project) = lit.project(&sig, num)
206 //! assert(lit' == #p_q(base,X,#p))
207 //! assert(projected == #p_q(base,#X1,#p))
208 //! assert(project == #p_q(base,#X1,#Y2))
209 //! \endcode
210 virtual ProjectRet project(bool rename, AuxGen &gen) = 0;
211 //! Obtain the type of a term.
212 //! \pre Must be called after simplify.
213 //! Whether evaluation of a term is guaranteed to not produce numeric values.
214 //! This means that the term is either a non-numeric constant or a function symbol.
215 virtual bool isNotNumeric() const = 0;
216 virtual bool isNotFunction() const = 0;
217 //! Obtain the invertibility of a term.
218 //! \pre Must be called after simplify.
219 virtual Invertibility getInvertibility() const = 0;
220 //! Evaluates the term to a value.
221 //! \pre Must be called after simplify.
222 virtual Symbol eval(bool &undefined, Logger &log) const = 0;
223 //! Returns true if the term evaluates to zero.
224 //! \pre Must be called after simplify.
225 //! \pre Term is ground or
226 bool isZero(Logger &log) const;
227 //! Collects variables in Terms.
228 //! \pre Must be called after simplify and project to properly account for bound variables.
229 // TODO: the way I am using these it would be nice to have a visitor for variables
230 // and implement the functions below using the visitor
231 virtual void collect(VarTermBoundVec &vars, bool bound) const = 0;
232 virtual void collect(VarTermSet &vars) const;
233 virtual void collect(VarSet &vars, unsigned minLevel = 0, unsigned maxLevel = std::numeric_limits<unsigned>::max()) const = 0;
234 virtual void collectIds(VarSet &vars) const = 0;
235 //! Returns the nesting level of a term.
236 //! That is the largest level of a nested variable or zero for ground terms.
237 //! \pre Must be called after assignLevel.
238 virtual unsigned getLevel() const = 0;
239 //! Removes non-invertible arithmetics.
240 //! \note The term is unusable if the method returned a non-zero replacement term.
241 //! \pre Must be called after assignLevel.
242 virtual UTerm rewriteArithmetics(ArithmeticsMap &arith, AuxGen &auxGen, bool forceDefined = false) = 0;
243 virtual bool match(Symbol const &val) const = 0;
244 bool bind(VarSet &bound);
245 virtual Sig getSig() const = 0;
246 virtual UTerm renameVars(RenameMap &names) const = 0;
247 SGRef _newRef(RenameMap &names, ReferenceMap &refs) const;
248 UGTerm gterm() const;
249 virtual UGFunTerm gfunterm(RenameMap &names, ReferenceMap &refs) const;
250 virtual bool hasPool() const = 0;
251 virtual UGTerm gterm(RenameMap &names, ReferenceMap &refs) const = 0;
252 virtual UTerm replace(Defines &defs, bool replace) = 0;
253 virtual double estimate(double size, VarSet const &bound) const = 0;
254 virtual Symbol isEDB() const = 0;
255 virtual int toNum(bool &undefined, Logger &log);
isAtomGringo::Term256 virtual bool isAtom() const { return false; }
257
~TermGringo::Term258 virtual ~Term() { }
259
260 //! Inserts a term into arith creating a new unique variable if necessary.
261 static UTerm insert(ArithmeticsMap &arith, AuxGen &auxGen, UTerm &&term, bool eq = false);
262
263 //! Set dst to src if src is non-zero.
264 template <class T, class U>
265 static void replace(std::unique_ptr<T> &dst, std::unique_ptr<U> &&src);
266 template <class T, class U, class V>
267 void replace(std::unique_ptr<T> &dst, std::unique_ptr<U> &&src, std::unique_ptr<V> &&alt);
268
269 //! Unpools a, calling g on each obtained element.
270 template <class A, class UnpoolA, class Callback>
271 static void unpool(A const &a, UnpoolA const &fA, Callback const &g);
272 //! Unpools a and b, calculates cross product, calling g on each obtained tuple.
273 template <class A, class B, class UnpoolA, class UnpoolB, class Callback>
274 static void unpool(A const &a, B const &b, UnpoolA const &fA, UnpoolB const &fB, Callback const &g);
275 //! Iterates of [begin, end] unpooling with f, calculates cross product, calling g on each obtained tuple.
276 template <class It, class Unpool, class Callback>
277 static void unpool(It const &begin, It const &end, Unpool const &f, Callback const &g);
278 //! Unpools each element of vec using f, and move the union of all pools back to f.
279 template <class Vec, class Unpool>
280 static void unpoolJoin(Vec &vec, Unpool const &f);
281 };
282
283 UTermVec unpool(UTerm const &x);
284
285 struct LinearTerm;
286 struct SimplifyState::SimplifyRet {
287 enum Type { UNTOUCHED, CONSTANT, LINEAR, REPLACE, UNDEFINED };
288 SimplifyRet(SimplifyRet const &) = delete;
289 SimplifyRet(SimplifyRet &&x);
290 //! Reference to untouched term.
291 SimplifyRet(Term &x, bool project);
292 //! Indicate replacement with linear term.
293 SimplifyRet(std::unique_ptr<LinearTerm> &&x);
294 //! Indicate replacement with arbitrary term.
295 SimplifyRet(UTerm &&x);
296 //! Indicate replacement with value.
297 SimplifyRet(Symbol const &x);
298 //! Indicate undefined term
299 SimplifyRet();
300 bool notNumeric() const;
301 bool notFunction() const;
302 bool constant() const;
303 bool isZero() const;
304 bool undefined() const;
305 LinearTerm &lin();
306 SimplifyRet &update(UTerm &x, bool arith);
307 ~SimplifyRet();
308 Type type;
309 bool project = false;
310 union {
311 Symbol val;
312 Term *term;
313 };
314 };
315
316 // }}}
317
318 // {{{ declaration of GRef
319
320 struct GRef {
321 enum Type { EMPTY, VALUE, TERM };
322 GRef(UTerm &&name);
323 operator bool() const;
324 void reset();
325 GRef &operator=(Symbol const &x);
326 GRef &operator=(GTerm &x);
327 bool occurs(GRef &x) const;
328 bool match(Symbol const &x);
329 template <class T>
330 bool unify(T &x);
331
332 Type type;
333 UTerm name;
334 // Note: these two could be put into a union
335 Symbol value;
336 GTerm *term;
337 };
338 using SGRef = std::shared_ptr<GRef>;
339
340 // }}}
341 // {{{ declaration of GValTerm
342
343 struct GValTerm : GTerm {
344 GValTerm(Symbol val);
345 virtual bool operator==(GTerm const &other) const;
346 virtual size_t hash() const;
347 virtual void print(std::ostream &out) const;
348 virtual Sig sig() const;
349 virtual EvalResult eval() const;
350 virtual bool occurs(GRef &x) const;
351 virtual void reset();
352 virtual bool match(Symbol const &x);
353 virtual bool unify(GTerm &x);
354 virtual bool unify(GFunctionTerm &x);
355 virtual bool unify(GLinearTerm &x);
356 virtual bool unify(GVarTerm &x);
cloneGringo::GValTerm357 virtual GValTerm *clone() const { return new GValTerm{val}; }
358 virtual ~GValTerm();
359
360 Symbol val;
361 };
362
363 // }}}
364 // {{{ declaration of GFunctionTerm
365
366 struct GFunctionTerm : GTerm {
367 GFunctionTerm(String name, UGTermVec &&args);
368 GFunctionTerm(GFunctionTerm const &x, bool sign);
369 virtual bool operator==(GTerm const &other) const;
370 virtual size_t hash() const;
371 virtual void print(std::ostream &out) const;
372 virtual Sig sig() const;
373 virtual EvalResult eval() const;
374 virtual bool occurs(GRef &x) const;
375 virtual void reset();
376 virtual bool match(Symbol const &x);
377 virtual bool unify(GTerm &x);
378 virtual bool unify(GFunctionTerm &x);
379 virtual bool unify(GLinearTerm &x);
380 virtual bool unify(GVarTerm &x);
cloneGringo::GFunctionTerm381 virtual GFunctionTerm *clone() const {
382 auto ret = new GFunctionTerm{name, get_clone(args)};
383 ret->sign = sign;
384 return ret;
385 }
386 virtual ~GFunctionTerm();
387
388 bool sign;
389 String name;
390 UGTermVec args;
391 };
392
393 // }}}
394 // {{{ declaration of GLinearTerm
395
396 struct GLinearTerm : GTerm {
397 GLinearTerm(SGRef ref, int m, int n);
398 virtual bool operator==(GTerm const &other) const;
399 virtual size_t hash() const;
400 virtual void print(std::ostream &out) const;
401 virtual Sig sig() const;
402 virtual EvalResult eval() const;
403 virtual bool occurs(GRef &x) const;
404 virtual void reset();
405 virtual bool match(Symbol const &x);
406 virtual bool unify(GTerm &x);
407 virtual bool unify(GFunctionTerm &x);
408 virtual bool unify(GLinearTerm &x);
409 virtual bool unify(GVarTerm &x);
cloneGringo::GLinearTerm410 virtual GLinearTerm *clone() const { return new GLinearTerm{ref, m, n}; }
411 virtual ~GLinearTerm();
412
413 SGRef ref;
414 int m;
415 int n;
416 };
417
418 // }}}
419 // {{{ declaration of GVarTerm
420
421 struct GVarTerm : GTerm {
422 GVarTerm(SGRef ref);
423 virtual bool operator==(GTerm const &other) const;
424 virtual size_t hash() const;
425 virtual void print(std::ostream &out) const;
426 virtual Sig sig() const;
427 virtual EvalResult eval() const;
428 virtual bool occurs(GRef &x) const;
429 virtual void reset();
430 virtual bool match(Symbol const &x);
431 virtual bool unify(GTerm &x);
432 virtual bool unify(GFunctionTerm &x);
433 virtual bool unify(GLinearTerm &x);
434 virtual bool unify(GVarTerm &x);
cloneGringo::GVarTerm435 virtual GVarTerm *clone() const { return new GVarTerm{ref}; }
436 virtual ~GVarTerm();
437
438 SGRef ref;
439 };
440
441 // }}}
442
443 // {{{ declaration of PoolTerm
444
445 struct PoolTerm : public Term {
446 PoolTerm(UTermVec &&terms);
447 virtual unsigned projectScore() const;
448 virtual void rename(String name);
449 virtual SimplifyRet simplify(SimplifyState &state, bool positional, bool arithmetic, Logger &log);
450 virtual ProjectRet project(bool rename, AuxGen &gen);
451 virtual bool hasVar() const;
452 virtual void collect(VarTermBoundVec &vars, bool bound) const;
453 virtual void collect(VarSet &vars, unsigned minLevel = 0, unsigned maxLevel = std::numeric_limits<unsigned>::max()) const;
454 virtual Symbol eval(bool &undefined, Logger &log) const;
455 virtual bool match(Symbol const &val) const;
456 virtual Sig getSig() const;
457 virtual UTerm renameVars(RenameMap &names) const;
458 virtual UGTerm gterm(RenameMap &names, ReferenceMap &refs) const;
459 virtual unsigned getLevel() const;
460 virtual bool isNotNumeric() const;
461 virtual bool isNotFunction() const;
462 virtual Invertibility getInvertibility() const;
463 virtual void print(std::ostream &out) const;
464 virtual void unpool(UTermVec &x) const;
465 virtual UTerm rewriteArithmetics(ArithmeticsMap &arith, AuxGen &auxGen, bool forceDefined);
466 virtual bool operator==(Term const &other) const;
467 virtual size_t hash() const;
468 virtual PoolTerm *clone() const;
469 virtual bool hasPool() const;
470 virtual void collectIds(VarSet &vars) const;
471 virtual UTerm replace(Defines &defs, bool replace = true);
472 virtual double estimate(double size, VarSet const &bound) const;
473 virtual Symbol isEDB() const;
474 virtual bool isAtom() const;
475 virtual ~PoolTerm();
476
477 UTermVec args;
478 };
479
480 // }}}
481 // {{{ declaration of ValTerm
482
483 struct ValTerm : public Term {
484 ValTerm(Symbol value);
485 virtual unsigned projectScore() const;
486 virtual void rename(String name);
487 virtual SimplifyRet simplify(SimplifyState &state, bool positional, bool arithmetic, Logger &log);
488 virtual ProjectRet project(bool rename, AuxGen &gen);
489 virtual bool hasVar() const;
490 virtual void collect(VarTermBoundVec &vars, bool bound) const;
491 virtual void collect(VarSet &vars, unsigned minLevel = 0, unsigned maxLevel = std::numeric_limits<unsigned>::max()) const;
492 virtual Symbol eval(bool &undefined, Logger &log) const;
493 virtual bool match(Symbol const &val) const;
494 virtual Sig getSig() const;
495 virtual UTerm renameVars(RenameMap &names) const;
496 virtual UGTerm gterm(RenameMap &names, ReferenceMap &refs) const;
497 virtual unsigned getLevel() const;
498 virtual bool isNotNumeric() const;
499 virtual bool isNotFunction() const;
500 virtual Invertibility getInvertibility() const;
501 virtual void print(std::ostream &out) const;
502 virtual void unpool(UTermVec &x) const;
503 virtual UTerm rewriteArithmetics(ArithmeticsMap &arith, AuxGen &auxGen, bool forceDefined);
504 virtual bool operator==(Term const &other) const;
505 virtual size_t hash() const;
506 virtual ValTerm *clone() const;
507 virtual bool hasPool() const;
508 virtual void collectIds(VarSet &vars) const;
509 virtual UTerm replace(Defines &defs, bool replace = true);
510 virtual double estimate(double size, VarSet const &bound) const;
511 virtual Symbol isEDB() const;
512 virtual bool isAtom() const;
513 virtual ~ValTerm();
514
515 Symbol value;
516 };
517
518 // }}}
519 // {{{ declaration of VarTerm
520
521 struct VarTerm : Term {
522 VarTerm(String name, SVal ref, unsigned level = 0, bool bindRef = false);
523 virtual unsigned projectScore() const;
524 virtual void rename(String name);
525 virtual SimplifyRet simplify(SimplifyState &state, bool positional, bool arithmetic, Logger &log);
526 virtual ProjectRet project(bool rename, AuxGen &gen);
527 virtual bool hasVar() const;
528 virtual void collect(VarTermBoundVec &vars, bool bound) const;
529 virtual void collect(VarSet &vars, unsigned minLevel = 0, unsigned maxLevel = std::numeric_limits<unsigned>::max()) const;
530 virtual Symbol eval(bool &undefined, Logger &log) const;
531 virtual bool match(Symbol const &val) const;
532 virtual Sig getSig() const;
533 virtual UTerm renameVars(RenameMap &names) const;
534 virtual UGTerm gterm(RenameMap &names, ReferenceMap &refs) const;
535 virtual unsigned getLevel() const;
536 virtual bool isNotNumeric() const;
537 virtual bool isNotFunction() const;
538 virtual Invertibility getInvertibility() const;
539 virtual void print(std::ostream &out) const;
540 virtual void unpool(UTermVec &x) const;
541 virtual UTerm rewriteArithmetics(ArithmeticsMap &arith, AuxGen &auxGen, bool forceDefined);
542 virtual bool operator==(Term const &other) const;
543 virtual size_t hash() const;
544 virtual VarTerm *clone() const;
545 virtual bool hasPool() const;
546 virtual void collectIds(VarSet &vars) const;
547 virtual UTerm replace(Defines &defs, bool replace = true);
548 virtual double estimate(double size, VarSet const &bound) const;
549 virtual Symbol isEDB() const;
550 virtual ~VarTerm();
551
552 String name;
553 SVal ref;
554 bool bindRef;
555 unsigned level;
556 };
557
558 // }}}
559 // {{{ declaration of UnOpTerm
560
561 struct UnOpTerm : public Term {
562 UnOpTerm(UnOp op, UTerm &&arg);
563 virtual unsigned projectScore() const;
564 virtual void rename(String name);
565 virtual SimplifyRet simplify(SimplifyState &state, bool positional, bool arithmetic, Logger &log);
566 virtual ProjectRet project(bool rename, AuxGen &gen);
567 virtual bool hasVar() const;
568 virtual void collect(VarTermBoundVec &vars, bool bound) const;
569 virtual void collect(VarSet &vars, unsigned minLevel = 0, unsigned maxLevel = std::numeric_limits<unsigned>::max()) const;
570 virtual Symbol eval(bool &undefined, Logger &log) const;
571 virtual bool match(Symbol const &val) const;
572 virtual Sig getSig() const;
573 virtual UTerm renameVars(RenameMap &names) const;
574 virtual UGTerm gterm(RenameMap &names, ReferenceMap &refs) const;
575 virtual UGFunTerm gfunterm(RenameMap &names, ReferenceMap &refs) const;
576 virtual unsigned getLevel() const;
577 virtual bool isNotNumeric() const;
578 virtual bool isNotFunction() const;
579 virtual Invertibility getInvertibility() const;
580 virtual void print(std::ostream &out) const;
581 virtual void unpool(UTermVec &x) const;
582 virtual UTerm rewriteArithmetics(ArithmeticsMap &arith, AuxGen &auxGen, bool forceDefined);
583 virtual bool operator==(Term const &other) const;
584 virtual size_t hash() const;
585 virtual UnOpTerm *clone() const;
586 virtual bool hasPool() const;
587 virtual void collectIds(VarSet &vars) const;
588 virtual UTerm replace(Defines &defs, bool replace = true);
589 virtual double estimate(double size, VarSet const &bound) const;
590 virtual Symbol isEDB() const;
591 virtual bool isAtom() const;
592 virtual ~UnOpTerm();
593
594 UnOp const op;
595 UTerm arg;
596 };
597
598 // }}}
599 // {{{ declaration of BinOpTerm
600
601 struct BinOpTerm : public Term {
602 BinOpTerm(BinOp op, UTerm &&left, UTerm &&right);
603 virtual unsigned projectScore() const;
604 virtual void rename(String name);
605 virtual SimplifyRet simplify(SimplifyState &state, bool positional, bool arithmetic, Logger &log);
606 virtual ProjectRet project(bool rename, AuxGen &gen);
607 virtual bool hasVar() const;
608 virtual void collect(VarTermBoundVec &vars, bool bound) const;
609 virtual void collect(VarSet &vars, unsigned minLevel = 0, unsigned maxLevel = std::numeric_limits<unsigned>::max()) const;
610 virtual Symbol eval(bool &undefined, Logger &log) const;
611 virtual bool match(Symbol const &val) const;
612 virtual Sig getSig() const;
613 virtual UTerm renameVars(RenameMap &names) const;
614 virtual UGTerm gterm(RenameMap &names, ReferenceMap &refs) const;
615 virtual unsigned getLevel() const;
616 virtual bool isNotNumeric() const;
617 virtual bool isNotFunction() const;
618 virtual Invertibility getInvertibility() const;
619 virtual void print(std::ostream &out) const;
620 virtual void unpool(UTermVec &x) const;
621 virtual UTerm rewriteArithmetics(ArithmeticsMap &arith, AuxGen &auxGen, bool forceDefined);
622 virtual bool operator==(Term const &other) const;
623 virtual size_t hash() const;
624 virtual BinOpTerm *clone() const;
625 virtual bool hasPool() const;
626 virtual void collectIds(VarSet &vars) const;
627 virtual UTerm replace(Defines &defs, bool replace = true);
628 virtual double estimate(double size, VarSet const &bound) const;
629 virtual Symbol isEDB() const;
630 virtual ~BinOpTerm();
631
632 BinOp op;
633 UTerm left;
634 UTerm right;
635 };
636
637 // }}}
638 // {{{ declaration of DotsTerm
639
640 struct DotsTerm : public Term {
641 DotsTerm(UTerm &&left, UTerm &&right);
642 virtual unsigned projectScore() const;
643 virtual void rename(String name);
644 virtual SimplifyRet simplify(SimplifyState &state, bool positional, bool arithmetic, Logger &log);
645 virtual ProjectRet project(bool rename, AuxGen &gen);
646 virtual bool hasVar() const;
647 virtual void collect(VarTermBoundVec &vars, bool bound) const;
648 virtual void collect(VarSet &vars, unsigned minLevel = 0, unsigned maxLevel = std::numeric_limits<unsigned>::max()) const;
649 virtual Symbol eval(bool &undefined, Logger &log) const;
650 virtual bool match(Symbol const &val) const;
651 virtual Sig getSig() const;
652 virtual UTerm renameVars(RenameMap &names) const;
653 virtual UGTerm gterm(RenameMap &names, ReferenceMap &refs) const;
654 virtual unsigned getLevel() const;
655 virtual bool isNotNumeric() const;
656 virtual bool isNotFunction() const;
657 virtual Invertibility getInvertibility() const;
658 virtual void print(std::ostream &out) const;
659 virtual void unpool(UTermVec &x) const;
660 virtual UTerm rewriteArithmetics(ArithmeticsMap &arith, AuxGen &auxGen, bool forceDefined);
661 virtual bool operator==(Term const &other) const;
662 virtual size_t hash() const;
663 virtual DotsTerm *clone() const;
664 virtual bool hasPool() const;
665 virtual void collectIds(VarSet &vars) const;
666 virtual UTerm replace(Defines &defs, bool replace = true);
667 virtual double estimate(double size, VarSet const &bound) const;
668 virtual Symbol isEDB() const;
669 virtual ~DotsTerm();
670
671 UTerm left;
672 UTerm right;
673 };
674
675 // }}}
676 // {{{ declaration of LuaTerm
677
678 struct LuaTerm : public Term {
679 LuaTerm(String name, UTermVec &&args);
680 virtual unsigned projectScore() const;
681 virtual void rename(String name);
682 virtual SimplifyRet simplify(SimplifyState &state, bool positional, bool arithmetic, Logger &log);
683 virtual ProjectRet project(bool rename, AuxGen &gen);
684 virtual bool hasVar() const;
685 virtual void collect(VarTermBoundVec &vars, bool bound) const;
686 virtual void collect(VarSet &vars, unsigned minLevel = 0, unsigned maxLevel = std::numeric_limits<unsigned>::max()) const;
687 virtual Symbol eval(bool &undefined, Logger &log) const;
688 virtual bool match(Symbol const &val) const;
689 virtual Sig getSig() const;
690 virtual UTerm renameVars(RenameMap &names) const;
691 virtual UGTerm gterm(RenameMap &names, ReferenceMap &refs) const;
692 virtual unsigned getLevel() const;
693 virtual bool isNotNumeric() const;
694 virtual bool isNotFunction() const;
695 virtual Invertibility getInvertibility() const;
696 virtual void print(std::ostream &out) const;
697 virtual void unpool(UTermVec &x) const;
698 virtual UTerm rewriteArithmetics(ArithmeticsMap &arith, AuxGen &auxGen, bool forceDefined);
699 virtual bool operator==(Term const &other) const;
700 virtual size_t hash() const;
701 virtual LuaTerm *clone() const;
702 virtual bool hasPool() const;
703 virtual void collectIds(VarSet &vars) const;
704 virtual UTerm replace(Defines &defs, bool replace = true);
705 virtual double estimate(double size, VarSet const &bound) const;
706 virtual Symbol isEDB() const;
707 virtual ~LuaTerm();
708
709 String const name;
710 UTermVec args;
711 };
712
713 // }}}
714 // {{{ declaration of FunctionTerm
715
716 struct FunctionTerm : public Term {
717 FunctionTerm(String name, UTermVec &&args);
718 virtual unsigned projectScore() const;
719 virtual void rename(String name);
720 virtual SimplifyRet simplify(SimplifyState &state, bool positional, bool arithmetic, Logger &log);
721 virtual ProjectRet project(bool rename, AuxGen &gen);
722 virtual bool hasVar() const;
723 virtual void collect(VarTermBoundVec &vars, bool bound) const;
724 virtual void collect(VarSet &vars, unsigned minLevel = 0, unsigned maxLevel = std::numeric_limits<unsigned>::max()) const;
725 virtual Symbol eval(bool &undefined, Logger &log) const;
726 virtual bool match(Symbol const &val) const;
727 virtual Sig getSig() const;
728 virtual UTerm renameVars(RenameMap &names) const;
729 virtual UGTerm gterm(RenameMap &names, ReferenceMap &refs) const;
730 virtual UGFunTerm gfunterm(RenameMap &names, ReferenceMap &refs) const;
731 virtual unsigned getLevel() const;
732 virtual bool isNotNumeric() const;
733 virtual bool isNotFunction() const;
734 virtual Invertibility getInvertibility() const;
735 virtual void print(std::ostream &out) const;
736 virtual void unpool(UTermVec &x) const;
737 virtual UTerm rewriteArithmetics(ArithmeticsMap &arith, AuxGen &auxGen, bool forceDefined);
738 virtual bool operator==(Term const &other) const;
739 virtual size_t hash() const;
740 virtual FunctionTerm *clone() const;
741 virtual bool hasPool() const;
742 virtual void collectIds(VarSet &vars) const;
743 virtual UTerm replace(Defines &defs, bool replace = true);
744 virtual double estimate(double size, VarSet const &bound) const;
745 virtual Symbol isEDB() const;
746 virtual bool isAtom() const;
747 virtual ~FunctionTerm();
748
749 String name;
750 UTermVec args;
751 mutable SymVec cache;
752 };
753
754 // }}}
755 // {{{ declaration of LinearTerm
756
757 // TODO: if it holds a var it can as well use its location
758 struct LinearTerm : Term {
759 using UVarTerm = std::unique_ptr<VarTerm>;
760 LinearTerm(VarTerm const &var, int m, int n);
761 LinearTerm(UVarTerm &&var, int m, int n);
762 virtual unsigned projectScore() const;
763 virtual void rename(String name);
764 virtual SimplifyRet simplify(SimplifyState &state, bool positional, bool arithmetic, Logger &log);
765 virtual ProjectRet project(bool rename, AuxGen &gen);
766 virtual bool hasVar() const;
767 virtual void collect(VarTermBoundVec &vars, bool bound) const;
768 virtual void collect(VarSet &vars, unsigned minLevel = 0, unsigned maxLevel = std::numeric_limits<unsigned>::max()) const;
769 virtual Symbol eval(bool &undefined, Logger &log) const;
770 virtual bool match(Symbol const &val) const;
771 virtual Sig getSig() const;
772 virtual UTerm renameVars(RenameMap &names) const;
773 virtual UGTerm gterm(RenameMap &names, ReferenceMap &refs) const;
774 virtual unsigned getLevel() const;
775 virtual bool isNotNumeric() const;
776 virtual bool isNotFunction() const;
777 virtual Invertibility getInvertibility() const;
778 virtual void print(std::ostream &out) const;
779 virtual void unpool(UTermVec &x) const;
780 virtual UTerm rewriteArithmetics(ArithmeticsMap &arith, AuxGen &auxGen, bool forceDefined);
781 virtual bool operator==(Term const &other) const;
782 virtual size_t hash() const;
783 virtual LinearTerm *clone() const;
784 virtual bool hasPool() const;
785 virtual void collectIds(VarSet &vars) const;
786 virtual UTerm replace(Defines &defs, bool replace = true);
787 virtual double estimate(double size, VarSet const &bound) const;
788 virtual Symbol isEDB() const;
789 virtual ~LinearTerm();
790
791 UVarTerm var;
792 int m;
793 int n;
794 };
795
796 // }}}
797
798 // {{{ definition of Term and auxiliary functions
799
800 // TODO: ugly
801
802 template <class T, class U>
replace(std::unique_ptr<T> & dst,std::unique_ptr<U> && src)803 void Term::replace(std::unique_ptr<T> &dst, std::unique_ptr<U> &&src) {
804 if (src) { dst = std::move(src); }
805 }
806
807 template <class A, class UnpoolA, class Callback>
unpool(A const & a,UnpoolA const & fA,Callback const & g)808 void Term::unpool(A const &a, UnpoolA const &fA, Callback const &g) {
809 for (auto &termA : fA(a)) { g(std::move(termA)); }
810 }
811
812 template <class A, class B, class UnpoolA, class UnpoolB, class Callback>
unpool(A const & a,B const & b,UnpoolA const & fA,UnpoolB const & fB,Callback const & g)813 void Term::unpool(A const &a, B const &b, UnpoolA const &fA, UnpoolB const &fB, Callback const &g) {
814 auto poolB(fB(b));
815 for (auto &termA : fA(a)) {
816 for (auto &termB : poolB) { g(get_clone(termA), get_clone(termB)); }
817 }
818 }
819
820 template <class It, class TermUnpool, class Callback>
unpool(It const & begin,It const & end,TermUnpool const & f,Callback const & g)821 void Term::unpool(It const &begin, It const &end, TermUnpool const &f, Callback const &g) {
822 using R = decltype(f(*begin));
823 std::vector<R> pools;
824 for (auto it = begin; it != end; ++it) { pools.emplace_back(f(*it)); }
825 cross_product(pools);
826 for (auto &pooled : pools) { g(std::move(pooled)); }
827 }
828
829 template <class Vec, class TermUnpool>
unpoolJoin(Vec & vec,TermUnpool const & f)830 void Term::unpoolJoin(Vec &vec, TermUnpool const &f) {
831 Vec join;
832 for (auto &x : vec) {
833 auto pool(f(x));
834 std::move(pool.begin(), pool.end(), std::back_inserter(join));
835 }
836 vec = std::move(join);
837 }
838
839 // }}}
840
841 } // namespace Gringo
842
843 GRINGO_HASH(Gringo::Term)
844 GRINGO_HASH(Gringo::VarTerm)
845 GRINGO_HASH(Gringo::GTerm)
846
847 #ifdef _MSC_VER
848 #pragma warning( pop )
849 #endif
850
851 #endif // _GRINGO_TERM_HH
852