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