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_BASE_HH
26 #define _GRINGO_BASE_HH
27
28 #include <cassert>
29 #include <gringo/term.hh>
30 #include <deque>
31
32 namespace Gringo {
33
34 // {{{1 declaration of Context
35
36 class Context {
37 public:
38 virtual bool callable(String name) = 0;
39 virtual SymVec call(Location const &loc, String name, SymSpan args, Logger &log) = 0;
40 virtual void exec(String type, Location loc, String code) = 0;
41 virtual ~Context() noexcept = default;
42 };
43
44 // {{{1 declaration of TheoryAtomType
45
46 enum class TheoryAtomType { Head, Body, Any, Directive };
47 std::ostream &operator<<(std::ostream &out, TheoryAtomType type);
48
49 // {{{1 declaration of TheoryOperatorType
50
51 enum class TheoryOperatorType { Unary, BinaryLeft, BinaryRight };
52 std::ostream &operator<<(std::ostream &out, TheoryOperatorType type);
53
54 // {{{1 declaration of NAF
55
56 enum class NAF { POS = 0, NOT = 1, NOTNOT = 2 };
57 std::ostream &operator<<(std::ostream &out, NAF naf);
58 NAF inv(NAF naf, bool recursive = true);
59
60 enum class RECNAF { POS, NOT, NOTNOT, RECNOT };
61 RECNAF recnaf(NAF naf, bool recursive);
62 std::ostream &operator<<(std::ostream &out, RECNAF naf);
63
64 // {{{1 declaration of Relation
65
66 enum class Relation : unsigned { GT, LT, LEQ, GEQ, NEQ, EQ };
67
68 Relation inv(Relation rel);
69 Relation neg(Relation rel);
70
71 std::ostream &operator<<(std::ostream &out, Relation rel);
72
73 // {{{1 declaration of AggregateFunction
74
75 enum class AggregateFunction { COUNT, SUM, SUMP, MIN, MAX };
76
77 std::ostream &operator<<(std::ostream &out, AggregateFunction fun);
78
79 // {{{1 declaration of Bound
80
81 struct Bound;
82 typedef std::vector<Bound> BoundVec;
83
84 struct Bound {
85 Bound(Relation rel, UTerm &&bound);
86 Bound(Bound &&bound) noexcept;
87 Bound& operator=(Bound &&) noexcept;
88 size_t hash() const;
89 bool operator==(Bound const &other) const;
90 //! Unpool the terms in the bound.
91 BoundVec unpool();
92 //! Simplify the terms in the bound.
93 //! \pre Must be called after unpool.
94 bool simplify(SimplifyState &state, Logger &log);
95 //! Rewrite arithmetics.
96 //! \pre Must be called after assignLevels.
97 void rewriteArithmetics(Term::ArithmeticsMap &arith, AuxGen &auxGen);
98
99 Relation rel;
100 UTerm bound;
101 };
102
103 // }}}1
104
105 // {{{1 definition of TheoryAtomType
106
operator <<(std::ostream & out,TheoryAtomType type)107 inline std::ostream &operator<<(std::ostream &out, TheoryAtomType type) {
108 switch (type) {
109 case TheoryAtomType::Head: { out << "head"; break; }
110 case TheoryAtomType::Body: { out << "body"; break; }
111 case TheoryAtomType::Any: { out << "any"; break; }
112 case TheoryAtomType::Directive: { out << "directive"; break; }
113 }
114 return out;
115 }
116
117 // {{{1 definition of TheoryOperatorType
118
operator <<(std::ostream & out,TheoryOperatorType type)119 inline std::ostream &operator<<(std::ostream &out, TheoryOperatorType type) {
120 switch (type) {
121 case TheoryOperatorType::Unary: { out << "unary"; break; }
122 case TheoryOperatorType::BinaryLeft: { out << "binary,left"; break; }
123 case TheoryOperatorType::BinaryRight: { out << "binary,right"; break; }
124 }
125 return out;
126 }
127
128 // {{{1 definition of NAF
129
inv(NAF naf,bool recursive)130 inline NAF inv(NAF naf, bool recursive) {
131 switch (naf) {
132 case NAF::NOTNOT: { return NAF::NOT; }
133 case NAF::NOT: { return recursive ? NAF::NOTNOT : NAF::POS; }
134 case NAF::POS: { return NAF::NOT; }
135 }
136 assert(false);
137 return NAF::POS;
138 }
139
operator <<(std::ostream & out,NAF naf)140 inline std::ostream &operator<<(std::ostream &out, NAF naf) {
141 switch (naf) {
142 case NAF::NOTNOT: { out << "not "; }
143 case NAF::NOT: { out << "not "; }
144 case NAF::POS: { }
145 }
146 return out;
147 }
148
operator <<(std::ostream & out,RECNAF naf)149 inline std::ostream &operator<<(std::ostream &out, RECNAF naf) {
150 switch (naf) {
151 case RECNAF::NOTNOT: { out << "not "; }
152 case RECNAF::RECNOT:
153 case RECNAF::NOT: { out << "not "; }
154 case RECNAF::POS: { }
155 }
156 return out;
157 }
158
recnaf(NAF naf,bool recursive)159 inline RECNAF recnaf(NAF naf, bool recursive) {
160 switch (naf) {
161 case NAF::POS: { return RECNAF::POS; }
162 case NAF::NOT: { return recursive ? RECNAF::RECNOT : RECNAF::NOT; }
163 case NAF::NOTNOT: { return recursive ? RECNAF::NOTNOT : RECNAF::POS; }
164 }
165 return RECNAF::POS;
166 }
167
168 // {{{1 definition of Relation
169
operator <<(std::ostream & out,Relation rel)170 inline std::ostream &operator<<(std::ostream &out, Relation rel) {
171 switch (rel) {
172 case Relation::GT: { out << ">"; break; }
173 case Relation::LT: { out << "<"; break; }
174 case Relation::LEQ: { out << "<="; break; }
175 case Relation::GEQ: { out << ">="; break; }
176 case Relation::NEQ: { out << "!="; break; }
177 case Relation::EQ: { out << "="; break; }
178 }
179 return out;
180 }
181
inv(Relation rel)182 inline Relation inv(Relation rel) {
183 switch (rel) {
184 case Relation::NEQ: { return Relation::NEQ; }
185 case Relation::GEQ: { return Relation::LEQ; }
186 case Relation::LEQ: { return Relation::GEQ; }
187 case Relation::EQ: { return Relation::EQ; }
188 case Relation::LT: { return Relation::GT; }
189 case Relation::GT: { return Relation::LT; }
190 }
191 assert(false);
192 return Relation(-1);
193 }
194
neg(Relation rel)195 inline Relation neg(Relation rel) {
196 switch (rel) {
197 case Relation::NEQ: { return Relation::EQ; }
198 case Relation::GEQ: { return Relation::LT; }
199 case Relation::LEQ: { return Relation::GT; }
200 case Relation::EQ: { return Relation::NEQ; }
201 case Relation::LT: { return Relation::GEQ; }
202 case Relation::GT: { return Relation::LEQ; }
203 }
204 assert(false);
205 return Relation(-1);
206 }
207
208 // {{{1 definition of AggregateFunction
209
operator <<(std::ostream & out,AggregateFunction fun)210 inline std::ostream &operator<<(std::ostream &out, AggregateFunction fun) {
211 switch (fun) {
212 case AggregateFunction::MIN: { out << "#min"; break; }
213 case AggregateFunction::MAX: { out << "#max"; break; }
214 case AggregateFunction::SUM: { out << "#sum"; break; }
215 case AggregateFunction::SUMP: { out << "#sum+"; break; }
216 case AggregateFunction::COUNT: { out << "#count"; break; }
217 }
218 return out;
219 }
220
221 // {{{1 definition of Bound
222
Bound(Relation rel,UTerm && bound)223 inline Bound::Bound(Relation rel, UTerm &&bound)
224 : rel(rel)
225 , bound(std::move(bound)) { }
226
hash() const227 inline size_t Bound::hash() const {
228 return get_value_hash(size_t(rel), bound);
229 }
230
operator ==(Bound const & other) const231 inline bool Bound::operator==(Bound const &other) const {
232 return rel == other.rel && is_value_equal_to(bound, other.bound);
233 }
234
235 inline Bound::Bound(Bound &&) noexcept = default;
236
237 inline Bound& Bound::operator=(Bound &&) noexcept = default;
238
unpool()239 inline BoundVec Bound::unpool() {
240 BoundVec pool;
241 auto f = [&](UTerm &&x) { pool.emplace_back(rel, std::move(x)); };
242 Term::unpool(bound, Gringo::unpool, f);
243 return pool;
244 }
245
simplify(SimplifyState & state,Logger & log)246 inline bool Bound::simplify(SimplifyState &state, Logger &log) {
247 return !bound->simplify(state, false, false, log).update(bound, false).undefined();
248 }
249
rewriteArithmetics(Term::ArithmeticsMap & arith,AuxGen & auxGen)250 inline void Bound::rewriteArithmetics(Term::ArithmeticsMap &arith, AuxGen &auxGen) {
251 // NOTE: this replaces all arithmetics to ensure that all terms in bounds are defined when evaluating
252 Term::replace(bound, bound->rewriteArithmetics(arith, auxGen, true));
253 }
254
255 template <>
256 struct clone<Bound> {
operator ()Gringo::clone257 Bound operator()(Bound const &bound) const {
258 return Bound(bound.rel, get_clone(bound.bound));
259 }
260 };
261
262 // }}}1
263
264 } // namespace Gringo
265
266 namespace std {
267
268 // {{{1 definition of hash<Gringo::Bound>
269
270 template <>
271 struct hash<Gringo::Bound> {
operator ()std::hash272 size_t operator()(Gringo::Bound const &x) const { return x.hash(); }
273 };
274
275 // {{{1 definition of hash<Gringo::Relation>
276
277 template <>
278 struct hash<Gringo::Relation> {
operator ()std::hash279 size_t operator()(Gringo::Relation const &x) const { return static_cast<unsigned>(x); }
280 };
281
282 // {{{1 definition of hash<Gringo::NAF>
283
284 template <>
285 struct hash<Gringo::NAF> {
operator ()std::hash286 size_t operator()(Gringo::NAF const &x) const { return static_cast<unsigned>(x); }
287 };
288
289 // }}}1
290
291 } // namespace std
292
293 #endif // _GRINGO_BASE_HH
294
295