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