1 
2 /*
3  * File SMTLIB.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 
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 
41 #include "SMTLIB.hpp"
42 
43 namespace Parse
44 {
45 
SMTLIB(const Options & opts,Mode mode)46 SMTLIB::SMTLIB(const Options& opts, Mode mode)
47 : _lispAssumptions(0),
48   _lispFormula(0),
49   _definitions(0),
50   _formulas(0),
51   _mode(mode),
52   _treatIntsAsReals(opts.smtlibConsiderIntsReal()),
53   _fletAsDefinition(opts.smtlibFletAsDefinition()),
54   _introducedSymbolColor(COLOR_TRANSPARENT),
55 
56   _array1Sort(0),
57   _array2Sort(0)
58 {
59   CALL("SMTLIB::SMTLIB");
60 
61 #if VDEBUG
62   _haveParsed = false;
63 #endif
64 }
65 
parse(istream & str)66 void SMTLIB::parse(istream& str)
67 {
68   CALL("SMTLIB::parse(istream&)");
69 
70   LispLexer lex(str);
71   LispParser lpar(lex);
72   LExpr* expr = lpar.parse();
73 
74   LispListReader eRdr(expr);
75   parse(eRdr.readListExpr());
76   eRdr.acceptEOL();
77 }
78 
79 /**
80  * @param bench lisp list having atom "benchmark" as the first element
81  */
parse(LExpr * bench)82 void SMTLIB::parse(LExpr* bench)
83 {
84   CALL("SMTLIB::parse(LExpr*)");
85 
86   ASS(!_haveParsed);
87   ASS(bench->isList());
88 #if VDEBUG
89   _haveParsed = true;
90 #endif
91 
92   readBenchmark(bench->list);
93 
94 
95   if(_mode==READ_BENCHMARK) { return; }
96 
97   doSortDeclarations();
98 
99 
100   if(_mode==DECLARE_SORTS) { return; }
101 
102 
103   doFunctionDeclarations();
104 
105   if(_mode==DECLARE_SYMBOLS) { return; }
106   ASS(_mode==BUILD_FORMULA);
107 
108 
109 
110 
111   buildFormula();
112 }
113 
readBenchmark(LExprList * bench)114 void SMTLIB::readBenchmark(LExprList* bench)
115 {
116 
117   LispListReader bRdr(bench);
118   bRdr.acceptAtom("benchmark");
119   _benchName = bRdr.readAtom();
120 
121   while(bRdr.hasNext()) {
122     if(bRdr.tryAcceptAtom(":status")) {
123       _statusStr = bRdr.readAtom();
124     }
125     else if(bRdr.tryAcceptAtom(":source")) {
126       if(!bRdr.tryAcceptCurlyBrackets()) {
127 	bRdr.acceptAtom();
128       }
129     }
130     else if(bRdr.tryAcceptAtom(":category")) {
131       if(!bRdr.tryAcceptCurlyBrackets()) {
132 	bRdr.acceptAtom();
133       }
134     }
135     else if(bRdr.tryAcceptAtom(":difficulty")) {
136       if(!bRdr.tryAcceptCurlyBrackets()) {
137 	bRdr.acceptAtom();
138       }
139     }
140     else if(bRdr.tryAcceptAtom(":logic")) {
141       bRdr.acceptAtom();
142     }
143     else if(bRdr.tryAcceptAtom(":extrasorts")) {
144       LispListReader declsListRdr(bRdr.readList());
145       while(declsListRdr.hasNext()) {
146 	readSort(declsListRdr.readAtom());
147       }
148     }
149     else if(bRdr.tryAcceptAtom(":extrafuns")) {
150       LispListReader declsListRdr(bRdr.readList());
151       while(declsListRdr.hasNext()) {
152 	readFunction(declsListRdr.readList());
153       }
154     }
155     else if(bRdr.tryAcceptAtom(":extrapreds")) {
156       LispListReader declsListRdr(bRdr.readList());
157       while(declsListRdr.hasNext()) {
158 	readPredicate(declsListRdr.readList());
159       }
160     }
161     else if(bRdr.tryAcceptAtom(":assumption")) {
162       LExprList::push(bRdr.readNext(), _lispAssumptions);
163     }
164     else if(bRdr.tryAcceptAtom(":formula")) {
165       if(_lispFormula) {
166 	USER_ERROR("two :formula elements in one benchmark");
167       }
168       _lispFormula = bRdr.readNext();
169     }
170     else {
171       //this will always give an error as we have bRdr.hasNext() set to true
172       bRdr.acceptEOL();
173     }
174   }
175 }
176 
readSort(vstring name)177 void SMTLIB::readSort(vstring name)
178 {
179   CALL("SMTLIB::readSort");
180 
181   BuiltInSorts bsym = getBuiltInSort(name);
182   if(bsym!=BS_INVALID) {
183     USER_ERROR("Cannot declare built-in sort: "+name);
184   }
185   _userSorts.push(name);
186 }
187 
readFunction(LExprList * decl)188 void SMTLIB::readFunction(LExprList* decl)
189 {
190   CALL("SMTLIB::declareFunction");
191 
192 
193   LispListReader dRdr(decl);
194   vstring name = dRdr.readAtom();
195 
196   LExpr* nextSym = dRdr.readNext();
197 
198   static Stack<vstring> argSorts;
199   argSorts.reset();
200 
201 
202   if (nextSym->isAtom()) {
203      vstring type = nextSym->str;
204      argSorts.push(type);
205      while(dRdr.hasNext()) {
206           argSorts.push(dRdr.readAtom());
207       }
208   }
209   else {if (nextSym->isList()) {
210         //for now we only treat one-dimensional integer arrays, given in SMT as (Array Int Int)
211         LExprList* l= nextSym->list;
212         vstring type = l->head()->toString();
213         if (type != "Array") {USER_ERROR("unknown non-atomic sort (we only handle arrays)");}
214         type = "Array1";
215         //type 1
216         if (!l->tail()) {	USER_ERROR("non-atomic sort has no domain and range");}
217         l=l->tail();
218         vstring tmpArg1 = l->head()->toString();
219       if (tmpArg1!= "Int") {USER_ERROR("Array indeces are not int");}
220         if (!l->tail()) {	USER_ERROR("non-atomic sort has no range sort");}
221         l=l->tail();
222         vstring tmpArg2 = l->head()->toString();
223       if (tmpArg2!= "Int") {USER_ERROR("Array elements are not int (we only handle arrays of int)");}
224         argSorts.push(type);
225         //read the leftover declaration
226         while(dRdr.hasNext()) {
227           argSorts.push(dRdr.readAtom());
228        }
229         //argSorts.push(tmpArg2);
230     }
231   }
232     vstring domainSort = argSorts.pop();
233   _funcs.push(FunctionInfo(name, argSorts, domainSort));
234 }
235 
readPredicate(LExprList * decl)236 void SMTLIB::readPredicate(LExprList* decl)
237 {
238   CALL("SMTLIB::declarePredicate");
239 
240   LispListReader dRdr(decl);
241   vstring name = dRdr.readAtom();
242 
243   static Stack<vstring> argSorts;
244   argSorts.reset();
245   while(dRdr.hasNext()) {
246     argSorts.push(dRdr.readAtom());
247   }
248 
249   _funcs.push(FunctionInfo(name, argSorts, "$o"));
250 }
251 
getSort(BuiltInSorts srt)252 unsigned SMTLIB::getSort(BuiltInSorts srt)
253 {
254   CALL("SMTLIB::getSort(BuiltInSorts)");
255 
256   switch(srt) {
257   case BS_ARRAY1:
258     if(!_array1Sort) {
259         _array1Sort = env.sorts->addArraySort(Sorts::SRT_INTEGER,Sorts::SRT_INTEGER);
260         ASS(_array1Sort);
261     }
262     return _array1Sort;
263   case BS_ARRAY2:
264     if(!_array2Sort) {
265       _array2Sort = env.sorts->addArraySort(Sorts::SRT_INTEGER,getSort(BS_ARRAY1));
266       ASS(_array2Sort);
267     }
268     return _array2Sort;
269   case BS_INT:
270     return _treatIntsAsReals ? Sorts::SRT_REAL : Sorts::SRT_INTEGER;
271   case BS_REAL:
272     return Sorts::SRT_REAL;
273   case BS_U:
274     return Sorts::SRT_DEFAULT;
275   default:
276     ASSERTION_VIOLATION;
277   }
278 }
279 
getSort(vstring name)280 unsigned SMTLIB::getSort(vstring name)
281 {
282   CALL("SMTLIB::getSort");
283 
284   BuiltInSorts bsym = getBuiltInSort(name);
285 
286   if(bsym==BS_INVALID) {
287     unsigned idx;
288     if(!env.sorts->findSort(name, idx)) {
289       USER_ERROR("undeclared sort: "+name);
290     }
291     return idx;
292   }
293   else {
294     return getSort(bsym);
295   }
296 }
297 
doSortDeclarations()298 void SMTLIB::doSortDeclarations()
299 {
300   CALL("SMTLIB::doSortDeclarations");
301 
302   Stack<vstring>::Iterator srtIt(_userSorts);
303   while(srtIt.hasNext()) {
304     vstring sortName = srtIt.next();
305     env.sorts->addSort(sortName,false);
306   }
307 }
308 
getSymbolType(const FunctionInfo & fnInfo)309 OperatorType* SMTLIB::getSymbolType(const FunctionInfo& fnInfo)
310 {
311   CALL("SMTLIB::getSymbolType");
312 
313 
314   unsigned arity = fnInfo.argSorts.size();
315   unsigned rangeSort = getSort(fnInfo.rangeSort);
316 
317   static Stack<unsigned> argSorts;
318   argSorts.reset();
319 
320   Stack<vstring>::BottomFirstIterator argSortIt(fnInfo.argSorts);
321   while(argSortIt.hasNext()) {
322     vstring argSortName = argSortIt.next();
323     argSorts.push(getSort(argSortName));
324   }
325 
326   return OperatorType::getFunctionType(arity, argSorts.begin(), rangeSort);
327 }
328 
doFunctionDeclarations()329 void SMTLIB::doFunctionDeclarations()
330 {
331   CALL("SMTLIB::doFunctionDeclarations");
332 
333   unsigned funCnt = _funcs.size();
334   for(unsigned i=0; i<funCnt; i++) {
335     FunctionInfo& fnInfo = _funcs[i];
336     unsigned arity = fnInfo.argSorts.size();
337 
338     OperatorType* type = getSymbolType(fnInfo);
339     bool isPred = type->isPredicateType();
340 
341     unsigned symNum;
342     Signature::Symbol* sym;
343     if(isPred) {
344       bool added;
345       symNum = env.signature->addPredicate(fnInfo.name, arity, added);
346       sym = env.signature->getPredicate(symNum);
347       if(added) {
348 	sym->setType(type);
349       }
350       else {
351 	if((*sym->predType())!=(*type)) {
352 	  USER_ERROR("incompatible type for predicate "+fnInfo.name);
353 	}
354       }
355     }
356     else {
357      bool added;
358       symNum = env.signature->addFunction(fnInfo.name, arity, added);
359       sym = env.signature->getFunction(symNum);
360       if(added) {
361 	sym->setType(type);
362       }
363       else {
364 	if((*sym->fnType())!=(*type)) {
365 	  USER_ERROR("incompatible type for function "+fnInfo.name);
366 	}
367       }
368     }
369   }
370 }
371 
372 ///////////////////////
373 // Formula building
374 //
375 
376 const char * SMTLIB::s_builtInSortNameStrings[] = {
377     "Array1",
378     "Array2",
379     "Int",
380     "Real",
381     "U"
382 };
383 
getBuiltInSort(vstring str)384 SMTLIB::BuiltInSorts SMTLIB::getBuiltInSort(vstring str)
385 {
386   CALL("SMTLIB::getBuiltInSort");
387 
388   static NameArray builtInSortNames(s_builtInSortNameStrings, sizeof(s_builtInSortNameStrings)/sizeof(char*));
389   ASS_EQ(builtInSortNames.length, BS_INVALID);
390 
391   int res = builtInSortNames.tryToFind(str.c_str());
392   if(res==-1) {
393     return BS_INVALID;
394   }
395   return static_cast<BuiltInSorts>(res);
396 }
397 
398 const char * SMTLIB::s_formulaSymbolNameStrings[] = {
399     "<",
400     "<=",
401     "=",
402     ">",
403     ">=",
404     "and",
405     "distinct",
406     "exists",
407     "flet",
408     "forall",
409     "if_then_else",
410     "iff",
411     "implies",
412     "let",
413     "not",
414     "or",
415     "xor"
416 };
417 
getFormulaSymbol(vstring str)418 SMTLIB::FormulaSymbol SMTLIB::getFormulaSymbol(vstring str)
419 {
420   CALL("SMTLIB::getFormulaSymbol");
421 
422   static NameArray formulaSymbolNames(s_formulaSymbolNameStrings, sizeof(s_formulaSymbolNameStrings)/sizeof(char*));
423   ASS_EQ(formulaSymbolNames.length, FS_USER_PRED_SYMBOL);
424 
425   int res = formulaSymbolNames.tryToFind(str.c_str());
426   if(res==-1) {
427     return FS_USER_PRED_SYMBOL;
428   }
429   return static_cast<FormulaSymbol>(res);
430 }
431 
432 const char * SMTLIB::s_termSymbolNameStrings[] = {
433     "*",
434     "+",
435     "-",
436     "div",
437     "ite",
438     "select",
439     "store",
440     "~",
441 };
442 
443 
getTermSymbol(vstring str,unsigned arity)444 SMTLIB::TermSymbol SMTLIB::getTermSymbol(vstring str,unsigned arity)
445 {
446   CALL("SMTLIB::getTermSymbol");
447 
448   static NameArray termSymbolNames(s_termSymbolNameStrings, sizeof(s_termSymbolNameStrings)/sizeof(char*));
449   ASS_EQ(termSymbolNames.length, TS_USER_FUNCTION);
450 
451 
452   int resInt = termSymbolNames.tryToFind(str.c_str());
453   TermSymbol res;
454 
455   if(resInt==-1) {
456     res =TS_USER_FUNCTION;
457   }
458   else {
459     res = static_cast<TermSymbol>(resInt);
460   }
461   if(res==TS_MINUS && arity==1) {
462     res = TS_UMINUS;
463   }
464 
465 return res;
466 }
467 
468 /**
469  * If 0 is returned, there is no mandatory argument count
470  */
getMandatoryConnectiveArgCnt(FormulaSymbol fsym)471 unsigned SMTLIB::getMandatoryConnectiveArgCnt(FormulaSymbol fsym)
472 {
473   CALL("SMTLIB::getConnectiveArgCnt");
474 
475   switch(fsym) {
476   case FS_AND:
477   case FS_OR:
478     return 0;
479   case FS_NOT:
480     return 1;
481   case FS_IFF:
482   case FS_IMPLIES:
483   case FS_XOR:
484     return 2;
485   case FS_IF_THEN_ELSE:
486     return 3;
487   default:
488     ASSERTION_VIOLATION;
489   }
490 }
491 
492 //unsigned SMTLIB::getPredSymbolArity(FormulaSymbol fsym, vstring str)
493 //{
494 //  switch(fsym) {
495 //  case FS_EQ:
496 //    return 2;
497 //  case FS_USER_PRED_SYMBOL:
498 //    return env.signature->pre
499 //  }
500 //}
501 
getSort(TermList t)502 unsigned SMTLIB::getSort(TermList t)
503 {
504   CALL("SMTLIB::readTermFromAtom");
505 
506   unsigned res;
507   TermList mvar;
508   if(!SortHelper::getResultSortOrMasterVariable(t, res, mvar)) {
509     ASS(mvar.isVar());
510     unsigned varIdx = mvar.var();
511     ASS_L(varIdx, _varSorts.size());
512     res = _varSorts[varIdx];
513   }
514   return res;
515 }
516 
ensureArgumentSorts(bool pred,unsigned symNum,TermList * args)517 void SMTLIB::ensureArgumentSorts(bool pred, unsigned symNum, TermList* args)
518 {
519   CALL("SMTLIB::ensureArgumentSorts");
520 
521   OperatorType* type;
522   if(pred) {
523     type = env.signature->getPredicate(symNum)->predType();
524   }
525   else {
526     type = env.signature->getFunction(symNum)->fnType();
527   }
528   unsigned arity = type->arity();
529   for(unsigned i=0; i<arity; i++) {
530     if(type->arg(i)!=getSort(args[i])) {
531       USER_ERROR("argument sort mismatch: "+args[i].toString());
532     }
533   }
534 }
535 
readTermFromAtom(vstring str)536 TermList SMTLIB::readTermFromAtom(vstring str)
537 {
538   CALL("SMTLIB::readTermFromAtom");
539 
540   if(str[0]=='?') {
541     TermList res;
542     if(!_termVars.find(str, res)) {
543       USER_ERROR("undefined term variable: "+str);
544     }
545 
546     return res;
547   }
548 
549   if(str[0]>='0' && str[0]<='9') {
550     if(!_treatIntsAsReals && StringUtils::isPositiveInteger(str)) {
551       return TermList(Theory::instance()->representIntegerConstant(str));
552     }
553     else if(StringUtils::isPositiveDecimal(str)) {
554       return TermList(Theory::instance()->representRealConstant(str));
555     }
556     else {
557       USER_ERROR("invalid base term: "+str);
558     }
559   }
560 
561   if(!env.signature->functionExists(str, 0)) {
562     USER_ERROR("undeclared constant: "+str);
563   }
564   return TermList(Term::createConstant(str));
565 }
566 
tryReadTermIte(LExpr * e,TermList & res)567 bool SMTLIB::tryReadTermIte(LExpr* e, TermList& res)
568 {
569   CALL("SMTLIB::tryReadTermIte");
570 
571   LispListReader rdr(e);
572   rdr.acceptAtom("ite");
573 
574   bool gotAll = true;
575   Formula* cond;
576   TermList thenBranch;
577   TermList elseBranch;
578   gotAll |= tryGetArgumentFormula(e, rdr.readNext(), cond);
579   gotAll |= tryGetArgumentTerm(e, rdr.readNext(), thenBranch);
580   gotAll |= tryGetArgumentTerm(e, rdr.readNext(), elseBranch);
581   if(!gotAll) {
582     return false;
583   }
584   res = TermList(Term::createITE(cond, thenBranch, elseBranch, 0)); // TODO: construct a proper sort
585   return true;
586 }
587 
588 /**
589  * Assume all the remaining elements in @c rdr to be term expressions
590  * and attempt to obtain their TermList representation to be put into
591  * the @c args stack. If successful, return true, otherwise return false,
592  * put an empty TermList in place of arguments that could not have been
593  * obtained and schedule those arguments for processing on the _todo list
594  * (by a call to the tryGetArgumentTerm() function).
595  */
readTermArgs(LExpr * parent,LispListReader & rdr,TermStack & args)596 bool SMTLIB::readTermArgs(LExpr* parent, LispListReader& rdr, TermStack& args)
597 {
598   CALL("SMTLIB::readTermArgs");
599   ASS(args.isEmpty());
600 
601   bool someArgsUnevaluated = false;
602 
603   while(rdr.hasNext()) {
604     TermList arg;
605     vstring atomArgStr;
606     if(rdr.tryReadAtom(atomArgStr)) {
607       arg = readTermFromAtom(atomArgStr);
608     }
609     else {
610       LExpr* argExpr = rdr.readListExpr();
611       if(!tryGetArgumentTerm(parent, argExpr, arg)) {
612         someArgsUnevaluated = true;
613       }
614     }
615     args.push(arg);
616   }
617   return !someArgsUnevaluated;
618 }
619 
getFormulaSymbolInterpretation(FormulaSymbol fs,unsigned firstArgSort)620 Interpretation SMTLIB::getFormulaSymbolInterpretation(FormulaSymbol fs, unsigned firstArgSort)
621 {
622   CALL("SMTLIB::getFormulaSymbolInterpretation");
623 
624   switch(fs) {
625   case FS_LESS:
626     switch(firstArgSort) {
627     case Sorts::SRT_INTEGER:
628 	return Theory::INT_LESS;
629     case Sorts::SRT_REAL:
630 	return Theory::REAL_LESS;
631     default:
632       break;
633     }
634     break;
635   case FS_LESS_EQ:
636     switch(firstArgSort) {
637     case Sorts::SRT_INTEGER:
638 	return Theory::INT_LESS_EQUAL;
639     case Sorts::SRT_REAL:
640       return Theory::REAL_LESS_EQUAL;
641     default:
642       break;
643     }
644     break;
645   case FS_GREATER:
646     switch(firstArgSort) {
647     case Sorts::SRT_INTEGER:
648       return Theory::INT_GREATER;
649     case Sorts::SRT_REAL:
650       return Theory::REAL_GREATER;
651     default:
652       break;
653     }
654     break;
655   case FS_GREATER_EQ:
656     switch(firstArgSort) {
657     case Sorts::SRT_INTEGER:
658       return Theory::INT_GREATER_EQUAL;
659     case Sorts::SRT_REAL:
660       return Theory::REAL_GREATER_EQUAL;
661     default:
662       break;
663     }
664     break;
665 
666   default:
667     ASSERTION_VIOLATION;
668   }
669     USER_ERROR("invalid sort "+env.sorts->sortName(firstArgSort)+" for interpretation "+vstring(s_formulaSymbolNameStrings[fs]));
670 }
671 
getTermSymbolInterpretation(TermSymbol ts,unsigned firstArgSort)672 Interpretation SMTLIB::getTermSymbolInterpretation(TermSymbol ts, unsigned firstArgSort)
673 {
674   CALL("SMTLIB::getTermSymbolInterpretation");
675 
676   switch(ts) {
677   case TS_MINUS:
678     switch(firstArgSort) {
679     case Sorts::SRT_INTEGER:
680 	return Theory::INT_MINUS;
681     case Sorts::SRT_REAL:
682 	return Theory::REAL_MINUS;
683     default:
684       break;
685     }
686     break;
687   case TS_PLUS:
688     switch(firstArgSort) {
689     case Sorts::SRT_INTEGER:
690 	return Theory::INT_PLUS;
691     case Sorts::SRT_REAL:
692       return Theory::REAL_PLUS;
693     default:
694       break;
695     }
696     break;
697   case TS_MULTIPLY:
698     switch(firstArgSort) {
699     case Sorts::SRT_INTEGER:
700       return Theory::INT_MULTIPLY;
701     case Sorts::SRT_REAL:
702       return Theory::REAL_MULTIPLY;
703     default:
704       break;
705     }
706     break;
707   case TS_UMINUS:
708     switch(firstArgSort) {
709     case Sorts::SRT_INTEGER:
710       return Theory::INT_UNARY_MINUS;
711     case Sorts::SRT_REAL:
712       return Theory::REAL_UNARY_MINUS;
713     default:
714       break;
715     }
716     break;
717   case TS_DIVIDE:
718     switch(firstArgSort) {
719     case Sorts::SRT_INTEGER:
720       return Theory::INT_QUOTIENT_E;
721     case Sorts::SRT_REAL:
722       return Theory::REAL_QUOTIENT;
723     default:
724       break;
725     }
726     break;
727 
728   default:
729     ASSERTION_VIOLATION_REP(ts);
730   }
731     USER_ERROR("invalid sort "+env.sorts->sortName(firstArgSort)+" for interpretation "+vstring(s_termSymbolNameStrings[ts]));
732 }
733 
734 
735 /**parse Select/Store terms
736  * @author Krystof Hoder and Laura Kovacs
737  * since 31/08/2012 Vienna
738 */
getTermSelectOrStoreFn(LExpr * e,TermSymbol tsym,const TermStack & args)739 unsigned SMTLIB::getTermSelectOrStoreFn(LExpr* e, TermSymbol tsym, const TermStack& args)
740 {
741   CALL("SMTLIB::tryReadTermSelectOrStoreFn");
742   ASS(tsym==TS_SELECT || tsym==TS_STORE);
743 
744 
745 //  Interpretation array_ax_interp = Theory::INVALID_INTERPRETATION;
746 
747   unsigned arity = args.size();
748   if(tsym==TS_SELECT) {
749     if(arity!=2) {
750       USER_ERROR("select should be a binary function: "+e->toString());
751     }
752   }
753   else {
754     ASS_EQ(tsym,TS_STORE);
755       if(arity!=3) {
756       USER_ERROR("store should be a ternary function: "+e->toString());
757     }
758   }
759 
760   vstring arrayName=e->list->tail()->head()->toString();
761   unsigned arrSort = getSort(args[0]);
762 
763   unsigned arrDomainSort;
764   unsigned arrRangeSort;
765   if(_array1Sort && arrSort==_array1Sort) {
766     arrDomainSort = getSort(BS_INT);
767     arrRangeSort = getSort(BS_INT); //change the arrRangeSort from BS_REAL to BS_INT, as for now we only handle arrays of Int
768   }
769   else if(_array2Sort && arrSort==_array2Sort) {
770     arrDomainSort = getSort(BS_INT);
771     arrRangeSort = getSort(BS_ARRAY1);
772   }
773   else {
774     USER_ERROR("invalid array sort: "+env.sorts->sortName(arrSort)+" in "+e->toString());
775   }
776 
777   if(getSort(args[1])!=arrDomainSort) {
778     USER_ERROR("invalid second argument sort: "+env.sorts->sortName(getSort(args[1]))+" in "+e->toString());
779   }
780   if(tsym==TS_STORE && getSort(args[2])!=arrRangeSort) {
781     USER_ERROR("invalid third argument sort: "+env.sorts->sortName(getSort(args[2]))+" in "+e->toString());
782   }
783 
784   unsigned res;
785 
786   if(tsym==TS_STORE) {
787      if (arrSort == _array1Sort) {
788        res=Theory::instance()->getSymbolForStructuredSort(_array1Sort,
789                              Theory::StructuredSortInterpretation::ARRAY_STORE);
790      }
791      else //this is an array2
792      {
793        res=Theory::instance()->getSymbolForStructuredSort(_array2Sort,
794                              Theory::StructuredSortInterpretation::ARRAY_STORE);
795      }
796   }
797   else {
798      if (arrSort == _array1Sort) {
799        res=Theory::instance()->getSymbolForStructuredSort(_array1Sort,
800                              Theory::StructuredSortInterpretation::ARRAY_SELECT);
801      }
802      else //this is an array2
803      {
804        res=Theory::instance()->getSymbolForStructuredSort(_array2Sort,
805                              Theory::StructuredSortInterpretation::ARRAY_SELECT);
806      }
807   }
808     return res;
809 }
810 
811 
812 
tryReadTerm(LExpr * e,TermList & res)813 bool SMTLIB::tryReadTerm(LExpr* e, TermList& res)
814 {
815   CALL("SMTLIB::tryReadTerm");
816 
817   if(e->isAtom()) {
818     res = readTermFromAtom(e->str);
819     return true;
820   }
821 
822   unsigned arity = List<LExpr*>::length(e->list) - 1;
823   LispListReader rdr(e);
824   vstring fnName = rdr.readAtom();
825 
826   TermSymbol ts = getTermSymbol(fnName, arity);
827 
828   if(ts==TS_ITE) {
829     return tryReadTermIte(e, res);
830   }
831 
832   static TermStack args;
833   args.reset();
834 
835   if(!readTermArgs(e, rdr, args)) {
836     return false;
837   }
838 
839   ASS_EQ(arity, args.size());
840   unsigned fnNum;
841 
842   if(ts==TS_USER_FUNCTION) {
843     if(!env.signature->functionExists(fnName, arity)) {
844       USER_ERROR("undeclared function: "+fnName+"/"+Int::toString(arity));
845     }
846     fnNum = env.signature->addFunction(fnName, arity);
847   }
848   else if(ts==TS_SELECT || ts==TS_STORE) {
849     fnNum = getTermSelectOrStoreFn(e, ts, args);
850   }
851   else {
852     if(arity==0) {
853       USER_ERROR("interpreted function with zero arity: "+fnName);
854     }
855     unsigned firstArgSort = getSort(args[0]);
856     Interpretation itp = getTermSymbolInterpretation(ts, firstArgSort);
857     if(Theory::instance()->getArity(itp)!=args.size()) {
858       USER_ERROR("invalid function arity: "+e->toString());
859     }
860     fnNum = Theory::instance()->getFnNum(itp);
861   }
862 
863   ASS_EQ(env.signature->functionArity(fnNum), args.size());
864   ensureArgumentSorts(false, fnNum, args.begin());
865   res = TermList(Term::create(fnNum, arity, args.begin()));
866 
867   return true;
868 }
869 
tryReadNonPropAtom(FormulaSymbol fsym,LExpr * e,Literal * & res)870 bool SMTLIB::tryReadNonPropAtom(FormulaSymbol fsym, LExpr* e, Literal*& res)
871 {
872   CALL("SMTLIB::tryReadNonPropAtom");
873 
874   LispListReader rdr(e);
875   vstring predName = rdr.readAtom();
876 
877   static TermStack args;
878   args.reset();
879 
880   if(!readTermArgs(e, rdr, args)) {
881     return false;
882   }
883 
884   if(fsym==FS_EQ) {
885     if(args.size()!=2) {
886       USER_ERROR("equality requires two arguments: "+e->toString());
887     }
888     unsigned srt = getSort(args[0]);
889     if(srt!=getSort(args[1])) {
890       USER_ERROR("equality argument sort mismatch: "+e->toString());
891     }
892     res = Literal::createEquality(true, args[0], args[1], srt);
893     return true;
894   }
895 
896 
897   unsigned arity = args.size();
898   unsigned predNum;
899 
900   if(fsym==FS_USER_PRED_SYMBOL) {
901     if(!env.signature->predicateExists(predName, arity)) {
902       USER_ERROR("undeclared predicate: "+predName+"/"+Int::toString(arity));
903     }
904     predNum = env.signature->addPredicate(predName, arity);
905   }
906   else {
907     if(arity==0) {
908       USER_ERROR("interpreted predicate with zero arity: "+predName);
909     }
910     unsigned firstArgSort = getSort(args[0]);
911     Interpretation itp = getFormulaSymbolInterpretation(fsym, firstArgSort);
912     if(Theory::instance()->getArity(itp)!=args.size()) {
913       USER_ERROR("invalid predicate arity: "+predName);
914     }
915     predNum = Theory::instance()->getPredNum(itp);
916   }
917 
918   ASS_EQ(env.signature->predicateArity(predNum), args.size());
919   ensureArgumentSorts(true, predNum, args.begin());
920   res = Literal::create(predNum, arity, true, false, args.begin());
921   return true;
922 }
923 
readFormulaFromAtom(vstring str)924 Formula* SMTLIB::readFormulaFromAtom(vstring str)
925 {
926   CALL("SMTLIB::readFormulaFromAtom");
927 
928   if(str=="true") {
929     return Formula::trueFormula();
930   }
931   if(str=="false") {
932     return Formula::falseFormula();
933   }
934   if(str[0]=='$') {
935     Formula* res;
936     if(!_formVars.find(str, res)) {
937       USER_ERROR("undefined formula variable "+str);
938     }
939     return res;
940   }
941   if(str[0]=='?') {
942     USER_ERROR("term variable where formula was expected: "+str);
943   }
944   if(!env.signature->predicateExists(str, 0)) {
945     USER_ERROR("undeclared propositional predicate: "+str);
946   }
947   unsigned predNum = env.signature->addPredicate(str, 0);
948   Literal* resLit = Literal::create(predNum, 0, true, false, 0);
949   return new AtomicFormula(resLit);
950 }
951 
tryReadConnective(FormulaSymbol fsym,LExpr * e,Formula * & res)952 bool SMTLIB::tryReadConnective(FormulaSymbol fsym, LExpr* e, Formula*& res)
953 {
954   CALL("SMTLIB::tryReadConnective");
955 
956   LispListReader rdr(e);
957   rdr.acceptAtom();
958 
959   bool someArgsUnevaluated = false;
960 
961   static FormulaStack argForms;
962   argForms.reset();
963   while(rdr.hasNext()) {
964     LExpr* arg = rdr.readNext();
965     Formula* form = 0;
966     if(!tryGetArgumentFormula(e, arg, form)) {
967       someArgsUnevaluated = true;
968     }
969     argForms.push(form);
970   }
971   if(someArgsUnevaluated) {
972     return false;
973   }
974   if(argForms.isEmpty()) {
975     USER_ERROR("conective with no arguments: "+e->toString());
976   }
977   unsigned mandArgCnt = getMandatoryConnectiveArgCnt(fsym);
978   if(mandArgCnt && argForms.size()!=mandArgCnt) {
979     USER_ERROR("invalid argument number: "+e->toString());
980   }
981 
982   switch(fsym) {
983   case FS_NOT:
984     res = new NegatedFormula(argForms[0]);
985     break;
986   case FS_AND:
987   case FS_OR:
988   {
989     if(argForms.size()==1) {
990       res = argForms[0];
991     }
992     else {
993       FormulaList* argLst = 0;
994       FormulaList::pushFromIterator(FormulaStack::Iterator(argForms), argLst);
995       res = new JunctionFormula( (fsym==FS_AND) ? AND : OR, argLst);
996     }
997     break;
998   }
999   case FS_IFF:
1000   case FS_IMPLIES:
1001   case FS_XOR:
1002   {
1003     Connective con = (fsym==FS_IFF) ? IFF : ((fsym==FS_IMPLIES) ? IMP : XOR);
1004     res = new BinaryFormula(con, argForms[0], argForms[1]);
1005     break;
1006   }
1007   case FS_IF_THEN_ELSE:
1008     res = Formula::createITE(argForms[0], argForms[1], argForms[2]);
1009     break;
1010   default:
1011     ASSERTION_VIOLATION;
1012   }
1013   return true;
1014 }
1015 
tryReadQuantifier(bool univ,LExpr * e,Formula * & res)1016 bool SMTLIB::tryReadQuantifier(bool univ, LExpr* e, Formula*& res)
1017 {
1018   CALL("SMTLIB::tryReadQuantifier");
1019 
1020   LispListReader rdr(e);
1021   rdr.acceptAtom();
1022 
1023   static Stack<LExpr*> qExprs;
1024   qExprs.reset();
1025   qExprs.loadFromIterator(rdr);
1026 
1027   LExpr* subFormExpr = qExprs.pop();
1028 
1029   static Stack<vstring> varNames;
1030   varNames.reset();
1031 
1032   Stack<LExpr*>::BottomFirstIterator qvarExprIt(qExprs);
1033   while(qvarExprIt.hasNext()) {
1034     LispListReader qvarRdr(qvarExprIt.next());
1035     vstring varName = qvarRdr.readAtom();
1036     vstring sortName = qvarRdr.readAtom();
1037     qvarRdr.acceptEOL();
1038 
1039     if(varName[0]!='?') {
1040       USER_ERROR("term variable expected in quantifier: "+varName);
1041     }
1042     if(_entering) {
1043       //we're entering the node
1044       if(_termVars.find(varName)) {
1045 	USER_ERROR("quantifying bound variable: "+varName);
1046       }
1047       unsigned varIdx = _nextQuantVar++;
1048       unsigned sort = getSort(sortName);
1049       _termVars.insert(varName, TermList(varIdx, false));
1050       ASS_EQ(_varSorts.size(), varIdx);
1051       _varSorts.push(sort);
1052     }
1053     ASS(_termVars.find(varName));
1054     ASS(_termVars.get(varName).isVar());
1055     varNames.push(varName);
1056   }
1057 
1058   Formula* subForm;
1059 
1060   ASS_EQ(_forms.find(subFormExpr), !_entering);
1061   if(!tryGetArgumentFormula(e, subFormExpr, subForm)) {
1062     ASS(_entering);
1063     return false;
1064   }
1065 
1066   Formula::VarList* qvars = 0;
1067   Stack<vstring>::Iterator vnameIt(varNames);
1068   while(vnameIt.hasNext()) {
1069     vstring varName = vnameIt.next();
1070     unsigned varIdx = _termVars.get(varName).var();
1071     Formula::VarList::push(varIdx, qvars);
1072     ALWAYS(_termVars.remove(varName));
1073   }
1074 
1075   // TODO add sort list
1076   res = new QuantifiedFormula(univ ? FORALL : EXISTS, qvars, 0, subForm);
1077   return true;
1078 }
1079 
tryReadFlet(LExpr * e,Formula * & res)1080 bool SMTLIB::tryReadFlet(LExpr* e, Formula*& res)
1081 {
1082   CALL("SMTLIB::tryReadFlet");
1083 
1084   LispListReader rdr(e);
1085 
1086   rdr.acceptAtom("flet");
1087   LispListReader defRdr(rdr.readList());
1088   vstring varName = defRdr.readAtom();
1089 
1090   if(varName[0]!='$') {
1091     USER_ERROR("invalid formula variable name: "+varName);
1092   }
1093 
1094   if(_entering && _formVars.find(varName)) {
1095     USER_ERROR("flet binds a formula variable that is already bound: "+varName);
1096   }
1097 
1098   LExpr* varRhsExpr = defRdr.readNext();
1099   defRdr.acceptEOL();
1100 
1101   Formula* varRhs;
1102   if(!tryGetArgumentFormula(e, varRhsExpr, varRhs)) {
1103     ASS(_entering);
1104     //it is important that we return at this point and don't request the
1105     //formula for the flet body. The variable value has to be assigned
1106     //before we start processing that expression.
1107     return false;
1108   }
1109   ASS(!_entering);
1110   if(!_formVars.find(varName)) {
1111     if(_fletAsDefinition) {
1112       varRhs = nameFormula(varRhs, varName);
1113     }
1114     _formVars.insert(varName, varRhs);
1115   }
1116 
1117   LExpr* bodyExpr = rdr.readNext();
1118   if(!tryGetArgumentFormula(e, bodyExpr, res)) {
1119     return false;
1120   }
1121 
1122   ALWAYS(_formVars.remove(varName));
1123   return true;
1124 }
1125 
tryReadLet(LExpr * e,Formula * & res)1126 bool SMTLIB::tryReadLet(LExpr* e, Formula*& res)
1127 {
1128   CALL("SMTLIB::tryReadLet");
1129 
1130   LispListReader rdr(e);
1131 
1132   rdr.acceptAtom("let");
1133   LispListReader defRdr(rdr.readList());
1134   vstring varName = defRdr.readAtom();
1135   if(varName[0]!='?') {
1136     USER_ERROR("invalid term variable name: "+varName);
1137   }
1138 
1139   LExpr* varRhsExpr = defRdr.readNext();
1140   defRdr.acceptEOL();
1141 
1142   if(_entering && _termVars.find(varName)) {
1143     USER_ERROR("let binds a variable that is already bound: "+varName);
1144   }
1145 
1146   TermList varRhs;
1147   if(!tryGetArgumentTerm(e, varRhsExpr, varRhs)) {
1148     ASS(_entering);
1149     //it is important that we return at this point and don't request the
1150     //formula for the let body. The variable value has to be assigned
1151     //before we start processing that expression.
1152     return false;
1153   }
1154   ASS(!_entering);
1155 
1156   if(!_termVars.insert(varName, varRhs)) {
1157     //we're in the third call
1158   }
1159 
1160   LExpr* bodyExpr = rdr.readNext();
1161   if(!tryGetArgumentFormula(e, bodyExpr, res)) {
1162     return false;
1163   }
1164 
1165   ALWAYS(_termVars.remove(varName));
1166   return true;
1167 }
1168 
tryReadDistinct(LExpr * e,Formula * & res)1169 bool SMTLIB::tryReadDistinct(LExpr* e, Formula*& res)
1170 {
1171   CALL("SMTLIB::tryReadDistinct");
1172 
1173   LispListReader rdr(e);
1174   rdr.acceptAtom("distinct");
1175 
1176   TermStack args;
1177 
1178   if(!readTermArgs(e, rdr, args)) {
1179     return false;
1180   }
1181 
1182   unsigned arity = args.size();
1183   if(arity<2) {
1184     USER_ERROR("distinct predicate should have at least two arguments: "+e->toString());
1185   }
1186 
1187   unsigned sort = getSort(args[0]);
1188   for(unsigned i=1; i<arity; i++) {
1189     if(sort!=getSort(args[i])) {
1190       USER_ERROR("sort mismatch in distinct predicate: "+e->toString());
1191     }
1192   }
1193 
1194   bool added;
1195   OperatorType* type = OperatorType::getPredicateTypeUniformRange(arity, sort);
1196 
1197   //this is a bit of a quick hack, we need to come up with
1198   //a proper way to have a polymorphic $distinct predicate
1199   unsigned predNum = env.signature->addPredicate("$distinct", arity, added);
1200   if(added) {
1201     env.signature->getPredicate(predNum)->setType(type);
1202   }
1203   else {
1204     OperatorType* prevType = env.signature->getPredicate(predNum)->predType();
1205     if(*type==*prevType) {
1206       delete type;
1207     }
1208     else {
1209       vstring name = "$distinct_"+StringUtils::sanitizeSuffix(env.sorts->sortName(sort));
1210       predNum = env.signature->addPredicate(name, arity, added);
1211       if(added) {
1212 	env.signature->getPredicate(predNum)->setType(type);
1213       }
1214       else {
1215 	ASS(*type==*env.signature->getPredicate(predNum)->predType());
1216 	delete type;
1217       }
1218     }
1219   }
1220 
1221   res = new AtomicFormula(Literal::create(predNum, arity, true, false, args.begin()));
1222   return true;
1223 }
1224 
tryReadFormula(LExpr * e,Formula * & res)1225 bool SMTLIB::tryReadFormula(LExpr* e, Formula*& res)
1226 {
1227   CALL("SMTLIB::tryReadFormula");
1228 
1229   if(e->isAtom()) {
1230     res = readFormulaFromAtom(e->str);
1231     return true;
1232   }
1233 
1234   LispListReader rdr(e);
1235   vstring sym = rdr.readAtom();
1236   FormulaSymbol fsym = getFormulaSymbol(sym);
1237   switch(fsym) {
1238   case FS_NOT:
1239   case FS_AND:
1240   case FS_IFF:
1241   case FS_IMPLIES:
1242   case FS_OR:
1243   case FS_XOR:
1244   case FS_IF_THEN_ELSE:
1245     return tryReadConnective(fsym, e, res);
1246 
1247   case FS_EXISTS:
1248   case FS_FORALL:
1249     return tryReadQuantifier(fsym==FS_FORALL, e, res);
1250 
1251   case FS_EQ:
1252   case FS_LESS:
1253   case FS_LESS_EQ:
1254   case FS_GREATER:
1255   case FS_GREATER_EQ:
1256   case FS_USER_PRED_SYMBOL:
1257   {
1258     Literal* lit;
1259     if(tryReadNonPropAtom(fsym, e, lit)) {
1260       res = new AtomicFormula(lit);
1261       return true;
1262     }
1263     return false;
1264   }
1265 
1266   case FS_DISTINCT:
1267     return tryReadDistinct(e, res);
1268 
1269   case FS_FLET:
1270     return tryReadFlet(e, res);
1271   case FS_LET:
1272     return tryReadLet(e, res);
1273   default:
1274     ASSERTION_VIOLATION;
1275   }
1276 }
1277 
tryGetArgumentTerm(LExpr * parent,LExpr * argument,TermList & res)1278 bool SMTLIB::tryGetArgumentTerm(LExpr* parent, LExpr* argument, TermList& res)
1279 {
1280   CALL("SMTLIB::tryGetArgumentTerm");
1281   ASS_EQ(parent,_current.first);
1282 
1283   if(_terms.find(argument, res)) {
1284     ASS(!_entering);
1285     return true;
1286   }
1287   requestSubexpressionProcessing(argument, false);
1288   return false;
1289 }
1290 
tryGetArgumentFormula(LExpr * parent,LExpr * argument,Formula * & res)1291 bool SMTLIB::tryGetArgumentFormula(LExpr* parent, LExpr* argument, Formula*& res)
1292 {
1293   CALL("SMTLIB::tryGetArgumentFormula");
1294   ASS_EQ(parent,_current.first);
1295 
1296   if(_forms.find(argument, res)) {
1297     ASS(!_entering);
1298     return true;
1299   }
1300   requestSubexpressionProcessing(argument, true);
1301   return false;
1302 }
1303 
requestSubexpressionProcessing(LExpr * subExpr,bool formula)1304 void SMTLIB::requestSubexpressionProcessing(LExpr* subExpr, bool formula)
1305 {
1306   CALL("SMTLIB::requestSubexpressionProcessing");
1307 
1308   _todo.push(ToDoEntry(subExpr, formula));
1309   _todo.push(ToDoEntry(0, true));
1310 }
1311 
buildFormula()1312 void SMTLIB::buildFormula()
1313 {
1314   CALL("SMTLIB::buildFormula");
1315 
1316 
1317   {
1318     Formula* f = readFormula(_lispFormula);
1319     FormulaUnit* fu = new FormulaUnit(f, new Inference0(Inference::INPUT), Unit::CONJECTURE);
1320     UnitList::push(fu, _formulas);
1321   }
1322 
1323 
1324   LExprList::Iterator asIt(_lispAssumptions);
1325   while(asIt.hasNext()) {
1326 
1327     LExpr* lispF = asIt.next();
1328     Formula* f = readFormula(lispF);
1329     FormulaUnit* fu = new FormulaUnit(f, new Inference0(Inference::INPUT), Unit::AXIOM);
1330     UnitList::push(fu, _formulas);
1331   }
1332 
1333 
1334   _formulas = UnitList::concat(_formulas, UnitList::copy(_definitions));
1335 }
1336 
readFormula(LExpr * e)1337 Formula* SMTLIB::readFormula(LExpr* e)
1338 {
1339   CALL("SMTLIB::readFormula");
1340 
1341 
1342   ASS(_formVars.isEmpty());
1343   ASS(_termVars.isEmpty());
1344 
1345   _forms.reset();
1346   _terms.reset();
1347 
1348   _varSorts.reset();
1349   _nextQuantVar = 0;
1350 
1351   _todo.push(ToDoEntry(e, true));
1352   _todo.push(ToDoEntry(0, true));
1353 
1354   while(_todo.isNonEmpty()) {
1355     _entering = false;
1356     if(_todo.top().first==0) {
1357       _entering = true;
1358       _todo.pop();
1359     }
1360     _current = _todo.top();
1361     ASS(_current.first);
1362     if(_current.second) {
1363       //we're processing a formula
1364       Formula* form;
1365       if(tryReadFormula(_current.first, form)) {
1366 	ASS(_todo.top()==_current); //if reading succeeded, there aren't any new requests
1367 	_todo.pop();
1368 	ALWAYS(_forms.insert(_current.first, form));
1369       }
1370       else {
1371 	ASS(_todo.top()!=_current); //if reading failed, there must be some new requests
1372       }
1373     }
1374     else {
1375       //we're processing a term
1376       TermList trm;
1377       if(tryReadTerm(_current.first, trm)) {
1378 	ASS(_todo.top()==_current); //if reading succeeded, there aren't any new requests
1379 	_todo.pop();
1380 	ALWAYS(_terms.insert(_current.first, trm));
1381       }
1382       else {
1383 	ASS(_todo.top()!=_current); //if reading failed, there must be some new requests
1384       }
1385     }
1386   }
1387 
1388   Formula* topForm;
1389   ALWAYS(_forms.find(e, topForm));
1390 
1391   ASS(_formVars.isEmpty());
1392   ASS(_termVars.isEmpty());
1393   return topForm;
1394 }
1395 
1396 
nameFormula(Formula * f,vstring fletVarName)1397 Formula* SMTLIB::nameFormula(Formula* f, vstring fletVarName)
1398 {
1399   CALL("SMTLIB::nameFormula");
1400 
1401   Formula::VarList* freeVars = f->freeVariables();
1402   unsigned varCnt = Formula::VarList::length(freeVars);
1403 
1404   static DHMap<unsigned,unsigned> sorts;
1405   sorts.reset();
1406 
1407   SortHelper::collectVariableSorts(f, sorts);
1408 
1409   static Stack<unsigned> argSorts;
1410   static Stack<TermList> args;
1411   argSorts.reset();
1412   args.reset();
1413 
1414   Formula::VarList::Iterator vit(freeVars);
1415   while(vit.hasNext()) {
1416     unsigned var = vit.next();
1417     args.push(TermList(var, false));
1418     argSorts.push(sorts.get(var));
1419   }
1420 
1421   fletVarName = StringUtils::sanitizeSuffix(fletVarName);
1422   unsigned predNum = env.signature->addFreshPredicate(varCnt, "sP", fletVarName.c_str());
1423   OperatorType* type = OperatorType::getPredicateType(varCnt, argSorts.begin());
1424 
1425   Signature::Symbol* predSym = env.signature->getPredicate(predNum);
1426   predSym->setType(type);
1427 
1428   Color symColor = ColorHelper::combine(_introducedSymbolColor, f->getColor());
1429   if(symColor==COLOR_INVALID) {
1430     USER_ERROR("invalid color in formula "+ f->toString());
1431   }
1432   if(symColor!=COLOR_TRANSPARENT) {
1433     predSym->addColor(symColor);
1434   }
1435 
1436   Literal* lhs = Literal::create(predNum, varCnt, true, false, args.begin());
1437   Formula* lhsF = new AtomicFormula(lhs);
1438   Formula* df = new BinaryFormula(IFF, lhsF, f);
1439   if(freeVars) {
1440     // TODO add sorts list
1441     df = new QuantifiedFormula(FORALL, freeVars,0, df);
1442   }
1443   FormulaUnit* def = new FormulaUnit(df, new Inference0(Inference::INPUT), Unit::AXIOM);
1444   UnitList::push(def, _definitions);
1445   return lhsF;
1446 }
1447 
1448 }
1449