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