1
2 /*
3 * File Formula.hpp.
4 *
5 * This file is part of the source code of the software program
6 * Vampire. It is protected by applicable
7 * copyright laws.
8 *
9 * This source code is distributed under the licence found here
10 * https://vprover.github.io/license.html
11 * and in the source directory
12 *
13 * In summary, you are allowed to use Vampire for non-commercial
14 * purposes but not allowed to distribute, modify, copy, create derivatives,
15 * or use in competitions.
16 * For other uses of Vampire please contact developers for a different
17 * licence, which we will make an effort to provide.
18 */
19 /**
20 * @file Formula.hpp
21 * Defines class Formula.
22 *
23 * @since 02/12/2003, Manchester, allocation changed to use Allocator
24 * @since 06/05/2007, Manchester, change to use new kind of Term and Literal
25 */
26
27 #ifndef __Formula__
28 #define __Formula__
29
30 #include <utility>
31
32 #include "Forwards.hpp"
33
34 #include "Lib/Environment.hpp"
35 #include "Lib/List.hpp"
36 #include "Lib/XML.hpp"
37
38 #include "Kernel/Signature.hpp"
39
40 #include "Connective.hpp"
41 #include "Term.hpp"
42
43
44 namespace Kernel {
45
46 using namespace Lib;
47
48 class Formula
49 {
50 public:
51 typedef List<int> VarList;
52 typedef List<unsigned> SortList;
53 /**
54 * Constructor of constant formulas (true/false)
55 * @since 02/07/2007 Manchester
56 */
Formula(bool value)57 explicit Formula (bool value)
58 : _connective(value ? TRUE : FALSE)
59 {
60 } // Formula::Formula (bool value)
61
62 // structure
63 /** Return the connective */
connective() const64 Connective connective () const { return _connective; }
65
66 const FormulaList* args() const;
67 FormulaList* args();
68 FormulaList** argsPtr();
69 const Formula* left() const;
70 Formula* left();
71 const Formula* right() const;
72 Formula* right();
73 const Formula* qarg() const;
74 Formula* qarg();
75 const VarList* vars() const;
76 VarList* vars();
77 const SortList* sorts() const;
78 SortList* sorts();
79 const Formula* uarg() const;
80 Formula* uarg();
81 const Literal* literal() const;
82 Literal* literal();
83 const TermList getBooleanTerm() const;
84 TermList getBooleanTerm();
85 VarList* freeVariables () const;
86 VarList* boundVariables () const;
87
88 // miscellaneous
89 bool equals(const Formula*) const;
90 void collectAtoms(Stack<Literal*>& acc);
91 void collectPredicates(Stack<unsigned>& acc);
92 void collectPredicatesWithPolarity(Stack<pair<unsigned,int> >& acc, int polarity=1);
93
94 XMLElement toXML() const;
95
96 // output
97 vstring toString() const;
98 vstring toStringInScopeOf(Connective con) const;
99 static vstring toString(Connective con);
100 bool parenthesesRequired(Connective outer) const;
101 // auxiliary functions
102 void destroy();
103
104 unsigned weight() const;
105
106 Color getColor();
107 bool getSkip();
108
109 static Formula* fromClause(Clause* cl);
110
111 static Formula* quantify(Formula* f);
112
113 static Formula* trueFormula();
114 static Formula* falseFormula();
115
116 static Formula* createITE(Formula* condition, Formula* thenArg, Formula* elseArg);
117 static Formula* createLet(unsigned functor, Formula::VarList* variables, TermList body, Formula* contents);
118 static Formula* createLet(unsigned predicate, Formula::VarList* variables, Formula* body, Formula* contents);
119
120 // use allocator to (de)allocate objects of this class
121 CLASS_NAME(Formula);
122 USE_ALLOCATOR(Formula);
123 protected:
124 static vstring toString(const Formula* f);
125
126 /** Create a dummy formula will null content */
Formula(Connective con)127 explicit Formula(Connective con)
128 : _connective(con)
129 {}
130
131 /** connective */
132 Connective _connective;
133 // auxiliary functions
134 static vstring _connectiveNames[];
135 }; // class Formula
136
137 /**
138 * Named formulas
139 * @since 04/12/2015
140 */
141 class NamedFormula
142 : public Formula
143 {
144 public:
NamedFormula(vstring name)145 explicit NamedFormula(vstring name) : Formula(NAME), _name(name) {}
146
147 CLASS_NAME(NamedFormula);
148 USE_ALLOCATOR(NamedFormula);
149
name()150 vstring name(){ return _name; }
name() const151 const vstring name() const { return _name;}
152
153 protected:
154 vstring _name;
155
156 }; // class NamedFormula
157
158 /**
159 * Atomic formulas.
160 * @since 02/06/2007 Manchester
161 */
162 class AtomicFormula
163 : public Formula
164 {
165 public:
166 /** building atomic formula from a literal */
AtomicFormula(Literal * lit)167 explicit AtomicFormula (Literal* lit)
168 : Formula(LITERAL),
169 _literal(lit)
170 {}
171 /** Return the literal of this formula */
getLiteral() const172 const Literal* getLiteral() const { return _literal; }
173 /** Return the literal of this formula */
getLiteral()174 Literal* getLiteral() { return _literal; }
175
176 // use allocator to (de)allocate objects of this class
177 CLASS_NAME(AtomicFormula);
178 USE_ALLOCATOR(AtomicFormula);
179 protected:
180 /** The literal of this formula */
181 Literal* _literal;
182 }; // class AtomicFormula
183
184
185 /**
186 * Quantified formulas.
187 * @since 02/06/2007 Manchester
188 */
189 class QuantifiedFormula
190 : public Formula
191 {
192 public:
193 /** Build a quantified formula */
QuantifiedFormula(Connective con,VarList * vs,SortList * ss,Formula * arg)194 QuantifiedFormula(Connective con, VarList* vs, SortList* ss, Formula* arg)
195 : Formula(con),
196 _vars(vs),
197 _sorts(ss),
198 _arg(arg)
199 {
200 ASS(con == FORALL || con == EXISTS);
201 ASS(vs);
202 ASS(!ss || VarList::length(vs) == SortList::length(ss));
203 }
204
205 /** Return the immediate subformula */
subformula() const206 const Formula* subformula () const { return _arg; }
207 /** Return the immediate subformula */
subformula()208 Formula* subformula () { return _arg; }
209 /** Return the list of variables */
varList() const210 const VarList* varList() const { return _vars; }
211 /** Return the list of variables */
varList()212 VarList* varList() { return _vars; }
213 /** Return the list of sorts */
sortList() const214 const SortList* sortList() const { return _sorts; }
215 /** Return the list of sorts */
sortList()216 SortList* sortList() { return _sorts; }
217
218 // use allocator to (de)allocate objects of this class
219 CLASS_NAME(QuantifiedFormula);
220 USE_ALLOCATOR(QuantifiedFormula);
221 protected:
222 /** list of variables */
223 VarList* _vars;
224 /** list of sorts */
225 SortList* _sorts;
226 /** argument */
227 Formula* _arg;
228 }; // class Formula::QuantifiedData
229
230 /**
231 * Negated formula.
232 * @since 02/06/2007 Manchester
233 */
234 class NegatedFormula
235 : public Formula
236 {
237 public:
238 /** building a negated formula */
NegatedFormula(Formula * f)239 explicit NegatedFormula (Formula* f)
240 : Formula(NOT),
241 _arg(f)
242 {}
243
244 /** Return the immediate subformula of this formula */
subformula() const245 const Formula* subformula() const { return _arg; }
246 /** Return the immediate subformula of this formula */
subformula()247 Formula* subformula() { return _arg; }
248
249 // use allocator to (de)allocate objects of this class
250 CLASS_NAME(NegatedFormula);
251 USE_ALLOCATOR(NegatedFormula);
252 protected:
253 /** The immediate subformula */
254 Formula* _arg;
255 }; // class NegatedFormula
256
257
258 /**
259 * Binary formula.
260 * @since 02/06/2007 Manchester
261 */
262 class BinaryFormula
263 : public Formula
264 {
265 public:
266 /** building binary formula */
BinaryFormula(Connective con,Formula * lhs,Formula * rhs)267 explicit BinaryFormula (Connective con,Formula* lhs,Formula* rhs)
268 : Formula(con),
269 _left(lhs),
270 _right(rhs)
271 {
272 ASS(con == IFF || con == XOR || con == IMP);
273 }
274
275 /** Return the lhs subformula of this formula */
lhs() const276 const Formula* lhs() const { return _left; }
277 /** Return the lhs subformula of this formula */
lhs()278 Formula* lhs() { return _left; }
279 /** Return the rhs subformula of this formula */
rhs() const280 const Formula* rhs() const { return _right; }
281 /** Return the rhs subformula of this formula */
rhs()282 Formula* rhs() { return _right; }
283
284 // use allocator to (de)allocate objects of this class
285 CLASS_NAME(BinaryFormula);
286 USE_ALLOCATOR(BinaryFormula);
287 protected:
288 /** The lhs subformula */
289 Formula* _left;
290 /** The rhs subformula */
291 Formula* _right;
292 }; // class BinaryFormula
293
294
295 /**
296 * Conjunction and disjunction.
297 * @since 02/06/2007 Manchester
298 */
299 class JunctionFormula
300 : public Formula
301 {
302 public:
JunctionFormula(Connective con,FormulaList * args)303 JunctionFormula (Connective con, FormulaList* args)
304 : Formula(con),
305 _args(args)
306 {
307 ASS(con == AND || con == OR);
308 ASS_GE(FormulaList::length(args),2);
309 }
310
311 /** set arguments to args */
setArgs(FormulaList * args)312 void setArgs(FormulaList* args) { _args = args; }
313
314 /** Return the list of immediate subformulas */
getArgs() const315 const FormulaList* getArgs() const { return _args; }
316 /** Return the list of immediate subformulas */
getArgs()317 FormulaList* getArgs() { return _args; }
318 /** Return a pointer to the list of immediate subformulas */
getArgsPtr()319 FormulaList** getArgsPtr() { return &_args; }
320
321 static Formula* generalJunction(Connective c, FormulaList* args);
322
323 // use allocator to (de)allocate objects of this class
324 CLASS_NAME(JunctionFormula);
325 USE_ALLOCATOR(JunctionFormula);
326 protected:
327 /** list of immediate subformulas */
328 FormulaList* _args;
329 }; // class JunctionFormula
330
331
332 /**
333 * A formula that is just a boolean term.
334 * @since 02/06/2007 Manchester
335 */
336 class BoolTermFormula
337 : public Formula
338 {
339 public:
BoolTermFormula(TermList ts)340 BoolTermFormula (TermList ts)
341 : Formula(BOOL_TERM),
342 _ts(ts)
343 {
344 // only boolean terms in formula context are expected here
345 ASS_REP(ts.isVar() || ts.term()->isITE() || ts.term()->isLet() || ts.term()->isTupleLet(), ts.toString());
346 }
347
create(TermList ts)348 static Formula* create(TermList ts) {
349 if (ts.isVar()) {
350 return new BoolTermFormula(ts);
351 }
352
353 Term* term = ts.term();
354 if (term->isSpecial()) {
355 Term::SpecialTermData *sd = term->getSpecialData();
356 switch (sd->getType()) {
357 case Term::SF_FORMULA:
358 return sd->getFormula();
359 default:
360 return new BoolTermFormula(ts);
361 }
362 } else {
363 unsigned functor = term->functor();
364 if (env.signature->isFoolConstantSymbol(true, functor)) {
365 return new Formula(true);
366 } else {
367 ASS(env.signature->isFoolConstantSymbol(false, functor));
368 return new Formula(false);
369 }
370 }
371 }
372
373 /** Return the variable */
getTerm() const374 const TermList getTerm() const { return _ts; }
getTerm()375 TermList getTerm() { return _ts; }
376
377 // use allocator to (de)allocate objects of this class
378 CLASS_NAME(BoolTermFormula);
379 USE_ALLOCATOR(BoolTermFormula);
380 protected:
381 /** boolean term */
382 TermList _ts;
383 }; // class BoolTermFormula
384
385 // definitions, had to be put out of class
386
387 /** Return the list of variables of a quantified formula */
388 inline
vars() const389 const Formula::VarList* Formula::vars() const
390 {
391 ASS(_connective == FORALL || _connective == EXISTS);
392 return static_cast<const QuantifiedFormula*>(this)->varList();
393 }
394 /** Return the list of variables of a quantified formula */
395 inline
vars()396 Formula::VarList* Formula::vars()
397 {
398 ASS(_connective == FORALL || _connective == EXISTS);
399 return static_cast<QuantifiedFormula*>(this)->varList();
400 }
401
402 /** Return the list of sorts of a quantified formula */
403 inline
sorts() const404 const Formula::SortList* Formula::sorts() const
405 {
406 ASS(_connective == FORALL || _connective == EXISTS);
407 return static_cast<const QuantifiedFormula*>(this)->sortList();
408 }
409 /** Return the list of sorts of a quantified formula */
410 inline
sorts()411 Formula::SortList* Formula::sorts()
412 {
413 ASS(_connective == FORALL || _connective == EXISTS);
414 return static_cast<QuantifiedFormula*>(this)->sortList();
415 }
416
417 /** Return the immediate subformula of a quantified formula */
418 inline
qarg() const419 const Formula* Formula::qarg() const
420 {
421 ASS(_connective == FORALL || _connective == EXISTS);
422 return static_cast<const QuantifiedFormula*>(this)->subformula();
423 }
424 /** Return the immediate subformula of a quantified formula */
425 inline
qarg()426 Formula* Formula::qarg()
427 {
428 ASS(_connective == FORALL || _connective == EXISTS);
429 return static_cast<QuantifiedFormula*>(this)->subformula();
430 }
431
432 /** Return the immediate subformula of a negated formula */
433 inline
uarg() const434 const Formula* Formula::uarg() const
435 {
436 ASS(_connective == NOT);
437 return static_cast<const NegatedFormula*>(this)->subformula();
438 }
439
440 /** Return the immediate subformula of a negated formula */
441 inline
uarg()442 Formula* Formula::uarg()
443 {
444 ASS(_connective == NOT);
445 return static_cast<NegatedFormula*>(this)->subformula();
446 }
447
448 /** Return the list of immediate subformulas of a junction formula */
449 inline
args() const450 const FormulaList* Formula::args() const
451 {
452 ASS(_connective == AND || _connective == OR);
453 return static_cast<const JunctionFormula*>(this)->getArgs();
454 }
455
456 /** Return the list of immediate subformulas of a junction formula */
457 inline
args()458 FormulaList* Formula::args()
459 {
460 ASS(_connective == AND || _connective == OR);
461 return static_cast<JunctionFormula*>(this)->getArgs();
462 }
463
464 /** Return a pointer to the list of immediate subformulas of a junction formula */
465 inline
argsPtr()466 FormulaList** Formula::argsPtr()
467 {
468 ASS(_connective == AND || _connective == OR);
469 return static_cast<JunctionFormula*>(this)->getArgsPtr();
470 }
471
472 /** Return the literal of an atomic formula */
473 inline
literal() const474 const Literal* Formula::literal() const
475 {
476 ASS(_connective == LITERAL);
477 return static_cast<const AtomicFormula*>(this)->getLiteral();
478 }
479
480 /** Return the literal of an atomic formula */
481 inline
literal()482 Literal* Formula::literal()
483 {
484 ASS(_connective == LITERAL);
485 return static_cast<AtomicFormula*>(this)->getLiteral();
486 }
487
488 /** Return the lhs subformula of a binary formula */
489 inline
left() const490 const Formula* Formula::left() const
491 {
492 ASS(_connective == IFF || _connective == XOR || _connective == IMP);
493 return static_cast<const BinaryFormula*>(this)->lhs();
494 }
495 /** Return the lhs subformula of a binary formula */
496 inline
left()497 Formula* Formula::left()
498 {
499 ASS(_connective == IFF || _connective == XOR || _connective == IMP);
500 return static_cast<BinaryFormula*>(this)->lhs();
501 }
502
503 /** Return the rhs subformula of a binary formula */
504 inline
right() const505 const Formula* Formula::right() const
506 {
507 ASS(_connective == IFF || _connective == XOR || _connective == IMP);
508 return static_cast<const BinaryFormula*>(this)->rhs();
509 }
510 /** Return the rhs subformula of a binary formula */
511 inline
right()512 Formula* Formula::right()
513 {
514 ASS(_connective == IFF || _connective == XOR || _connective == IMP);
515 return static_cast<BinaryFormula*>(this)->rhs();
516 }
517
518 inline
getBooleanTerm() const519 const TermList Formula::getBooleanTerm() const
520 {
521 ASS(_connective == BOOL_TERM);
522 return static_cast<const BoolTermFormula*>(this)->getTerm();
523 }
524 inline
getBooleanTerm()525 TermList Formula::getBooleanTerm()
526 {
527 ASS(_connective == BOOL_TERM);
528 return static_cast<BoolTermFormula*>(this)->getTerm();
529 }
530
531 // operators
532
533 std::ostream& operator<< (ostream& out, const Formula& f);
534 std::ostream& operator<< (ostream& out, const Formula* f);
535
536 }
537
538 #endif // __Formula__
539