1
2 /*
3 * File SMTLIB2.cpp.
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 SMTLIB.cpp
21 * Implements class SMTLIB.
22 */
23
24 #include <climits>
25 #include <fstream>
26
27 #include "Lib/Environment.hpp"
28 #include "Lib/NameArray.hpp"
29 #include "Lib/StringUtils.hpp"
30 #include "Kernel/Clause.hpp"
31 #include "Kernel/ColorHelper.hpp"
32 #include "Kernel/Formula.hpp"
33 #include "Kernel/FormulaUnit.hpp"
34 #include "Kernel/Inference.hpp"
35 #include "Kernel/Signature.hpp"
36 #include "Kernel/SortHelper.hpp"
37
38 #include "Shell/LispLexer.hpp"
39 #include "Shell/Options.hpp"
40 #include "Shell/SMTLIBLogic.hpp"
41 #include "Shell/TermAlgebra.hpp"
42
43 #include "SMTLIB2.hpp"
44
45 #include "TPTP.hpp"
46
47 #undef LOGGING
48 #define LOGGING 0
49
50 #if LOGGING
51 #define LOG1(arg) cout << arg << endl;
52 #define LOG2(a1,a2) cout << a1 << a2 << endl;
53 #define LOG3(a1,a2,a3) cout << a1 << a2 << a3 << endl;
54 #define LOG4(a1,a2,a3,a4) cout << a1 << a2 << a3 << a4 << endl;
55 #else
56 #define LOG1(arg)
57 #define LOG2(a1,a2)
58 #define LOG3(a1,a2,a3)
59 #define LOG4(a1,a2,a3,a4)
60 #endif
61
62 namespace Parse {
63
SMTLIB2(const Options & opts)64 SMTLIB2::SMTLIB2(const Options& opts)
65 : _logicSet(false),
66 _logic(SMT_UNDEFINED),
67 _numeralsAreReal(false),
68 _formulas(nullptr)
69 {
70 CALL("SMTLIB2::SMTLIB2");
71 }
72
parse(istream & str)73 void SMTLIB2::parse(istream& str)
74 {
75 CALL("SMTLIB2::parse(istream&)");
76
77 LispLexer lex(str);
78 LispParser lpar(lex);
79 LExpr* expr = lpar.parse();
80 parse(expr);
81 }
82
parse(LExpr * bench)83 void SMTLIB2::parse(LExpr* bench)
84 {
85 CALL("SMTLIB2::parse(LExpr*)");
86
87 ASS(bench->isList());
88 readBenchmark(bench->list);
89 }
90
readBenchmark(LExprList * bench)91 void SMTLIB2::readBenchmark(LExprList* bench)
92 {
93 CALL("SMTLIB2::readBenchmark");
94 LispListReader bRdr(bench);
95
96 // iteration over benchmark top level entries
97 while(bRdr.hasNext()){
98 LExpr* lexp = bRdr.next();
99
100 LOG2("readBenchmark ",lexp->toString(true));
101
102 LispListReader ibRdr(lexp);
103
104 if (ibRdr.tryAcceptAtom("set-logic")) {
105 if (_logicSet) {
106 USER_ERROR("set-logic can appear only once in a problem");
107 }
108 readLogic(ibRdr.readAtom());
109 ibRdr.acceptEOL();
110 continue;
111 }
112
113 if (ibRdr.tryAcceptAtom("set-info")) {
114
115 if (ibRdr.tryAcceptAtom(":status")) {
116 _statusStr = ibRdr.readAtom();
117 ibRdr.acceptEOL();
118 continue;
119 }
120
121 if (ibRdr.tryAcceptAtom(":source")) {
122 _sourceInfo = ibRdr.readAtom();
123 ibRdr.acceptEOL();
124 continue;
125 }
126
127 // ignore unknown info
128 ibRdr.readAtom();
129 ibRdr.readAtom();
130 ibRdr.acceptEOL();
131 continue;
132 }
133
134 if (ibRdr.tryAcceptAtom("declare-sort")) {
135 vstring name = ibRdr.readAtom();
136 vstring arity;
137 if (!ibRdr.tryReadAtom(arity)) {
138 USER_ERROR("Unspecified arity while declaring sort: "+name);
139 }
140
141 readDeclareSort(name,arity);
142
143 ibRdr.acceptEOL();
144
145 continue;
146 }
147
148 if (ibRdr.tryAcceptAtom("define-sort")) {
149 vstring name = ibRdr.readAtom();
150 LExprList* args = ibRdr.readList();
151 LExpr* body = ibRdr.readNext();
152
153 readDefineSort(name,args,body);
154
155 ibRdr.acceptEOL();
156
157 continue;
158 }
159
160 if (ibRdr.tryAcceptAtom("declare-fun")) {
161 vstring name = ibRdr.readAtom();
162 LExprList* iSorts = ibRdr.readList();
163 LExpr* oSort = ibRdr.readNext();
164
165 readDeclareFun(name,iSorts,oSort);
166
167 ibRdr.acceptEOL();
168
169 continue;
170 }
171
172 if (ibRdr.tryAcceptAtom("declare-datatypes")) {
173 LExprList* sorts = ibRdr.readList();
174 LExprList* datatypes = ibRdr.readList();
175
176 readDeclareDatatypes(sorts, datatypes, false);
177
178 ibRdr.acceptEOL();
179
180 continue;
181 }
182
183 if (ibRdr.tryAcceptAtom("declare-codatatypes")) {
184 LExprList* sorts = ibRdr.readList();
185 LExprList* datatypes = ibRdr.readList();
186
187 readDeclareDatatypes(sorts, datatypes, true);
188
189 ibRdr.acceptEOL();
190
191 continue;
192 }
193
194 if (ibRdr.tryAcceptAtom("declare-const")) {
195 vstring name = ibRdr.readAtom();
196 LExpr* oSort = ibRdr.readNext();
197
198 readDeclareFun(name,nullptr,oSort);
199
200 ibRdr.acceptEOL();
201
202 continue;
203 }
204
205 if (ibRdr.tryAcceptAtom("define-fun")) {
206 vstring name = ibRdr.readAtom();
207 LExprList* iArgs = ibRdr.readList();
208 LExpr* oSort = ibRdr.readNext();
209 LExpr* body = ibRdr.readNext();
210
211 readDefineFun(name,iArgs,oSort,body);
212
213 ibRdr.acceptEOL();
214
215 continue;
216 }
217
218 if (ibRdr.tryAcceptAtom("assert")) {
219 readAssert(ibRdr.readNext());
220
221 ibRdr.acceptEOL();
222
223 continue;
224 }
225
226 if (ibRdr.tryAcceptAtom("assert-not")) {
227 readAssertNot(ibRdr.readNext());
228
229 ibRdr.acceptEOL();
230
231 continue;
232 }
233
234 // not an official SMTLIB command
235 if (ibRdr.tryAcceptAtom("color-symbol")) {
236 vstring symbol = ibRdr.readAtom();
237
238 if (ibRdr.tryAcceptAtom(":left")) {
239 colorSymbol(symbol, Color::COLOR_LEFT);
240 } else if (ibRdr.tryAcceptAtom(":right")) {
241 colorSymbol(symbol, Color::COLOR_RIGHT);
242 } else {
243 USER_ERROR("'"+ibRdr.readAtom()+"' is not a color keyword");
244 }
245
246 ibRdr.acceptEOL();
247
248 continue;
249 }
250
251 if (ibRdr.tryAcceptAtom("check-sat")) {
252 if (bRdr.hasNext()) {
253 LispListReader exitRdr(bRdr.readList());
254 if (!exitRdr.tryAcceptAtom("exit")) {
255 if(env.options->mode()!=Options::Mode::SPIDER) {
256 env.beginOutput();
257 env.out() << "% Warning: check-sat is not the last entry. Skipping the rest!" << endl;
258 env.endOutput();
259 }
260 }
261 }
262 break;
263 }
264
265 if (ibRdr.tryAcceptAtom("exit")) {
266 bRdr.acceptEOL();
267 break;
268 }
269
270 if (ibRdr.tryAcceptAtom("reset")) {
271 LOG1("ignoring reset");
272 continue;
273 }
274
275 if (ibRdr.tryAcceptAtom("set-option")) {
276 LOG2("ignoring set-option", ibRdr.readAtom());
277 continue;
278 }
279
280 if (ibRdr.tryAcceptAtom("push")) {
281 LOG1("ignoring push");
282 continue;
283 }
284
285 if (ibRdr.tryAcceptAtom("get-info")) {
286 LOG2("ignoring get-info", ibRdr.readAtom());
287 continue;
288 }
289
290 USER_ERROR("unrecognized entry "+ibRdr.readAtom());
291 }
292 }
293
294 // ----------------------------------------------------------------------
295
296 const char * SMTLIB2::s_smtlibLogicNameStrings[] = {
297 "ALIA",
298 "ALL",
299 "AUFDTLIA",
300 "AUFDTLIRA",
301 "AUFDTNIRA",
302 "AUFLIA",
303 "AUFLIRA",
304 "AUFNIA",
305 "AUFNIRA",
306 "BV",
307 "LIA",
308 "LRA",
309 "NIA",
310 "NRA",
311 "QF_ABV",
312 "QF_ALIA",
313 "QF_ANIA",
314 "QF_AUFBV",
315 "QF_AUFLIA",
316 "QF_AUFNIA",
317 "QF_AX",
318 "QF_BV",
319 "QF_IDL",
320 "QF_LIA",
321 "QF_LIRA",
322 "QF_LRA",
323 "QF_NIA",
324 "QF_NIRA",
325 "QF_NRA",
326 "QF_RDL",
327 "QF_UF",
328 "QF_UFBV",
329 "QF_UFIDL",
330 "QF_UFLIA",
331 "QF_UFLRA",
332 "QF_UFNIA",
333 "QF_UFNRA",
334 "UF",
335 "UFBV",
336 "UFDT",
337 "UFDTLIA",
338 "UFDTLIRA",
339 "UFDTNIA",
340 "UFDTNIRA",
341 "UFIDL",
342 "UFLIA",
343 "UFLRA",
344 "UFNIA"
345 };
346
getLogicFromString(const vstring & str)347 SMTLIBLogic SMTLIB2::getLogicFromString(const vstring& str)
348 {
349 CALL("SMTLIB2::getLogicFromString");
350
351 static NameArray smtlibLogicNames(s_smtlibLogicNameStrings, sizeof(s_smtlibLogicNameStrings)/sizeof(char*));
352 ASS_EQ(smtlibLogicNames.length, SMT_UNDEFINED);
353
354 int res = smtlibLogicNames.tryToFind(str.c_str());
355 if(res==-1) {
356 return SMT_UNDEFINED;
357 }
358 return static_cast<SMTLIBLogic>(res);
359 }
360
readLogic(const vstring & logicStr)361 void SMTLIB2::readLogic(const vstring& logicStr)
362 {
363 CALL("SMTLIB2::checkLogic");
364
365 _logic = getLogicFromString(logicStr);
366 _logicSet = true;
367
368 switch (_logic) {
369 case SMT_ALL:
370 case SMT_ALIA:
371 case SMT_AUFDTLIA:
372 case SMT_AUFDTLIRA:
373 case SMT_AUFDTNIRA:
374 case SMT_AUFLIA:
375 case SMT_AUFNIA:
376 case SMT_AUFLIRA:
377 case SMT_AUFNIRA:
378 case SMT_LIA:
379 case SMT_NIA:
380 case SMT_QF_ALIA:
381 case SMT_QF_ANIA:
382 case SMT_QF_AUFLIA:
383 case SMT_QF_AUFNIA:
384 case SMT_QF_AX:
385 case SMT_QF_IDL:
386 case SMT_QF_LIA:
387 case SMT_QF_LIRA:
388 case SMT_QF_NIA:
389 case SMT_QF_NIRA:
390 case SMT_QF_UF:
391 case SMT_QF_UFIDL:
392 case SMT_QF_UFLIA:
393 case SMT_QF_UFNIA:
394 case SMT_UF:
395 case SMT_UFDT:
396 case SMT_UFDTLIA:
397 case SMT_UFDTLIRA:
398 case SMT_UFDTNIA:
399 case SMT_UFDTNIRA:
400 case SMT_UFIDL:
401 case SMT_UFLIA:
402 case SMT_UFNIA:
403 break;
404
405 // pure real arithmetic theories treat decimals as Real constants
406 case SMT_LRA:
407 case SMT_NRA:
408 case SMT_QF_LRA:
409 case SMT_QF_NRA:
410 case SMT_QF_RDL:
411 case SMT_QF_UFLRA:
412 case SMT_QF_UFNRA:
413 case SMT_UFLRA:
414 _numeralsAreReal = true;
415 break;
416
417 // we don't support bit vectors
418 case SMT_BV:
419 case SMT_QF_ABV:
420 case SMT_QF_AUFBV:
421 case SMT_QF_BV:
422 case SMT_QF_UFBV:
423 case SMT_UFBV:
424 USER_ERROR("unsupported logic "+logicStr);
425 default:
426 USER_ERROR("unrecognized logic "+logicStr);
427 }
428
429 }
430
431 // ----------------------------------------------------------------------
432
433 const char * SMTLIB2::s_builtInSortNameStrings[] = {
434 "Array",
435 "Bool",
436 "Int",
437 "Real"
438 };
439
getBuiltInSortFromString(const vstring & str)440 SMTLIB2::BuiltInSorts SMTLIB2::getBuiltInSortFromString(const vstring& str)
441 {
442 CALL("SMTLIB::getBuiltInSortFromString");
443
444 static NameArray builtInSortNames(s_builtInSortNameStrings, sizeof(s_builtInSortNameStrings)/sizeof(char*));
445 ASS_EQ(builtInSortNames.length, BS_INVALID);
446
447 int res = builtInSortNames.tryToFind(str.c_str());
448 if(res==-1) {
449 return BS_INVALID;
450 }
451 return static_cast<BuiltInSorts>(res);
452 }
453
isAlreadyKnownSortSymbol(const vstring & name)454 bool SMTLIB2::isAlreadyKnownSortSymbol(const vstring& name)
455 {
456 CALL("SMTLIB::isAlreadyKnownSortSymbol");
457
458 if (getBuiltInSortFromString(name) != BS_INVALID) {
459 return true;
460 }
461
462 if (_declaredSorts.find(name)) {
463 return true;
464 }
465
466 if (_sortDefinitions.find(name)) {
467 return true;
468 }
469
470 return false;
471 }
472
readDeclareSort(const vstring & name,const vstring & arity)473 void SMTLIB2::readDeclareSort(const vstring& name, const vstring& arity)
474 {
475 CALL("SMTLIB2::readDeclareSort");
476
477 if (isAlreadyKnownSortSymbol(name)) {
478 USER_ERROR("Redeclaring built-in, declared or defined sort symbol: "+name);
479 }
480
481 if (not StringUtils::isPositiveInteger(arity)) {
482 USER_ERROR("Unrecognized declared sort arity: "+arity);
483 }
484
485 unsigned val;
486 if (!Int::stringToUnsignedInt(arity, val)) {
487 USER_ERROR("Couldn't convert sort arity: "+arity);
488 }
489
490 ALWAYS(_declaredSorts.insert(name,val));
491 }
492
readDefineSort(const vstring & name,LExprList * args,LExpr * body)493 void SMTLIB2::readDefineSort(const vstring& name, LExprList* args, LExpr* body)
494 {
495 CALL("SMTLIB2::readDefineSort");
496
497 if (isAlreadyKnownSortSymbol(name)) {
498 USER_ERROR("Redeclaring built-in, declared or defined sort symbol: "+name);
499 }
500
501 // here we could check the definition for well-formed-ness
502 // current solution: crash only later, at application site
503
504 ALWAYS(_sortDefinitions.insert(name,SortDefinition(args,body)));
505 }
506
507 // ----------------------------------------------------------------------
508
509 /**
510 * SMTLIB sort expression turned into vampire sort id.
511 *
512 * Taking into account built-in sorts, declared sorts and sort definitions.
513 */
declareSort(LExpr * sExpr)514 unsigned SMTLIB2::declareSort(LExpr* sExpr)
515 {
516 CALL("SMTLIB2::declareSort");
517
518 enum SortParseOperation {
519 SPO_PARSE,
520 SPO_POP_LOOKUP,
521 SPO_CHECK_ARITY
522 };
523 static Stack<pair<SortParseOperation,LExpr*> > todo;
524 ASS(todo.isEmpty());
525
526 ASS_EQ(Sorts::SRT_DEFAULT,0); // there is no default sort in smtlib, so we can use 0 as a results separator
527 static const int SEPARATOR = 0;
528 static Stack<unsigned> results;
529 ASS(results.isEmpty());
530
531 // evaluation contexts for the expansion of sort definitions
532 typedef DHMap<vstring,unsigned> SortLookup;
533 static Stack<SortLookup*> lookups;
534 ASS(lookups.isEmpty());
535
536 // to store defined sort's identifier when expanding its definition
537 // (for preventing circular non-sense)
538 static Stack<vstring> forbidden;
539 ASS(forbidden.isEmpty());
540
541 todo.push(make_pair(SPO_PARSE,sExpr));
542
543 while (todo.isNonEmpty()) {
544 pair<SortParseOperation,LExpr*> cur = todo.pop();
545 SortParseOperation op = cur.first;
546
547 if (op == SPO_POP_LOOKUP) {
548 delete lookups.pop();
549 forbidden.pop();
550 continue;
551 }
552
553 if (op == SPO_CHECK_ARITY) {
554 if (results.size() < 2) {
555 goto malformed;
556 }
557 unsigned true_result = results.pop();
558 unsigned separator = results.pop();
559
560 if (true_result == SEPARATOR || separator != SEPARATOR) {
561 goto malformed;
562 }
563 results.push(true_result);
564
565 continue;
566 }
567
568 ASS_EQ(op,SPO_PARSE);
569 LExpr* exp = cur.second;
570
571 if (exp->isList()) {
572 LExprList::Iterator lIt(exp->list);
573
574 todo.push(make_pair(SPO_CHECK_ARITY,nullptr));
575 results.push(SEPARATOR);
576
577 while (lIt.hasNext()) {
578 todo.push(make_pair(SPO_PARSE,lIt.next()));
579 }
580 } else {
581 ASS(exp->isAtom());
582 vstring& id = exp->str;
583
584 // try (top) context lookup
585 if (lookups.isNonEmpty()) {
586 SortLookup* lookup = lookups.top();
587 unsigned res;
588 if (lookup->find(id,res)) {
589 results.push(res);
590 continue;
591 }
592 }
593
594 {
595 for (unsigned i = 0; i < forbidden.size(); i++) {
596 if (id == forbidden[i]) {
597 USER_ERROR("Expanding circular sort definition "+ id);
598 }
599 }
600 }
601
602 // try declared sorts
603 unsigned arity;
604 if (_declaredSorts.find(id,arity)) {
605 // building an arbitrary but unique sort string
606 // TODO: this may not be good enough for a tptp-compliant output!
607 vstring sortName = id + "(";
608 while (arity--) {
609 if (results.isEmpty() || results.top() == SEPARATOR) {
610 goto malformed;
611 }
612 sortName += Int::toString(results.pop());
613 if (arity) {
614 sortName += ",";
615 }
616 }
617 sortName += ")";
618
619 unsigned newSort = env.sorts->addSort(sortName,false);
620 results.push(newSort);
621
622 continue;
623 }
624
625 // try defined sorts
626 SortDefinition def;
627 if (_sortDefinitions.find(id,def)) {
628 SortLookup* lookup = new SortLookup();
629
630 LispListReader argRdr(def.args);
631
632 while (argRdr.hasNext()) {
633 if (results.isEmpty() || results.top() == SEPARATOR) {
634 goto malformed;
635 }
636 unsigned argSort = results.pop();
637 const vstring& argName = argRdr.readAtom();
638 // TODO: could check if the same string names more than one argument positions
639 // the following just takes the first and ignores the others
640 lookup->insert(argName,argSort);
641 }
642
643 lookups.push(lookup);
644 forbidden.push(id);
645
646 todo.push(make_pair(SPO_POP_LOOKUP,nullptr)); //schedule lookup deletion (see above)
647 todo.push(make_pair(SPO_PARSE,def.body));
648
649 continue;
650 }
651
652 // try built-ins
653 BuiltInSorts bs = getBuiltInSortFromString(id);
654 switch (bs) {
655 case BS_BOOL:
656 results.push(Sorts::SRT_BOOL);
657 continue;
658 case BS_INT:
659 results.push(Sorts::SRT_INTEGER);
660 continue;
661 case BS_REAL:
662 results.push(Sorts::SRT_REAL);
663 continue;
664 case BS_ARRAY:
665 if (results.size() < 2) {
666 goto malformed;
667 } else {
668 unsigned indexSort = results.pop();
669 unsigned innerSort = results.pop();
670 if (indexSort == SEPARATOR || innerSort == SEPARATOR) {
671 goto malformed;
672 }
673 results.push(env.sorts->addArraySort(indexSort,innerSort));
674 continue;
675 }
676
677 default:
678 ASS_EQ(bs,BS_INVALID);
679 }
680
681 USER_ERROR("Unrecognized sort identifier "+id);
682 }
683 }
684
685 if (results.size() == 1) {
686 return results.pop();
687 } else {
688 malformed:
689 USER_ERROR("Malformed type expression "+sExpr->toString());
690 }
691 }
692
693 static const char* EXISTS = "exists";
694 static const char* FORALL = "forall";
695
696 const char * SMTLIB2::s_formulaSymbolNameStrings[] = {
697 "<",
698 "<=",
699 "=",
700 "=>",
701 ">",
702 ">=",
703 "and",
704 "distinct",
705 EXISTS,
706 "false",
707 FORALL,
708 "is_int",
709 "not",
710 "or",
711 "true",
712 "xor"
713 };
714
getBuiltInFormulaSymbol(const vstring & str)715 SMTLIB2::FormulaSymbol SMTLIB2::getBuiltInFormulaSymbol(const vstring& str)
716 {
717 CALL("SMTLIB::getFormulaSymbol");
718
719 static NameArray formulaSymbolNames(s_formulaSymbolNameStrings, sizeof(s_formulaSymbolNameStrings)/sizeof(char*));
720 ASS_EQ(formulaSymbolNames.length, FS_USER_PRED_SYMBOL);
721
722 int res = formulaSymbolNames.tryToFind(str.c_str());
723 if(res==-1) {
724 return FS_USER_PRED_SYMBOL;
725 }
726 return static_cast<FormulaSymbol>(res);
727 }
728
729 static const char* LET = "let";
730
731 const char * SMTLIB2::s_termSymbolNameStrings[] = {
732 "*",
733 "+",
734 "-",
735 "/",
736 "abs",
737 "div",
738 "ite",
739 LET,
740 "mod",
741 "select",
742 "store",
743 "to_int",
744 "to_real"
745 };
746
getBuiltInTermSymbol(const vstring & str)747 SMTLIB2::TermSymbol SMTLIB2::getBuiltInTermSymbol(const vstring& str)
748 {
749 CALL("SMTLIB::getTermSymbol");
750
751 static NameArray termSymbolNames(s_termSymbolNameStrings, sizeof(s_termSymbolNameStrings)/sizeof(char*));
752 ASS_EQ(termSymbolNames.length, TS_USER_FUNCTION);
753
754 int resInt = termSymbolNames.tryToFind(str.c_str());
755 if(resInt==-1) {
756 return TS_USER_FUNCTION;
757 }
758 return static_cast<TermSymbol>(resInt);
759 }
760
isAlreadyKnownFunctionSymbol(const vstring & name)761 bool SMTLIB2::isAlreadyKnownFunctionSymbol(const vstring& name)
762 {
763 CALL("SMTLIB2::isAlreadyKnownFunctionSymbol");
764
765 if (getBuiltInFormulaSymbol(name) != FS_USER_PRED_SYMBOL) {
766 return true;
767 }
768
769 if (getBuiltInTermSymbol(name) != TS_USER_FUNCTION) {
770 return true;
771 }
772
773 if (_declaredFunctions.find(name)) {
774 return true;
775 }
776
777 return false;
778 }
779
readDeclareFun(const vstring & name,LExprList * iSorts,LExpr * oSort)780 void SMTLIB2::readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSort)
781 {
782 CALL("SMTLIB2::readDeclareFun");
783
784 if (isAlreadyKnownFunctionSymbol(name)) {
785 USER_ERROR("Redeclaring function symbol: "+name);
786 }
787
788 unsigned rangeSort = declareSort(oSort);
789
790 LispListReader isRdr(iSorts);
791
792 static Stack<unsigned> argSorts;
793 argSorts.reset();
794
795 while (isRdr.hasNext()) {
796 argSorts.push(declareSort(isRdr.next()));
797 }
798
799 declareFunctionOrPredicate(name,rangeSort,argSorts);
800 }
801
declareFunctionOrPredicate(const vstring & name,signed rangeSort,const Stack<unsigned> & argSorts)802 SMTLIB2::DeclaredFunction SMTLIB2::declareFunctionOrPredicate(const vstring& name, signed rangeSort, const Stack<unsigned>& argSorts)
803 {
804 CALL("SMTLIB2::declareFunctionOrPredicate");
805
806 bool added;
807 unsigned symNum;
808 Signature::Symbol* sym;
809 OperatorType* type;
810
811 if (rangeSort == Sorts::SRT_BOOL) { // predicate
812 symNum = env.signature->addPredicate(name, argSorts.size(), added);
813
814 sym = env.signature->getPredicate(symNum);
815
816 type = OperatorType::getPredicateType(argSorts.size(),argSorts.begin());
817
818 LOG1("declareFunctionOrPredicate-Predicate");
819 } else { // proper function
820 if (argSorts.size() > 0) {
821 symNum = env.signature->addFunction(name, argSorts.size(), added);
822 } else {
823 symNum = TPTP::addUninterpretedConstant(name,_overflow,added);
824 }
825
826 sym = env.signature->getFunction(symNum);
827
828 type = OperatorType::getFunctionType(argSorts.size(), argSorts.begin(), rangeSort);
829
830 LOG1("declareFunctionOrPredicate-Function");
831 }
832
833 ASS(added);
834 sym->setType(type);
835
836 DeclaredFunction res = make_pair(symNum,type->isFunctionType());
837
838 LOG2("declareFunctionOrPredicate -name ",name);
839 LOG2("declareFunctionOrPredicate -symNum ",symNum);
840
841 ALWAYS(_declaredFunctions.insert(name,res));
842
843 return res;
844 }
845
846 // ----------------------------------------------------------------------
847
readDefineFun(const vstring & name,LExprList * iArgs,LExpr * oSort,LExpr * body)848 void SMTLIB2::readDefineFun(const vstring& name, LExprList* iArgs, LExpr* oSort, LExpr* body)
849 {
850 CALL("SMTLIB2::readDefineFun");
851
852 if (isAlreadyKnownFunctionSymbol(name)) {
853 USER_ERROR("Redeclaring function symbol: "+name);
854 }
855
856 unsigned rangeSort = declareSort(oSort);
857
858 _nextVar = 0;
859 ASS(_scopes.isEmpty());
860 TermLookup* lookup = new TermLookup();
861
862 static Stack<unsigned> argSorts;
863 argSorts.reset();
864
865 static Stack<TermList> args;
866 args.reset();
867
868 LispListReader iaRdr(iArgs);
869 while (iaRdr.hasNext()) {
870 LExprList* pair = iaRdr.readList();
871 LispListReader pRdr(pair);
872
873 vstring vName = pRdr.readAtom();
874 unsigned vSort = declareSort(pRdr.readNext());
875
876 pRdr.acceptEOL();
877
878 TermList arg = TermList(_nextVar++, false);
879 args.push(arg);
880
881 if (!lookup->insert(vName,make_pair(arg,vSort))) {
882 USER_ERROR("Multiple occurrence of variable "+vName+" in the definition of function "+name);
883 }
884
885 argSorts.push(vSort);
886 }
887
888 _scopes.push(lookup);
889
890 ParseResult res = parseTermOrFormula(body);
891
892 delete _scopes.pop();
893
894 TermList rhs;
895 if (res.asTerm(rhs) != rangeSort) {
896 USER_ERROR("Defined function body "+body->toString()+" has different sort than declared "+oSort->toString());
897 }
898
899 // Only after parsing, so that the definition cannot be recursive
900 DeclaredFunction fun = declareFunctionOrPredicate(name,rangeSort,argSorts);
901
902 unsigned symbIdx = fun.first;
903 bool isTrueFun = fun.second;
904
905 TermList lhs;
906 if (isTrueFun) {
907 lhs = TermList(Term::create(symbIdx,args.size(),args.begin()));
908 } else {
909 Formula* frm = new AtomicFormula(Literal::create(symbIdx,args.size(),true,false,args.begin()));
910 lhs = TermList(Term::createFormula(frm));
911 }
912
913 Formula* fla = new AtomicFormula(Literal::createEquality(true,lhs,rhs,rangeSort));
914
915 FormulaUnit* fu = new FormulaUnit(fla, FromInput(UnitInputType::ASSUMPTION));
916
917 UnitList::push(fu, _formulas);
918 }
919
readDeclareDatatypes(LExprList * sorts,LExprList * datatypes,bool codatatype)920 void SMTLIB2::readDeclareDatatypes(LExprList* sorts, LExprList* datatypes, bool codatatype)
921 {
922 CALL("SMTLIB2::readDeclareDatatypes");
923
924 if(LExprList::length(sorts) != LExprList::length(datatypes)){
925 USER_ERROR("declare-datatype(s) declaration mismatch between declared datatypes and definitions");
926 }
927
928 // first declare all the sorts, and then only the constructors, in
929 // order to allow mutually recursive datatypes definitions
930 LispListReader dtypesNamesRdr(sorts);
931 Stack<vstring> dtypeNames;
932 while (dtypesNamesRdr.hasNext()) {
933 LispListReader dtypeNRdr(dtypesNamesRdr.readList());
934
935 const vstring& dtypeName = dtypeNRdr.readAtom();
936 const vstring& dtypeSize = dtypeNRdr.readAtom();
937 unsigned arity;
938 if(!Int::stringToUnsignedInt(dtypeSize,arity)){ USER_ERROR("datatype arity not given"); }
939 if(arity>0){ USER_ERROR("unsupported parametric datatype declaration"); }
940 if (isAlreadyKnownSortSymbol(dtypeName)) {
941 USER_ERROR("Redeclaring built-in, declared or defined sort symbol as datatype: "+dtypeName);
942 }
943
944 ALWAYS(_declaredSorts.insert(dtypeName, 0));
945 bool added;
946 unsigned srt = env.sorts->addSort(dtypeName + "()", added,false);
947 ASS(added);
948 (void)srt; // to get rid of compiler warning when logging is off
949 // TODO: is it really OK we normally don't need the sort?
950 LOG2("reading datatype "+dtypeName+" as sort ",srt);
951 dtypeNames.push(dtypeName+"()");
952 }
953
954 Stack<TermAlgebraConstructor*> constructors;
955 Stack<unsigned> argSorts;
956 Stack<vstring> destructorNames;
957
958 LispListReader dtypesDefsRdr(datatypes);
959 Stack<vstring>::BottomFirstIterator dtypeNameIter(dtypeNames);
960 while(dtypesDefsRdr.hasNext()) {
961 ASS(dtypeNameIter.hasNext());
962 constructors.reset();
963 const vstring& taName = dtypeNameIter.next();
964 bool added;
965 unsigned taSort = env.sorts->addSort(taName, added, false);
966 ASS(!added);
967
968 LispListReader dtypeRdr(dtypesDefsRdr.readList());
969 while (dtypeRdr.hasNext()) {
970 argSorts.reset();
971 destructorNames.reset();
972 // read each constructor declaration
973 vstring constrName;
974 LExpr *constr = dtypeRdr.next();
975 if (constr->isAtom()) {
976 // atom, construtor of arity 0
977 constrName = constr->str;
978 } else {
979 ASS(constr->isList());
980 LispListReader constrRdr(constr);
981 constrName = constrRdr.readAtom();
982
983 while (constrRdr.hasNext()) {
984 LExpr *arg = constrRdr.next();
985 LispListReader argRdr(arg);
986 destructorNames.push(argRdr.readAtom());
987 argSorts.push(declareSort(argRdr.next()));
988 if (argRdr.hasNext()) {
989 USER_ERROR("Bad constructor argument:" + arg->toString());
990 }
991 }
992 }
993 constructors.push(buildTermAlgebraConstructor(constrName, taSort, destructorNames, argSorts));
994 }
995
996 ASS(!env.signature->isTermAlgebraSort(taSort));
997 TermAlgebra* ta = new TermAlgebra(taSort, constructors.size(), constructors.begin(), codatatype);
998
999 if (ta->emptyDomain()) {
1000 USER_ERROR("Datatype " + taName + " defines an empty sort");
1001 }
1002
1003 env.signature->addTermAlgebra(ta);
1004 }
1005 }
1006
buildTermAlgebraConstructor(vstring constrName,unsigned taSort,Stack<vstring> destructorNames,Stack<unsigned> argSorts)1007 TermAlgebraConstructor* SMTLIB2::buildTermAlgebraConstructor(vstring constrName, unsigned taSort,
1008 Stack<vstring> destructorNames, Stack<unsigned> argSorts) {
1009 CALL("SMTLIB2::buildTermAlgebraConstructor");
1010
1011 if (isAlreadyKnownFunctionSymbol(constrName)) {
1012 USER_ERROR("Redeclaring function symbol: " + constrName);
1013 }
1014
1015 unsigned arity = (unsigned)argSorts.size();
1016
1017 bool added;
1018 unsigned functor = env.signature->addFunction(constrName, arity, added);
1019 ASS(added);
1020
1021 OperatorType* constructorType = OperatorType::getFunctionType(arity, argSorts.begin(), taSort);
1022 env.signature->getFunction(functor)->setType(constructorType);
1023 env.signature->getFunction(functor)->markTermAlgebraCons();
1024
1025 LOG1("build constructor "+constrName+": "+constructorType->toString());
1026
1027 ALWAYS(_declaredFunctions.insert(constrName, make_pair(functor, true)));
1028
1029 Lib::Array<unsigned> destructorFunctors(arity);
1030 for (unsigned i = 0; i < arity; i++) {
1031 vstring destructorName = destructorNames[i];
1032 unsigned destructorSort = argSorts[i];
1033
1034 if (isAlreadyKnownFunctionSymbol(destructorName)) {
1035 USER_ERROR("Redeclaring function symbol: " + destructorName);
1036 }
1037
1038 bool isPredicate = destructorSort == Sorts::SRT_BOOL;
1039 bool added;
1040 unsigned destructorFunctor = isPredicate ? env.signature->addPredicate(destructorName, 1, added)
1041 : env.signature->addFunction(destructorName, 1, added);
1042 ASS(added);
1043
1044 OperatorType* destructorType = isPredicate ? OperatorType::getPredicateType(1, &taSort)
1045 : OperatorType::getFunctionType(1, &taSort, destructorSort);
1046
1047 LOG1("build destructor "+destructorName+": "+destructorType->toString());
1048
1049 if (isPredicate) {
1050 env.signature->getPredicate(destructorFunctor)->setType(destructorType);
1051 } else {
1052 env.signature->getFunction(destructorFunctor)->setType(destructorType);
1053 }
1054
1055 ALWAYS(_declaredFunctions.insert(destructorName, make_pair(destructorFunctor, !isPredicate)));
1056
1057 destructorFunctors[i] = destructorFunctor;
1058 }
1059
1060 return new TermAlgebraConstructor(functor, destructorFunctors);
1061 }
1062
asFormula(Formula * & resFrm)1063 bool SMTLIB2::ParseResult::asFormula(Formula*& resFrm)
1064 {
1065 CALL("SMTLIB2::ParseResult::asFormula");
1066
1067 if (formula) {
1068 ASS_EQ(sort, Sorts::SRT_BOOL);
1069 resFrm = frm;
1070
1071 LOG2("asFormula formula ",resFrm->toString());
1072 return true;
1073 }
1074
1075 if (sort == Sorts::SRT_BOOL) {
1076 // can we unwrap instead of wrapping back and forth?
1077 if (trm.isTerm()) {
1078 Term* t = trm.term();
1079 if (t->isFormula()) {
1080 resFrm = t->getSpecialData()->getFormula();
1081
1082 // t->destroy(); -- we cannot -- it can be accessed more than once
1083
1084 LOG2("asFormula unwrap ",trm.toString());
1085
1086 return true;
1087 }
1088 }
1089
1090 LOG2("asFormula wrap ",trm.toString());
1091
1092 resFrm = new BoolTermFormula(trm);
1093 return true;
1094 }
1095
1096 return false;
1097 }
1098
asTerm(TermList & resTrm)1099 unsigned SMTLIB2::ParseResult::asTerm(TermList& resTrm)
1100 {
1101 CALL("SMTLIB2::ParseResult::asTerm");
1102
1103 if (formula) {
1104 ASS_EQ(sort, Sorts::SRT_BOOL);
1105
1106 LOG2("asTerm wrap ",frm->toString());
1107
1108 resTrm = TermList(Term::createFormula(frm));
1109
1110 LOG2("asTerm sort ",sort);
1111 return Sorts::SRT_BOOL;
1112 } else {
1113 resTrm = trm;
1114
1115 LOG2("asTerm native ",trm.toString());
1116
1117 LOG2("asTerm sort ",sort);
1118
1119 return sort;
1120 }
1121 }
1122
toString()1123 vstring SMTLIB2::ParseResult::toString()
1124 {
1125 CALL("SMTLIB2::ParseResult::toString");
1126 if (isSeparator()) {
1127 return "separator";
1128 }
1129 if (formula) {
1130 return "formula of sort "+Int::toString(sort)+": "+frm->toString();
1131 }
1132 return "term of sort "+Int::toString(sort)+": "+trm.toString();
1133 }
1134
getFormulaSymbolInterpretation(FormulaSymbol fs,unsigned firstArgSort)1135 Interpretation SMTLIB2::getFormulaSymbolInterpretation(FormulaSymbol fs, unsigned firstArgSort)
1136 {
1137 CALL("SMTLIB2::getFormulaSymbolInterpretation");
1138
1139 switch(fs) {
1140 case FS_LESS:
1141 switch(firstArgSort) {
1142 case Sorts::SRT_INTEGER:
1143 return Theory::INT_LESS;
1144 case Sorts::SRT_REAL:
1145 return Theory::REAL_LESS;
1146 default:
1147 break;
1148 }
1149 break;
1150 case FS_LESS_EQ:
1151 switch(firstArgSort) {
1152 case Sorts::SRT_INTEGER:
1153 return Theory::INT_LESS_EQUAL;
1154 case Sorts::SRT_REAL:
1155 return Theory::REAL_LESS_EQUAL;
1156 default:
1157 break;
1158 }
1159 break;
1160 case FS_GREATER:
1161 switch(firstArgSort) {
1162 case Sorts::SRT_INTEGER:
1163 return Theory::INT_GREATER;
1164 case Sorts::SRT_REAL:
1165 return Theory::REAL_GREATER;
1166 default:
1167 break;
1168 }
1169 break;
1170 case FS_GREATER_EQ:
1171 switch(firstArgSort) {
1172 case Sorts::SRT_INTEGER:
1173 return Theory::INT_GREATER_EQUAL;
1174 case Sorts::SRT_REAL:
1175 return Theory::REAL_GREATER_EQUAL;
1176 default:
1177 break;
1178 }
1179 break;
1180
1181 default:
1182 ASSERTION_VIOLATION;
1183 }
1184 USER_ERROR("invalid sort "+env.sorts->sortName(firstArgSort)+" for interpretation "+vstring(s_formulaSymbolNameStrings[fs]));
1185 }
1186
getUnaryMinusInterpretation(unsigned argSort)1187 Interpretation SMTLIB2::getUnaryMinusInterpretation(unsigned argSort)
1188 {
1189 CALL("SMTLIB2::getUnaryMinusInterpretation");
1190
1191 switch(argSort) {
1192 case Sorts::SRT_INTEGER:
1193 return Theory::INT_UNARY_MINUS;
1194 case Sorts::SRT_REAL:
1195 return Theory::REAL_UNARY_MINUS;
1196 default:
1197 USER_ERROR("invalid sort "+env.sorts->sortName(argSort)+" for interpretation -");
1198 }
1199 }
1200
getTermSymbolInterpretation(TermSymbol ts,unsigned firstArgSort)1201 Interpretation SMTLIB2::getTermSymbolInterpretation(TermSymbol ts, unsigned firstArgSort)
1202 {
1203 CALL("SMTLIB2::getTermSymbolInterpretation");
1204
1205 switch(ts) {
1206 case TS_MINUS:
1207 switch(firstArgSort) {
1208 case Sorts::SRT_INTEGER:
1209 return Theory::INT_MINUS;
1210 case Sorts::SRT_REAL:
1211 return Theory::REAL_MINUS;
1212 default:
1213 break;
1214 }
1215 break;
1216 case TS_PLUS:
1217 switch(firstArgSort) {
1218 case Sorts::SRT_INTEGER:
1219 return Theory::INT_PLUS;
1220 case Sorts::SRT_REAL:
1221 return Theory::REAL_PLUS;
1222 default:
1223 break;
1224 }
1225 break;
1226 case TS_MULTIPLY:
1227 switch(firstArgSort) {
1228 case Sorts::SRT_INTEGER:
1229 return Theory::INT_MULTIPLY;
1230 case Sorts::SRT_REAL:
1231 return Theory::REAL_MULTIPLY;
1232 default:
1233 break;
1234 }
1235 break;
1236
1237 case TS_DIVIDE:
1238 if (firstArgSort == Sorts::SRT_REAL)
1239 return Theory::REAL_QUOTIENT;
1240 break;
1241
1242 case TS_DIV:
1243 if (firstArgSort == Sorts::SRT_INTEGER)
1244 return Theory::INT_QUOTIENT_E;
1245 break;
1246
1247 default:
1248 ASSERTION_VIOLATION_REP(ts);
1249 }
1250 USER_ERROR("invalid sort "+env.sorts->sortName(firstArgSort)+" for interpretation "+vstring(s_termSymbolNameStrings[ts]));
1251 }
1252
complainAboutArgShortageOrWrongSorts(const vstring & symbolClass,LExpr * exp)1253 void SMTLIB2::complainAboutArgShortageOrWrongSorts(const vstring& symbolClass, LExpr* exp)
1254 {
1255 CALL("SMTLIB2::complainAboutArgShortageOrWrongSorts");
1256
1257 USER_ERROR("Not enough arguments or wrong sorts for "+symbolClass+" application "+exp->toString());
1258 }
1259
parseLetBegin(LExpr * exp)1260 void SMTLIB2::parseLetBegin(LExpr* exp)
1261 {
1262 CALL("SMTLIB2::parseLetBegin");
1263
1264 LOG2("parseLetBegin ",exp->toString());
1265
1266 ASS(exp->isList());
1267 LispListReader lRdr(exp->list);
1268
1269 // the let atom
1270 const vstring& theLetAtom = lRdr.readAtom();
1271 ASS_EQ(theLetAtom,LET);
1272
1273 // now, there should be a list of bindings
1274 LExprList* bindings = lRdr.readList();
1275
1276 // and the actual body term
1277 if (!lRdr.hasNext()) {
1278 complainAboutArgShortageOrWrongSorts(LET,exp);
1279 }
1280 LExpr* body = lRdr.readNext();
1281
1282 // and that's it
1283 lRdr.acceptEOL();
1284
1285 // now read the following bottom up:
1286
1287 // this will later create the actual let term and kill the lookup
1288 _todo.push(make_pair(PO_LET_END,exp));
1289
1290 // this will parse the let's body (in the context of the lookup)
1291 _todo.push(make_pair(PO_PARSE,body));
1292
1293 // this will create the lookup when all bindings' expressions are parsed (and their sorts known)
1294 _todo.push(make_pair(PO_LET_PREPARE_LOOKUP,exp));
1295
1296 // but we start by parsing the bound expressions
1297 LispListReader bindRdr(bindings);
1298 while (bindRdr.hasNext()) {
1299 LExprList* pair = bindRdr.readList();
1300 LispListReader pRdr(pair);
1301
1302 pRdr.readAtom(); // for now ignore the identifier
1303 LExpr* expr = pRdr.readNext();
1304
1305 _todo.push(make_pair(PO_PARSE,expr)); // just parse the expression
1306 pRdr.acceptEOL();
1307 }
1308 }
1309
parseLetPrepareLookup(LExpr * exp)1310 void SMTLIB2::parseLetPrepareLookup(LExpr* exp)
1311 {
1312 CALL("SMTLIB2::parseLetPrepareLookup");
1313 LOG2("PO_LET_PREPARE_LOOKUP",exp->toString());
1314
1315 // so we know it is let
1316 ASS(exp->isList());
1317 LispListReader lRdr(exp->list);
1318 const vstring& theLetAtom = lRdr.readAtom();
1319 ASS_EQ(theLetAtom,LET);
1320
1321 // with a list of bindings
1322 LispListReader bindRdr(lRdr.readList());
1323
1324 // corresponding results have already been parsed
1325 ParseResult* boundExprs = _results.end();
1326
1327 TermLookup* lookup = new TermLookup();
1328
1329 while (bindRdr.hasNext()) {
1330 LExprList* pair = bindRdr.readList();
1331 LispListReader pRdr(pair);
1332
1333 const vstring& cName = pRdr.readAtom();
1334 unsigned sort = (--boundExprs)->sort; // the should be big enough (
1335
1336 TermList trm;
1337 if (sort == Sorts::SRT_BOOL) {
1338 unsigned symb = env.signature->addFreshPredicate(0,"sLP");
1339 OperatorType* type = OperatorType::getPredicateType(0, nullptr);
1340 env.signature->getPredicate(symb)->setType(type);
1341
1342 Formula* atom = new AtomicFormula(Literal::create(symb,0,true,false,nullptr));
1343 trm = TermList(Term::createFormula(atom));
1344 } else {
1345 unsigned symb = env.signature->addFreshFunction (0,"sLF");
1346 OperatorType* type = OperatorType::getFunctionType(0, nullptr, sort);
1347 env.signature->getFunction(symb)->setType(type);
1348
1349 trm = TermList(Term::createConstant(symb));
1350 }
1351
1352 if (!lookup->insert(cName,make_pair(trm,sort))) {
1353 USER_ERROR("Multiple bindings of symbol "+cName+" in let expression "+exp->toString());
1354 }
1355 }
1356
1357 _scopes.push(lookup);
1358 }
1359
parseLetEnd(LExpr * exp)1360 void SMTLIB2::parseLetEnd(LExpr* exp)
1361 {
1362 CALL("SMTLIB2::parseLetEnd");
1363 LOG2("PO_LET_END ",exp->toString());
1364
1365 // so we know it is let
1366 ASS(exp->isList());
1367 LispListReader lRdr(exp->list);
1368 const vstring& theLetAtom = lRdr.readAtom();
1369 ASS_EQ(getBuiltInTermSymbol(theLetAtom),TS_LET);
1370
1371 // with a list of bindings
1372 LispListReader bindRdr(lRdr.readList());
1373
1374 TermLookup* lookup = _scopes.pop();
1375
1376 // there has to be the body result:
1377 TermList let;
1378 unsigned letSort = _results.pop().asTerm(let);
1379
1380 LOG2("LET body ",let.toString());
1381
1382 while (bindRdr.hasNext()) {
1383 LExprList* pair = bindRdr.readList();
1384 LispListReader pRdr(pair);
1385
1386 const vstring& cName = pRdr.readAtom();
1387 TermList boundExpr;
1388 _results.pop().asTerm(boundExpr);
1389
1390 LOG2("BOUND name ",cName);
1391 LOG2("BOUND term ",boundExpr.toString());
1392
1393 SortedTerm term;
1394 ALWAYS(lookup->find(cName,term));
1395 TermList exprTerm = term.first;
1396 unsigned exprSort = term.second;
1397
1398 unsigned symbol = 0;
1399 if (exprSort == Sorts::SRT_BOOL) { // it has to be formula term, with atomic formula
1400 symbol = exprTerm.term()->getSpecialData()->getFormula()->literal()->functor();
1401 } else {
1402 symbol = exprTerm.term()->functor();
1403 }
1404
1405 let = TermList(Term::createLet(symbol, nullptr, boundExpr, let, letSort));
1406 }
1407
1408 _results.push(ParseResult(letSort,let));
1409
1410 delete lookup;
1411 }
1412
parseQuantBegin(LExpr * exp)1413 void SMTLIB2::parseQuantBegin(LExpr* exp)
1414 {
1415 CALL("SMTLIB2::parseQuantBegin");
1416
1417 ASS(exp->isList());
1418 LispListReader lRdr(exp->list);
1419
1420 // the quant atom
1421 const vstring& theQuantAtom = lRdr.readAtom();
1422 ASS(theQuantAtom == FORALL || theQuantAtom == EXISTS);
1423
1424 // there should next be a list of sorted variables
1425 LispListReader varRdr(lRdr.readList());
1426
1427 TermLookup* lookup = new TermLookup();
1428
1429 while (varRdr.hasNext()) {
1430 LExprList* pair = varRdr.readList();
1431 LispListReader pRdr(pair);
1432
1433 vstring vName = pRdr.readAtom();
1434 unsigned vSort = declareSort(pRdr.readNext());
1435
1436 pRdr.acceptEOL();
1437
1438 if (!lookup->insert(vName,make_pair(TermList(_nextVar++,false),vSort))) {
1439 USER_ERROR("Multiple occurrence of variable "+vName+" in quantification "+exp->toString());
1440 }
1441 }
1442
1443 _scopes.push(lookup);
1444
1445 _todo.push(make_pair(PO_PARSE_APPLICATION,exp)); // will create the actual quantified formula and clear the lookup...
1446 _todo.push(make_pair(PO_PARSE,lRdr.readNext())); // ... from the only remaining argument, the body
1447 lRdr.acceptEOL();
1448 }
1449
1450 static const char* EXCLAMATION = "!";
1451
parseAnnotatedTerm(LExpr * exp)1452 void SMTLIB2::parseAnnotatedTerm(LExpr* exp)
1453 {
1454 CALL("SMTLIB2::parseAnnotatedTerm");
1455
1456 ASS(exp->isList());
1457 LispListReader lRdr(exp->list);
1458
1459 // the exclamation atom
1460 const vstring& theExclAtom = lRdr.readAtom();
1461 ASS_EQ(theExclAtom,EXCLAMATION);
1462
1463 LExpr* toParse = 0;
1464 if(lRdr.peekAtNext()->isAtom()){
1465 toParse = lRdr.next();
1466 }
1467 else{
1468 toParse = lRdr.readListExpr();
1469 }
1470
1471 static bool annotation_warning = false; // print warning only once
1472
1473 if (!annotation_warning) {
1474 //env.beginOutput();
1475 //env.out() << "% Warning: term annotations ignored!" << endl;
1476 //env.endOutput();
1477 annotation_warning = true;
1478 }
1479
1480 // we ignore the rest in lRdr (no matter the number of remaining arguments and their structure)
1481
1482 _todo.push(make_pair(PO_PARSE,toParse));
1483 }
1484
parseAsScopeLookup(const vstring & id)1485 bool SMTLIB2::parseAsScopeLookup(const vstring& id)
1486 {
1487 CALL("SMTLIB2::parseAsScopeLookup");
1488
1489 Scopes::Iterator sIt(_scopes);
1490 while (sIt.hasNext()) {
1491 TermLookup* lookup = sIt.next();
1492
1493 SortedTerm st;
1494 if (lookup->find(id,st)) {
1495 _results.push(ParseResult(st.second,st.first));
1496 return true;
1497 }
1498 }
1499
1500 return false;
1501 }
1502
parseAsSpecConstant(const vstring & id)1503 bool SMTLIB2::parseAsSpecConstant(const vstring& id)
1504 {
1505 CALL("SMTLIB2::parseAsSpecConstant");
1506
1507 if (StringUtils::isPositiveInteger(id)) {
1508 if (_numeralsAreReal) {
1509 goto real_constant; // just below
1510 }
1511
1512 unsigned symb = TPTP::addIntegerConstant(id,_overflow,false);
1513 TermList res = TermList(Term::createConstant(symb));
1514 _results.push(ParseResult(Sorts::SRT_INTEGER,res));
1515
1516 return true;
1517 }
1518
1519 if (StringUtils::isPositiveDecimal(id)) {
1520 real_constant:
1521
1522 unsigned symb = TPTP::addRealConstant(id,_overflow,false);
1523 TermList res = TermList(Term::createConstant(symb));
1524 _results.push(ParseResult(Sorts::SRT_REAL,res));
1525
1526 return true;
1527 }
1528
1529 return false;
1530 }
1531
parseAsUserDefinedSymbol(const vstring & id,LExpr * exp)1532 bool SMTLIB2::parseAsUserDefinedSymbol(const vstring& id,LExpr* exp)
1533 {
1534 CALL("SMTLIB2::parseAsUserDefinedSymbol");
1535
1536 DeclaredFunction fun;
1537 if (!_declaredFunctions.find(id,fun)) {
1538 return false;
1539 }
1540
1541 unsigned symbIdx = fun.first;
1542 bool isTrueFun = fun.second;
1543
1544 Signature::Symbol* symbol = isTrueFun ? env.signature->getFunction(symbIdx)
1545 : env.signature->getPredicate(symbIdx);
1546 OperatorType* type = isTrueFun ? symbol->fnType() : symbol->predType();
1547
1548 unsigned arity = symbol->arity();
1549
1550 static Stack<TermList> args;
1551 args.reset();
1552
1553 LOG2("DeclaredFunction of arity ",arity);
1554
1555 for (unsigned i = 0; i < arity; i++) {
1556 unsigned sort = type->arg(i);
1557
1558 TermList arg;
1559 if (_results.isEmpty() || _results.top().isSeparator() ||
1560 _results.pop().asTerm(arg) != sort) {
1561 complainAboutArgShortageOrWrongSorts("user defined symbol",exp);
1562 }
1563
1564 args.push(arg);
1565 }
1566
1567 if (isTrueFun) {
1568 unsigned sort = symbol->fnType()->result();
1569 TermList res = TermList(Term::create(symbIdx,arity,args.begin()));
1570 _results.push(ParseResult(sort,res));
1571 } else {
1572 Formula* res = new AtomicFormula(Literal::create(symbIdx,arity,true,false,args.begin()));
1573 _results.push(ParseResult(res));
1574 }
1575
1576 return true;
1577 }
1578
1579 static const char* BUILT_IN_SYMBOL = "built-in symbol";
1580
parseAsBuiltinFormulaSymbol(const vstring & id,LExpr * exp)1581 bool SMTLIB2::parseAsBuiltinFormulaSymbol(const vstring& id, LExpr* exp)
1582 {
1583 CALL("SMTLIB2::parseAsBuiltinFormulaSymbol");
1584
1585 FormulaSymbol fs = getBuiltInFormulaSymbol(id);
1586 switch (fs) {
1587 case FS_TRUE:
1588 _results.push(ParseResult(Formula::trueFormula()));
1589 return true;
1590 case FS_FALSE:
1591 _results.push(ParseResult(Formula::falseFormula()));
1592 return true;
1593 case FS_NOT:
1594 {
1595 if (_results.isEmpty() || _results.top().isSeparator()) {
1596 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1597 }
1598 Formula* argFla;
1599 if (!(_results.pop().asFormula(argFla))) {
1600 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1601 }
1602 Formula* res = new NegatedFormula(argFla);
1603 _results.push(ParseResult(res));
1604 return true;
1605 }
1606 case FS_AND:
1607 case FS_OR:
1608 {
1609 FormulaList* argLst = nullptr;
1610
1611 LOG1("FS_AND and FS_OR");
1612
1613 unsigned argcnt = 0;
1614 while (_results.isNonEmpty() && (!_results.top().isSeparator())) {
1615 argcnt++;
1616 Formula* argFla;
1617 if (!(_results.pop().asFormula(argFla))) {
1618 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1619 }
1620 FormulaList::push(argFla,argLst);
1621 }
1622
1623 if (argcnt < 1) { // TODO: officially, we might want to disallow singleton AND and OR, but they are harmless and appear in smtlib
1624 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1625 }
1626
1627 Formula* res;
1628 if (argcnt > 1) {
1629 res = new JunctionFormula( (fs==FS_AND) ? AND : OR, argLst);
1630 } else {
1631 res = argLst->head();
1632 FormulaList::destroy(argLst);
1633 }
1634 _results.push(ParseResult(res));
1635
1636 return true;
1637 }
1638 case FS_IMPLIES: // done in a right-assoc multiple-argument fashion
1639 case FS_XOR: // they say XOR should be left-associative, but semantically, it does not matter
1640 {
1641 Connective con = (fs==FS_IMPLIES) ? IMP : XOR;
1642
1643 static Stack<Formula*> args;
1644 ASS(args.isEmpty());
1645
1646 // put argument formulas on stack (reverses the order)
1647 while (_results.isNonEmpty() && (!_results.top().isSeparator())) {
1648 Formula* argFla;
1649 if (!(_results.pop().asFormula(argFla))) {
1650 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1651 }
1652 args.push(argFla);
1653 }
1654
1655 if (args.size() < 2) {
1656 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1657 }
1658
1659 // the last two go first
1660 Formula* arg_n = args.pop();
1661 Formula* arg_n_1 = args.pop();
1662 Formula* res = new BinaryFormula(con, arg_n_1, arg_n);
1663
1664 // keep on adding in a right-assoc way
1665 while(args.isNonEmpty()) {
1666 res = new BinaryFormula(con, args.pop(), res);
1667 }
1668
1669 _results.push(ParseResult(res));
1670
1671 return true;
1672 }
1673 // all the following are "chainable" and need to respect sorts
1674 case FS_EQ:
1675 case FS_LESS:
1676 case FS_LESS_EQ:
1677 case FS_GREATER:
1678 case FS_GREATER_EQ:
1679 {
1680 // read the first two arguments
1681 if (_results.isEmpty() || _results.top().isSeparator()) {
1682 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1683 }
1684 auto firstParseResult = _results.pop();
1685 if (_results.isEmpty() || _results.top().isSeparator()) {
1686 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1687 }
1688 auto secondParseResult = _results.pop();
1689 if (firstParseResult.sort != secondParseResult.sort)
1690 {
1691 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1692 }
1693
1694 Formula* lastConjunct;
1695 unsigned pred = 0;
1696 if (fs == FS_EQ) {
1697 if (firstParseResult.formula && secondParseResult.formula) {
1698 Formula* first;
1699 Formula* second;
1700 firstParseResult.asFormula(first);
1701 secondParseResult.asFormula(second);
1702 lastConjunct = new BinaryFormula(IFF, first, second);
1703 } else {
1704 TermList first;
1705 TermList second;
1706 firstParseResult.asTerm(first);
1707 secondParseResult.asTerm(second);
1708 lastConjunct = new AtomicFormula(Literal::createEquality(true, first, second, firstParseResult.sort));
1709 }
1710 } else {
1711 Interpretation intp = getFormulaSymbolInterpretation(fs,firstParseResult.sort);
1712 pred = env.signature->getInterpretingSymbol(intp);
1713 TermList first;
1714 TermList second;
1715 firstParseResult.asTerm(first);
1716 secondParseResult.asTerm(second);
1717 lastConjunct = new AtomicFormula(Literal::create2(pred,true,first,second));
1718 }
1719
1720 FormulaList* argLst = nullptr;
1721 // for every other argument ... pipelining
1722 while (_results.isEmpty() || !_results.top().isSeparator()) {
1723 auto nextParseResult = _results.pop();
1724 if (nextParseResult.sort != firstParseResult.sort) {
1725 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1726 }
1727 // store the old conjunct
1728 FormulaList::push(lastConjunct,argLst);
1729 // shift the arguments
1730 firstParseResult = secondParseResult;
1731 secondParseResult = nextParseResult;
1732 // create next conjunct
1733 if (fs == FS_EQ) {
1734 if (firstParseResult.formula && secondParseResult.formula) {
1735 Formula* first;
1736 Formula* second;
1737 firstParseResult.asFormula(first);
1738 secondParseResult.asFormula(second);
1739 lastConjunct = new BinaryFormula(IFF, first, second);
1740 } else {
1741 TermList first;
1742 TermList second;
1743 firstParseResult.asTerm(first);
1744 secondParseResult.asTerm(second);
1745 lastConjunct = new AtomicFormula(Literal::createEquality(true, first, second, firstParseResult.sort));
1746 }
1747 } else {
1748 Interpretation intp = getFormulaSymbolInterpretation(fs,firstParseResult.sort);
1749 pred = env.signature->getInterpretingSymbol(intp);
1750 TermList first;
1751 TermList second;
1752 firstParseResult.asTerm(first);
1753 secondParseResult.asTerm(second);
1754 lastConjunct = new AtomicFormula(Literal::create2(pred,true,first,second));
1755 }
1756 }
1757 if (argLst == nullptr) { // there were only two arguments, let's return lastConjunct
1758 _results.push(lastConjunct);
1759 } else {
1760 // add the last lastConjunct created (pipelining)
1761 FormulaList::push(lastConjunct,argLst);
1762 // create the actual conjunction
1763 Formula* res = new JunctionFormula( AND, argLst);
1764 _results.push(ParseResult(res));
1765 }
1766
1767 return true;
1768 }
1769 case FS_DISTINCT:
1770 {
1771 static Stack<TermList> args;
1772 args.reset();
1773
1774 // read the first argument and its sort
1775 TermList first;
1776 if (_results.isEmpty() || _results.top().isSeparator()) {
1777 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1778 }
1779 unsigned sort = _results.pop().asTerm(first);
1780
1781 args.push(first);
1782
1783 // put remaining arguments on stack (reverses the order, which does not matter)
1784 while (_results.isNonEmpty() && (!_results.top().isSeparator())) {
1785 TermList argTerm;
1786 if (_results.pop().asTerm(argTerm) != sort) {
1787 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1788 }
1789 args.push(argTerm);
1790 }
1791
1792 if (args.size() < 2) {
1793 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1794 }
1795
1796 Formula* res;
1797 if(args.size()==2) { // if there are 2 just create a disequality
1798 res = new AtomicFormula(Literal::createEquality(false,args[0],args[1],sort));
1799 } else { // Otherwise create a formula list of disequalities
1800 FormulaList* diseqs = nullptr;
1801
1802 for(unsigned i=0;i<args.size();i++){
1803 for(unsigned j=0;j<i;j++){
1804 Formula* new_dis = new AtomicFormula(Literal::createEquality(false,args[i],args[j],sort));
1805 FormulaList::push(new_dis,diseqs);
1806 }
1807 }
1808
1809 res = new JunctionFormula(AND, diseqs);
1810 }
1811
1812 _results.push(res);
1813
1814 return true;
1815 }
1816 case FS_IS_INT:
1817 {
1818 TermList arg;
1819 if (_results.isEmpty() || _results.top().isSeparator() ||
1820 _results.pop().asTerm(arg) != Sorts::SRT_REAL) {
1821 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1822 }
1823
1824 unsigned pred = env.signature->getInterpretingSymbol(Theory::REAL_IS_INT);
1825 Formula* res = new AtomicFormula(Literal::create1(pred,true,arg));
1826
1827 _results.push(res);
1828
1829 return true;
1830 }
1831 case FS_EXISTS:
1832 case FS_FORALL:
1833 {
1834 Formula* argFla;
1835 if (_results.isEmpty() || _results.top().isSeparator() ||
1836 !(_results.pop().asFormula(argFla))) {
1837 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1838 }
1839
1840 Formula::VarList* qvars = nullptr;
1841 Formula::SortList* qsorts = nullptr;
1842
1843 TermLookup::Iterator varIt(*_scopes.top());
1844 while(varIt.hasNext()) {
1845 SortedTerm vTerm = varIt.next();
1846 unsigned varIdx = vTerm.first.var();
1847 unsigned sort = vTerm.second;
1848 Formula::VarList::push(varIdx, qvars);
1849 Formula::SortList::push(sort,qsorts);
1850 }
1851 delete _scopes.pop();
1852
1853 Formula* res = new QuantifiedFormula((fs==FS_EXISTS) ? Kernel::EXISTS : Kernel::FORALL, qvars, qsorts, argFla);
1854
1855 _results.push(ParseResult(res));
1856 return true;
1857 }
1858
1859 default:
1860 ASS_EQ(fs,FS_USER_PRED_SYMBOL);
1861 return false;
1862 }
1863 }
1864
parseAsBuiltinTermSymbol(const vstring & id,LExpr * exp)1865 bool SMTLIB2::parseAsBuiltinTermSymbol(const vstring& id, LExpr* exp)
1866 {
1867 CALL("SMTLIB2::parseAsBuiltinTermSymbol");
1868
1869 // try built-in term symbols
1870 TermSymbol ts = getBuiltInTermSymbol(id);
1871 switch(ts) {
1872 case TS_ITE:
1873 {
1874 Formula* cond;
1875 if (_results.isEmpty() || _results.top().isSeparator() ||
1876 !(_results.pop().asFormula(cond))) {
1877 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1878 }
1879 TermList thenBranch;
1880 if (_results.isEmpty() || _results.top().isSeparator()){
1881 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1882 }
1883 unsigned sort = _results.pop().asTerm(thenBranch);
1884 TermList elseBranch;
1885 if (_results.isEmpty() || _results.top().isSeparator() ||
1886 _results.pop().asTerm(elseBranch) != sort){
1887 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1888 }
1889
1890 TermList res = TermList(Term::createITE(cond, thenBranch, elseBranch, sort));
1891
1892 _results.push(ParseResult(sort,res));
1893 return true;
1894 }
1895 case TS_TO_REAL:
1896 {
1897 TermList theInt;
1898 if (_results.isEmpty() || _results.top().isSeparator() ||
1899 _results.pop().asTerm(theInt) != Sorts::SRT_INTEGER) {
1900 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1901 }
1902
1903 unsigned fun = env.signature->getInterpretingSymbol(Theory::INT_TO_REAL);
1904 TermList res = TermList(Term::create1(fun,theInt));
1905
1906 _results.push(ParseResult(Sorts::SRT_REAL,res));
1907 return true;
1908 }
1909 case TS_TO_INT:
1910 {
1911 TermList theReal;
1912 if (_results.isEmpty() || _results.top().isSeparator() ||
1913 _results.pop().asTerm(theReal) != Sorts::SRT_REAL) {
1914 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1915 }
1916
1917 unsigned fun = env.signature->getInterpretingSymbol(Theory::REAL_TO_INT);
1918 TermList res = TermList(Term::create1(fun,theReal));
1919
1920 _results.push(ParseResult(Sorts::SRT_INTEGER,res));
1921 return true;
1922 }
1923 case TS_SELECT:
1924 {
1925 TermList theArray;
1926 if (_results.isEmpty() || _results.top().isSeparator()) {
1927 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1928 }
1929 unsigned arraySortIdx = _results.pop().asTerm(theArray);
1930 if (!env.sorts->isOfStructuredSort(arraySortIdx,Sorts::StructuredSort::ARRAY)) {
1931 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1932 }
1933 Sorts::ArraySort* arraySort = env.sorts->getArraySort(arraySortIdx);
1934
1935 TermList theIndex;
1936 if (_results.isEmpty() || _results.top().isSeparator() ||
1937 _results.pop().asTerm(theIndex) != arraySort->getIndexSort()) {
1938 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1939 }
1940
1941 if (arraySort->getInnerSort() == Sorts::SRT_BOOL) {
1942 OperatorType* predType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_BOOL_SELECT);
1943 unsigned pred = env.signature->getInterpretingSymbol(Theory::ARRAY_BOOL_SELECT,predType);
1944
1945 Formula* res = new AtomicFormula(Literal::create2(pred,true,theArray,theIndex));
1946
1947 _results.push(ParseResult(res));
1948 } else {
1949 OperatorType* funType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_SELECT);
1950 unsigned fun = env.signature->getInterpretingSymbol(Theory::ARRAY_SELECT,funType);
1951
1952 TermList res = TermList(Term::create2(fun,theArray,theIndex));
1953
1954 _results.push(ParseResult(arraySort->getInnerSort(),res));
1955 }
1956
1957 return true;
1958 }
1959 case TS_STORE:
1960 {
1961 TermList theArray;
1962 if (_results.isEmpty() || _results.top().isSeparator()) {
1963 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1964 }
1965 unsigned arraySortIdx = _results.pop().asTerm(theArray);
1966 if (!env.sorts->isOfStructuredSort(arraySortIdx,Sorts::StructuredSort::ARRAY)) {
1967 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1968 }
1969 Sorts::ArraySort* arraySort = env.sorts->getArraySort(arraySortIdx);
1970
1971 TermList theIndex;
1972 if (_results.isEmpty() || _results.top().isSeparator() ||
1973 _results.pop().asTerm(theIndex) != arraySort->getIndexSort()) {
1974 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1975 }
1976
1977 TermList theValue;
1978 if (_results.isEmpty() || _results.top().isSeparator() ||
1979 _results.pop().asTerm(theValue) != arraySort->getInnerSort()) {
1980 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1981 }
1982
1983 OperatorType* funType = Theory::getArrayOperatorType(arraySortIdx,Theory::ARRAY_STORE);
1984 unsigned fun = env.signature->getInterpretingSymbol(Theory::ARRAY_STORE,funType);
1985
1986 TermList args[] = {theArray, theIndex, theValue};
1987 TermList res = TermList(Term::Term::create(fun, 3, args));
1988
1989 _results.push(ParseResult(arraySortIdx,res));
1990
1991 return true;
1992 }
1993 case TS_ABS:
1994 {
1995 TermList theInt;
1996 if (_results.isEmpty() || _results.top().isSeparator() ||
1997 _results.pop().asTerm(theInt) != Sorts::SRT_INTEGER) {
1998 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
1999 }
2000
2001 unsigned fun = env.signature->getInterpretingSymbol(Theory::INT_ABS);
2002 TermList res = TermList(Term::create1(fun,theInt));
2003
2004 _results.push(ParseResult(Sorts::SRT_INTEGER,res));
2005
2006 return true;
2007 }
2008 case TS_MOD:
2009 {
2010 TermList int1, int2;
2011 if (_results.isEmpty() || _results.top().isSeparator() || _results.pop().asTerm(int1) != Sorts::SRT_INTEGER ||
2012 _results.isEmpty() || _results.top().isSeparator() || _results.pop().asTerm(int2) != Sorts::SRT_INTEGER) {
2013 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
2014 }
2015
2016 unsigned fun = env.signature->getInterpretingSymbol(Theory::INT_REMAINDER_E); // TS_MOD is the always positive remainder, therefore INT_REMAINDER_E
2017 TermList res = TermList(Term::create2(fun,int1,int2));
2018
2019 _results.push(ParseResult(Sorts::SRT_INTEGER,res));
2020
2021 return true;
2022 }
2023 case TS_MULTIPLY:
2024 case TS_PLUS:
2025 case TS_MINUS:
2026 case TS_DIVIDE:
2027 case TS_DIV:
2028 {
2029 // read the first argument
2030 TermList first;
2031 if (_results.isEmpty() || _results.top().isSeparator()) {
2032 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
2033 }
2034 unsigned sort = _results.pop().asTerm(first);
2035
2036 if (_results.isEmpty() || _results.top().isSeparator()) {
2037 if (ts == TS_MINUS) { // unary minus
2038 Interpretation intp = getUnaryMinusInterpretation(sort);
2039 unsigned fun = env.signature->getInterpretingSymbol(intp);
2040
2041 TermList res = TermList(Term::create1(fun,first));
2042
2043 _results.push(ParseResult(sort,res));
2044
2045 return true;
2046 } else {
2047 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp); // we need at least two arguments otherwise
2048 }
2049 }
2050
2051 Interpretation intp = getTermSymbolInterpretation(ts,sort);
2052 unsigned fun = env.signature->getInterpretingSymbol(intp);
2053
2054 TermList second;
2055 if (_results.pop().asTerm(second) != sort) {
2056 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
2057 }
2058
2059 TermList res = TermList(Term::create2(fun,first,second));
2060 while (_results.isNonEmpty() && !_results.top().isSeparator()) {
2061 TermList another;
2062 if (_results.pop().asTerm(another) != sort) {
2063 complainAboutArgShortageOrWrongSorts(BUILT_IN_SYMBOL,exp);
2064 }
2065
2066 res = TermList(Term::create2(fun,res,another));
2067 }
2068 _results.push(ParseResult(sort,res));
2069
2070 return true;
2071 }
2072 default:
2073 ASS_EQ(ts,TS_USER_FUNCTION);
2074 return false;
2075 }
2076 }
2077
2078 static const char* UNDERSCORE = "_";
2079
parseRankedFunctionApplication(LExpr * exp)2080 void SMTLIB2::parseRankedFunctionApplication(LExpr* exp)
2081 {
2082 CALL("SMTLIB2::parseRankedFunctionApplication");
2083
2084 ASS(exp->isList());
2085 LispListReader lRdr(exp->list);
2086 LExpr* head = lRdr.readNext();
2087 ASS(head->isList());
2088 LispListReader headRdr(head);
2089
2090 headRdr.acceptAtom(UNDERSCORE);
2091
2092 if(headRdr.tryAcceptAtom("divisible")){
2093
2094 const vstring& numeral = headRdr.readAtom();
2095
2096 if (!StringUtils::isPositiveInteger(numeral)) {
2097 USER_ERROR("Expected numeral as an argument of a ranked function in "+head->toString());
2098 }
2099
2100 unsigned divisorSymb = TPTP::addIntegerConstant(numeral,_overflow,false);
2101 TermList divisorTerm = TermList(Term::createConstant(divisorSymb));
2102
2103 TermList arg;
2104 if (_results.isEmpty() || _results.top().isSeparator() ||
2105 _results.pop().asTerm(arg) != Sorts::SRT_INTEGER) {
2106 complainAboutArgShortageOrWrongSorts("ranked function symbol",exp);
2107 }
2108
2109 unsigned pred = env.signature->getInterpretingSymbol(Theory::INT_DIVIDES);
2110 env.signature->recordDividesNvalue(divisorTerm);
2111
2112 Formula* res = new AtomicFormula(Literal::create2(pred,true,divisorTerm,arg));
2113
2114 _results.push(ParseResult(res));
2115 }
2116 else if(headRdr.tryAcceptAtom("is")){
2117 // discriminator predicate for term algebras
2118 const vstring& consName = headRdr.readAtom();
2119
2120 if (_declaredFunctions.find(consName)) {
2121 DeclaredFunction& f = _declaredFunctions.get(consName);
2122 if (f.second) {
2123 TermAlgebraConstructor* c = env.signature->getTermAlgebraConstructor(f.first);
2124 if (c) /* else the symbol is not a TA constructor */ {
2125
2126 unsigned sort = env.signature->getFunction(f.first)->fnType()->result();
2127 if (!c->hasDiscriminator()) {
2128 // add discriminator predicate
2129 bool added;
2130 unsigned pred = env.signature->addPredicate(c->discriminatorName(), 1, added);
2131 ASS(added);
2132 OperatorType* type = OperatorType::getPredicateType({ sort });
2133 env.signature->getPredicate(pred)->setType(type);
2134 c->addDiscriminator(pred);
2135 // this predicate is not declare for the parser as it has a reserved name
2136 }
2137 TermList arg;
2138 if (_results.isEmpty() || _results.top().isSeparator() ||
2139 _results.pop().asTerm(arg) != sort) {
2140 complainAboutArgShortageOrWrongSorts("ranked function symbol",exp);
2141 }
2142 Formula* res = new AtomicFormula(Literal::create1(c->discriminator(),true,arg));
2143
2144 _results.push(ParseResult(res));
2145 return;
2146 }
2147 }
2148 }
2149 USER_ERROR("'"+consName+"' is not a datatype constructor");
2150 }
2151 else{
2152 USER_ERROR("Ranked function application "+headRdr.readAtom()+" not known");
2153 }
2154
2155 }
2156
parseTermOrFormula(LExpr * body)2157 SMTLIB2::ParseResult SMTLIB2::parseTermOrFormula(LExpr* body)
2158 {
2159 CALL("SMTLIB2::parseTermOrFormula");
2160
2161 ASS(_todo.isEmpty());
2162 ASS(_results.isEmpty());
2163
2164 _todo.push(make_pair(PO_PARSE,body));
2165
2166 while (_todo.isNonEmpty()) {
2167 /*
2168 cout << "Results:" << endl;
2169 for (unsigned i = 0; i < results.size(); i++) {
2170 cout << results[i].toString() << endl;
2171 }
2172 cout << "---" << endl;
2173 */
2174
2175 pair<ParseOperation,LExpr*> cur = _todo.pop();
2176 ParseOperation op = cur.first;
2177 LExpr* exp = cur.second;
2178
2179 switch (op) {
2180 case PO_PARSE: {
2181 if (exp->isList()) {
2182 LispListReader lRdr(exp->list);
2183
2184 // schedule arity check
2185 _results.push(ParseResult()); // separator into results
2186 _todo.push(make_pair(PO_CHECK_ARITY,exp)); // check as a todo (exp for error reporting)
2187
2188 // special treatment of some tokens
2189 LExpr* fst = lRdr.readNext();
2190 if (fst->isAtom()) {
2191 vstring& id = fst->str;
2192
2193 if (id == FORALL || id == EXISTS) {
2194 parseQuantBegin(exp);
2195 continue;
2196 }
2197
2198 if (id == LET) {
2199 parseLetBegin(exp);
2200 continue;
2201 }
2202
2203 if (id == EXCLAMATION) {
2204 parseAnnotatedTerm(exp);
2205 continue;
2206 }
2207
2208 if (id == UNDERSCORE) {
2209 USER_ERROR("Indexed identifiers in general term position are not supported: "+exp->toString());
2210
2211 // we only support indexed identifiers as functors applied to something (see just below)
2212 }
2213 } else {
2214 // this has to be an UNDERSCORE, otherwise we error later when we PO_PARSE_APPLICATION
2215 }
2216
2217 // this handles the general function-to-arguments application:
2218
2219 _todo.push(make_pair(PO_PARSE_APPLICATION,exp));
2220 // and all the other arguments too
2221 while (lRdr.hasNext()) {
2222 _todo.push(make_pair(PO_PARSE,lRdr.next()));
2223 }
2224
2225 continue;
2226 }
2227
2228 // INTENTIONAL FALL-THROUGH FOR ATOMS
2229 }
2230 case PO_PARSE_APPLICATION: { // the arguments have already been parsed
2231 vstring id;
2232 if (exp->isAtom()) { // the fall-through case
2233 id = exp->str;
2234 } else {
2235 ASS(exp->isList());
2236 LispListReader lRdr(exp->list);
2237
2238 LExpr* head = lRdr.readNext();
2239
2240 if (head->isList()) {
2241 parseRankedFunctionApplication(exp);
2242 continue;
2243 }
2244 ASS(head->isAtom());
2245 id = head->str;
2246 }
2247
2248 if (parseAsScopeLookup(id)) {
2249 continue;
2250 }
2251
2252 if (parseAsSpecConstant(id)) {
2253 continue;
2254 }
2255
2256 if (parseAsUserDefinedSymbol(id,exp)) {
2257 continue;
2258 }
2259
2260 if (parseAsBuiltinFormulaSymbol(id,exp)) {
2261 continue;
2262 }
2263
2264 if (parseAsBuiltinTermSymbol(id,exp)) {
2265 continue;
2266 }
2267
2268 USER_ERROR("Unrecognized term identifier "+id);
2269 }
2270 case PO_CHECK_ARITY: {
2271 LOG1("PO_CHECK_ARITY");
2272
2273 ASS_GE(_results.size(),2);
2274 ParseResult true_result = _results.pop();
2275 ParseResult separator = _results.pop();
2276
2277 if (true_result.isSeparator() || !separator.isSeparator()) {
2278 USER_ERROR("Too many arguments in "+exp->toString());
2279 }
2280 _results.push(true_result);
2281
2282 continue;
2283 }
2284 case PO_LET_PREPARE_LOOKUP:
2285 parseLetPrepareLookup(exp);
2286 continue;
2287 case PO_LET_END:
2288 parseLetEnd(exp);
2289 continue;
2290 }
2291 }
2292
2293 if (_results.size() == 1) {
2294 return _results.pop();
2295 } else {
2296 USER_ERROR("Malformed term expression "+body->toString());
2297 }
2298 }
2299
readAssert(LExpr * body)2300 void SMTLIB2::readAssert(LExpr* body)
2301 {
2302 CALL("SMTLIB2::readAssert");
2303
2304 _nextVar = 0;
2305 ASS(_scopes.isEmpty());
2306
2307 ParseResult res = parseTermOrFormula(body);
2308
2309 Formula* fla;
2310 if (!res.asFormula(fla)) {
2311 USER_ERROR("Asserted expression of non-boolean sort "+body->toString());
2312 }
2313
2314 FormulaUnit* fu = new FormulaUnit(fla, FromInput(UnitInputType::ASSUMPTION));
2315 UnitList::push(fu, _formulas);
2316 }
2317
readAssertNot(LExpr * body)2318 void SMTLIB2::readAssertNot(LExpr* body)
2319 {
2320 CALL("SMTLIB2::readAssert");
2321
2322 _nextVar = 0;
2323 ASS(_scopes.isEmpty());
2324
2325 ParseResult res = parseTermOrFormula(body);
2326
2327 Formula* fla;
2328 if (!res.asFormula(fla)) {
2329 USER_ERROR("Asserted expression of non-boolean sort "+body->toString());
2330 }
2331
2332 FormulaUnit* fu = new FormulaUnit(fla, FromInput(UnitInputType::CONJECTURE));
2333 fu = new FormulaUnit(new NegatedFormula(fla),
2334 FormulaTransformation(InferenceRule::NEGATED_CONJECTURE, fu));
2335 UnitList::push(fu, _formulas);
2336 }
2337
colorSymbol(const vstring & name,Color color)2338 void SMTLIB2::colorSymbol(const vstring& name, Color color)
2339 {
2340 CALL("SMTLIB2::colorSymbol");
2341
2342 if (!_declaredFunctions.find(name)) {
2343 USER_ERROR("'"+name+"' is not a user symbol");
2344 }
2345 DeclaredFunction& f = _declaredFunctions.get(name);
2346
2347 env.colorUsed = true;
2348
2349 Signature::Symbol* sym = f.second
2350 ? env.signature->getFunction(f.first)
2351 : env.signature->getPredicate(f.first);
2352
2353 sym->addColor(color);
2354 }
2355
2356 }
2357