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_TERMS_HH
26 #define _GRINGO_TERMS_HH
27
28 #include <gringo/base.hh>
29 #include <gringo/term.hh>
30 #include <gringo/hash_set.hh>
31 #include <potassco/theory_data.h>
32 #include <gringo/logger.hh>
33 #include <functional>
34
35 namespace Gringo {
36
37 using StringVec = std::vector<String>;
38 template <class T>
39 struct GetName {
40 using result_type = String;
operator ()Gringo::GetName41 String operator()(T const &x) const {
42 return x.name();
43 }
44 };
45
46 // {{{1 TheoryOpDef
47
48 class TheoryOpDef {
49 public:
50 using Key = std::pair<String, bool>;
51 struct GetKey {
operator ()Gringo::TheoryOpDef::GetKey52 Key operator()(TheoryOpDef const &x) const {
53 return x.key();
54 }
55 };
56 public:
57 TheoryOpDef(Location const &loc, String op, unsigned priority, TheoryOperatorType type);
58 TheoryOpDef(TheoryOpDef &&);
59 ~TheoryOpDef() noexcept;
60 TheoryOpDef &operator=(TheoryOpDef &&);
61 String op() const;
62 Key key() const;
63 Location const &loc() const;
64 void print(std::ostream &out) const;
65 unsigned priority() const;
66 TheoryOperatorType type() const;
67 private:
68 Location loc_;
69 String op_;
70 unsigned priority_;
71 TheoryOperatorType type_;
72 };
73 using TheoryOpDefs = UniqueVec<TheoryOpDef, HashKey<TheoryOpDef::Key, TheoryOpDef::GetKey, value_hash<TheoryOpDef::Key>>, EqualToKey<TheoryOpDef::Key, TheoryOpDef::GetKey>>;
operator <<(std::ostream & out,TheoryOpDef const & def)74 inline std::ostream &operator<<(std::ostream &out, TheoryOpDef const &def) {
75 def.print(out);
76 return out;
77 }
78
79 // {{{1 TheoryTermDef
80
81 class TheoryTermDef {
82 public:
83 TheoryTermDef(Location const &loc, String name);
84 TheoryTermDef(TheoryTermDef &&);
85 ~TheoryTermDef() noexcept;
86 TheoryTermDef &operator=(TheoryTermDef &&);
87 void addOpDef(TheoryOpDef &&def, Logger &log);
88 String name() const;
89 Location const &loc() const;
90 void print(std::ostream &out) const;
91 // returns (priority, flag) where flag is true if the binary operator is left associative
92 std::pair<unsigned, bool> getPrioAndAssoc(String op) const;
93 unsigned getPrio(String op, bool unary) const;
94 bool hasOp(String op, bool unary) const;
95 private:
96 Location loc_;
97 String name_;
98 TheoryOpDefs opDefs_;
99 };
100 using TheoryTermDefs = UniqueVec<TheoryTermDef, HashKey<String, GetName<TheoryTermDef>>, EqualToKey<String, GetName<TheoryTermDef>>>;
operator <<(std::ostream & out,TheoryTermDef const & def)101 inline std::ostream &operator<<(std::ostream &out, TheoryTermDef const &def) {
102 def.print(out);
103 return out;
104 }
105
106 // {{{1 TheoryAtomDef
107
108 class TheoryAtomDef {
109 public:
110 using Key = Sig;
111 struct GetKey {
operator ()Gringo::TheoryAtomDef::GetKey112 Key operator()(TheoryAtomDef const &x) const {
113 return x.sig();
114 }
115 };
116 public:
117 TheoryAtomDef(Location const &loc, String name, unsigned arity, String elemDef, TheoryAtomType type);
118 TheoryAtomDef(Location const &loc, String name, unsigned arity, String elemDef, TheoryAtomType type, StringVec &&ops, String guardDef);
119 TheoryAtomDef(TheoryAtomDef &&);
120 ~TheoryAtomDef() noexcept;
121 TheoryAtomDef &operator=(TheoryAtomDef &&);
122 Sig sig() const;
123 bool hasGuard() const;
124 TheoryAtomType type() const;
125 StringVec const &ops() const;
126 Location const &loc() const;
127 String elemDef() const;
128 String guardDef() const;
129 void print(std::ostream &out) const;
130 private:
131 Location loc_;
132 Sig sig_;
133 String elemDef_;
134 String guardDef_;
135 StringVec ops_;
136 TheoryAtomType type_;
137 };
138 using TheoryAtomDefs = UniqueVec<TheoryAtomDef, HashKey<TheoryAtomDef::Key, TheoryAtomDef::GetKey, value_hash<TheoryAtomDef::Key>>, EqualToKey<TheoryAtomDef::Key, TheoryAtomDef::GetKey>>;
operator <<(std::ostream & out,TheoryAtomDef const & def)139 inline std::ostream &operator<<(std::ostream &out, TheoryAtomDef const &def) {
140 def.print(out);
141 return out;
142 }
143
144 // {{{1 TheoryDef
145
146 class TheoryDef {
147 public:
148 TheoryDef(Location const &loc, String name);
149 TheoryDef(TheoryDef &&);
150 ~TheoryDef() noexcept;
151 TheoryDef &operator=(TheoryDef &&);
152 String name() const;
153 void addAtomDef(TheoryAtomDef &&def, Logger &log);
154 void addTermDef(TheoryTermDef &&def, Logger &log);
155 TheoryAtomDef const *getAtomDef(Sig name) const;
156 TheoryTermDef const *getTermDef(String name) const;
157 TheoryAtomDefs const &atomDefs() const;
158 Location const &loc() const;
159 void print(std::ostream &out) const;
160 private:
161 Location loc_;
162 TheoryTermDefs termDefs_;
163 TheoryAtomDefs atomDefs_;
164 String name_;
165 };
166 using TheoryDefs = UniqueVec<TheoryDef, HashKey<String, GetName<TheoryDef>>, EqualToKey<String, GetName<TheoryDef>>>;
operator <<(std::ostream & out,TheoryDef const & def)167 inline std::ostream &operator<<(std::ostream &out, TheoryDef const &def) {
168 def.print(out);
169 return out;
170 }
171 // }}}1
172
173 // {{{1 declaration of CSPMulTerm
174
175 struct CSPMulTerm {
176 CSPMulTerm(UTerm &&var, UTerm &&coe);
177 CSPMulTerm(CSPMulTerm &&x);
178 CSPMulTerm &operator=(CSPMulTerm &&x);
179 void collect(VarTermBoundVec &vars) const;
180 void collect(VarTermSet &vars) const;
181 void replace(Defines &x);
182 bool operator==(CSPMulTerm const &x) const;
183 bool simplify(SimplifyState &state, Logger &log);
184 void rewriteArithmetics(Term::ArithmeticsMap &arith, AuxGen &auxGen);
185 size_t hash() const;
186 bool hasPool() const;
187 std::vector<CSPMulTerm> unpool() const;
188 ~CSPMulTerm();
189
190 UTerm var;
191 UTerm coe;
192 };
193
194 std::ostream &operator<<(std::ostream &out, CSPMulTerm const &x);
195
196 template <>
197 struct clone<CSPMulTerm> {
198 CSPMulTerm operator()(CSPMulTerm const &x) const;
199 };
200
201 // {{{1 declaration of CSPAddTerm
202
203 using CSPGroundAdd = std::vector<std::pair<int,Symbol>>;
204 using CSPGroundLit = std::tuple<Relation, CSPGroundAdd, int>;
205
206 struct CSPAddTerm {
207 using Terms = std::vector<CSPMulTerm>;
208
209 CSPAddTerm(CSPMulTerm &&x);
210 CSPAddTerm(CSPAddTerm &&x);
211 CSPAddTerm(Terms &&terms);
212 CSPAddTerm &operator=(CSPAddTerm &&x);
213 void append(CSPMulTerm &&x);
214 bool simplify(SimplifyState &state, Logger &log);
215 void collect(VarTermBoundVec &vars) const;
216 void collect(VarTermSet &vars) const;
217 void replace(Defines &x);
218 bool operator==(CSPAddTerm const &x) const;
219 void rewriteArithmetics(Term::ArithmeticsMap &arith, AuxGen &auxGen);
220 std::vector<CSPAddTerm> unpool() const;
221 size_t hash() const;
222 bool hasPool() const;
223 void toGround(CSPGroundLit &ground, bool invert, Logger &log) const;
224 bool checkEval(Logger &log) const;
225 ~CSPAddTerm();
226
227 Terms terms;
228 };
229
230 std::ostream &operator<<(std::ostream &out, CSPAddTerm const &x);
231
232 template <>
233 struct clone<CSPAddTerm> {
234 CSPAddTerm operator()(CSPAddTerm const &x) const;
235 };
236
237 // {{{1 declaration of CSPRelTerm
238
239 struct CSPRelTerm {
240 CSPRelTerm(CSPRelTerm &&x);
241 CSPRelTerm(Relation rel, CSPAddTerm &&x);
242 CSPRelTerm &operator=(CSPRelTerm &&x);
243 void collect(VarTermBoundVec &vars) const;
244 void collect(VarTermSet &vars) const;
245 void replace(Defines &x);
246 bool operator==(CSPRelTerm const &x) const;
247 bool simplify(SimplifyState &state, Logger &log);
248 void rewriteArithmetics(Term::ArithmeticsMap &arith, AuxGen &auxGen);
249 size_t hash() const;
250 bool hasPool() const;
251 std::vector<CSPRelTerm> unpool() const;
252 ~CSPRelTerm();
253
254 Relation rel;
255 CSPAddTerm term;
256 };
257
258 std::ostream &operator<<(std::ostream &out, CSPRelTerm const &x);
259
260 template <>
261 struct clone<CSPRelTerm> {
262 CSPRelTerm operator()(CSPRelTerm const &x) const;
263 };
264
265 // }}}1
266
267 } // namespace Gringo
268
269 GRINGO_CALL_HASH(Gringo::CSPRelTerm)
270 GRINGO_CALL_HASH(Gringo::CSPMulTerm)
271 GRINGO_CALL_HASH(Gringo::CSPAddTerm)
272
273 #endif // _GRINGO_TERMS_HH
274