45 string Translator::fileToSMTLIBIdentifier(
const string& filename)
49 if (pos == string::npos) {
53 tmpName = filename.substr(pos+1);
57 if ((c < 'A' || c >
'Z') && (c < 'a' || c >
'z')) {
60 for (
unsigned i = 0; i < tmpName.length(); ++i) {
62 if ((c < 'A' || c >
'Z') && (c < 'a' || c >
'z') &&
63 (c < '0' || c >
'9') && (c !=
'.' && c !=
'_')) {
75 if(i != cache.
end()) {
79 if (d_theoryCore->getFlags()[
"liftITE"].getBool() &&
81 Theorem thm = d_theoryCore->getCommonRules()->liftOneITE(e);
82 return preprocessRec(thm.
getRHS(), cache);
91 d_theoryCore->theoryOf(e2)->setUsed();
97 vector<Expr> children;
100 for(
int k = 0; k < e.
arity(); ++k) {
102 Expr child = preprocessRec(e[k], cache);
103 if (child != e[k]) diff =
true;
104 children.push_back(child);
116 FatalAssert(
false,
"Cannot convert non-integer constant to BV");
120 FatalAssert(
false,
"Cannot convert to BV: integer too big");
122 else if (r < -limit) {
123 FatalAssert(
false,
"Cannot convert to BV: integer too small");
125 e2 = d_theoryBitvector->signed_newBVConstExpr(r, d_convertToBV);
130 if (!d_unknown && d_theoryCore->getFlags()[
"convert2array"].getBool()) {
131 if (e2[1].getKind() !=
UCONST)
break;
132 map<string, Type>::iterator i = d_arrayConvertMap->find(e2[1].getName());
133 if (i == d_arrayConvertMap->end()) {
134 (*d_arrayConvertMap)[e2[1].
getName()] = *d_indexType;
137 if ((*i).second != (*d_indexType)) {
145 if (!d_unknown && d_theoryCore->getFlags()[
"convert2array"].getBool()) {
146 map<string, Type>::iterator i;
147 if (e2[1].getKind() ==
UCONST) {
148 i = d_arrayConvertMap->find(e2[1].getName());
149 if (i == d_arrayConvertMap->end()) {
150 (*d_arrayConvertMap)[e2[1].
getName()] = *d_indexType;
153 if ((*i).second != (*d_indexType)) {
159 if (e2[2].getKind() !=
UCONST)
break;
160 i = d_arrayConvertMap->find(e2[2].getName());
161 if (i == d_arrayConvertMap->end()) {
162 (*d_arrayConvertMap)[e2[2].
getName()] = *d_elementType;
165 if ((*i).second != (*d_elementType)) {
176 Expr body(lambda.getBody());
177 const vector<Expr>& vars = lambda.
getVars();
179 "wrong number of arguments applied to lambda\n");
180 body = body.substExpr(vars, e2.
getKids());
181 e2 = preprocessRec(body, cache);
186 if (d_theoryArith->getBaseType(e2[0]) != d_theoryArith->realType())
188 if (d_theoryCore->getFlags()[
"convert2array"].getBool() &&
189 ((e2[0].
getKind() ==
UCONST && d_arrayConvertMap->find(e2[0].getName()) == d_arrayConvertMap->end()) ||
190 (e2[1].getKind() ==
UCONST && d_arrayConvertMap->find(e2[1].getName()) == d_arrayConvertMap->end()))) {
191 d_equalities.push_back(e2);
200 if (d_theoryArith->isSyntacticRational(e2, r)) {
201 e2 = preprocessRec(d_em->newRatExpr(r), cache);
208 FatalAssert(
false,
"Conversion of DIVIDE to BV not implemented yet");
211 if (d_theoryArith->isSyntacticRational(e2, r)) {
212 e2 = preprocessRec(d_em->newRatExpr(r), cache);
215 else if (d_convertArith && e2[1].
isRational()) {
218 e2 = d_em->newRatExpr(1/r) * e2[0];
219 e2 = preprocessRec(e2, cache);
230 if (d_convertArith) {
232 e2 = d_em->newRatExpr(e2[0].getRational() - e2[1].getRational());
243 if (d_convertArith) {
246 bool changed =
false;
250 for(; i!=iend; ++i) {
251 if ((*i).getKind() ==
PLUS) {
254 for (; i2 != i2end; ++i2) {
255 if ((*i2).isRational()) {
256 r += (*i2).getRational();
259 else terms.push_back(*i2);
263 if ((*i).isRational()) {
264 r += (*i).getRational();
266 if (numConst > 1) changed =
true;
268 else terms.push_back(*i);
271 if (terms.size() == 0) {
272 e2 = preprocessRec(d_em->newRatExpr(r), cache);
275 else if (terms.size() == 1) {
281 e2 = preprocessRec(
Expr(
MINUS, terms[0], d_em->newRatExpr(-r)), cache);
286 if (r != 0) terms.push_back(d_em->newRatExpr(r));
287 e2 = preprocessRec(
Expr(
PLUS, terms), cache);
298 if (d_convertArith) {
301 bool changed =
false;
305 for(; i!=iend; ++i) {
306 if ((*i).getKind() ==
MULT) {
309 for (; i2 != i2end; ++i2) {
310 if ((*i2).isRational()) {
311 r *= (*i2).getRational();
314 else terms.push_back(*i2);
318 if ((*i).isRational()) {
319 r *= (*i).getRational();
321 if (numConst > 1) changed =
true;
323 else terms.push_back(*i);
327 e2 = preprocessRec(d_em->newRatExpr(0), cache);
330 else if (terms.size() == 0) {
331 e2 = preprocessRec(d_em->newRatExpr(r), cache);
334 else if (terms.size() == 1) {
341 if (r != 1) terms.push_back(d_em->newRatExpr(r));
342 e2 = preprocessRec(
Expr(
MULT, terms), cache);
350 FatalAssert(
false,
"Conversion of POW to BV not implemented");
356 e2 = preprocessRec(e2[1] * e2[1], cache);
391 if (d_iteLiftArith) {
394 vector<Expr> children2;
396 for (
int k = 0; k < e2.
arity(); ++k) {
397 if (e2[k].getKind() ==
ITE && !diff) {
400 children.push_back(e2[k][1]);
401 children2.push_back(e2[k][2]);
404 children.push_back(e2[k]);
405 children2.push_back(e2[k]);
411 e2 = cond.
iteExpr(thenpart, elsepart);
412 e2 = preprocessRec(e2, cache);
417 if (d_convertToDiff !=
"" && d_theoryArith->isAtomicArithFormula(e2)) {
418 Expr e3 = d_theoryArith->rewriteToDiff(e2);
420 DebugAssert(e3 == d_theoryArith->rewriteToDiff(e3),
"Expected idempotent rewrite");
421 e2 = preprocessRec(e3, cache);
430 e2 = d_theoryCore->newVar(e2.getName()+
"_bv", d_theoryBitvector->newBitvectorType(d_convertToBV));
441 d_intConstUsed =
true;
453 if (e2.
arity() == 2) {
454 int nonconst = 0, isconst = 0;
456 for(; i!=iend; ++i) {
457 if ((*i).isRational()) {
458 if ((*i).getRational() <= 0) {
466 if (nonconst > 1 || isconst > 1)
469 else d_UFIDL_ok =
false;
487 bool nonconst =
false;
488 for (
int i=0; i!=e2.
arity(); ++i) {
504 if (d_theoryArith->getBaseType(e2[0]) != d_theoryArith->realType() ||
505 (e2[0].
getType() == d_theoryArith->intType() && d_theoryCore->getFlags()[
"convert2array"].getBool()))
511 if (d_langUsed >=
LINEAR)
break;
512 if (!d_theoryArith->isAtomicArithFormula(e2)) {
516 if (e2[0].getKind() ==
MINUS &&
517 d_theoryArith->isLeaf(e2[0][0]) &&
518 d_theoryArith->isLeaf(e2[0][1]) &&
523 if (d_theoryArith->isLeaf(e2[0]) &&
524 d_theoryArith->isLeaf(e2[1])) {
539 if (e2.
arity() == 0)
break;
541 d_theoryCore->theoryOf(e2)->setUsed();
553 result = preprocessRec(e, cache);
555 cerr <<
"Error while processing the formula:\n"
565 TRACE(
"smtlib2-linear",
"preprocess2Rec: ", e,
"");
567 if(i != cache.
end()) {
568 if ((desiredType.
isNull() &&
569 (*i).second.getType() != d_theoryArith->realType()) ||
570 (*i).second.getType() == desiredType) {
585 bool forceReal =
false;
586 if (desiredType == d_theoryArith->intType() &&
587 e.
getType() != d_theoryArith->intType()) {
602 if (e[0].getType() != e[1].
getType()) {
603 if (e[0].getType() != d_theoryArith->intType() &&
604 e[1].
getType() != d_theoryArith->intType()) {
606 throw SmtlibException(
"Expected each side to be REAL or INT, but we got lhs: "+
607 e[0].getType().getExpr().toString()+
" and rhs: "+
608 e[1].getType().getExpr().toString()+
609 "\n\nwhile processing the term:\n"+
619 if (desiredType == d_theoryArith->realType())
631 vector<Expr> children;
643 kids.push_back(e.
getType()[0]);
644 kids.push_back(e.
getType()[1]);
645 funType = Type::funType(kids, e.
getType());
648 for(
int k = 0; k < e.
arity(); ++k) {
650 if (forceReal && e[k].getType() == d_theoryArith->intType())
651 t = d_theoryArith->realType();
652 else if (!funType.
isNull()) t = funType[k];
654 Expr child = preprocess2Rec(e[k], cache, t);
655 if (child != e[k]) diff =
true;
656 children.push_back(child);
662 if (e2.
getType() == d_theoryArith->realType() ||
663 (e2.
getType() == d_theoryArith->intType() &&
664 desiredType == d_theoryArith->realType()))
672 TRACE(
"smtlib2-linear",
"SMT-LIBv2 linearizing: ", e2save,
"");
677 bool realConst =
false;
678 bool trmFirst =
false;
679 for(
int i = 0; i < e2.
arity(); ++i) {
689 FatalAssert(trm.isNull(),
"translating with LINEAR restriction, but found > 1 non-constant under MULT");
697 if( !( e2.
arity() == 2 && !trm.isNull() &&
698 (trm.isApply() || trm.getKind() ==
READ || trm.isVar()) ) ) {
701 Expr coef = d_em->newRatExpr(constCoef);
711 TRACE(
"smtlib2-linear",
"(1) constant",
"",
"");
713 }
else if(constCoef == 1) {
715 TRACE(
"smtlib2-linear",
"(2) unit coefficient: ", trm,
"");
717 }
else if(trm.getKind() ==
PLUS || trm.getKind() ==
MINUS) {
719 TRACE(
"smtlib2-linear",
"(3) mult over plus/minus: ", trm,
"");
721 for(
int i = 0; i < trm.arity(); ++i) {
723 trmi = preprocess2Rec(trmi, cache, desiredType);
724 kids.push_back(trmi);
726 e2 =
Expr(trm.getKind(), kids);
727 }
else if(trm.getKind() ==
MULT) {
729 TRACE(
"smtlib2-linear",
"(4) mult over mult: ", trm,
"");
731 kids.push_back(coef);
732 for(
int i = 0; i < trm.arity(); ++i) {
733 kids.push_back(trm[i]);
736 e2 = preprocess2Rec(e2, cache, desiredType);
737 }
else if(trm.getKind() ==
ITE) {
739 TRACE(
"smtlib2-linear",
"(5) mult over ite: ", trm,
"");
742 thn = preprocess2Rec(thn, cache, desiredType);
743 els = preprocess2Rec(els, cache, desiredType);
744 e2 =
Expr(
ITE, trm[0], thn, els);
747 TRACE(
"smtlib2-linear",
"(*) coef, trm: ", coef, trm);
754 FatalAssert(trm.isVar(), string(
"translating with LINEAR restriction, but found malformed MULT over term that's not a free constant: ") + e2.
toString());
757 TRACE(
"smtlib2-linear",
"(x) no handling necessary: ", trm,
"");
759 TRACE(
"smtlib2-linear",
"SMT-LIBv2 linearized: ", e2save,
"");
760 TRACE(
"smtlib2-linear",
" into: ", e2,
"");
773 "\n\nwhile processing term:\n"+
787 result = preprocess2Rec(e, cache,
Type());
789 cerr <<
"Error while processing the formula:\n"
799 bool Translator::containsArray(
const Expr& e)
803 for(; i!=iend; ++i)
if (containsArray(*i))
return true;
809 const bool& translate,
810 const bool& real2int,
811 const bool& convertArith,
812 const string& convertToDiff,
814 const string& expResult,
815 const string& category,
819 : d_em(em), d_translate(translate),
820 d_real2int(real2int),
821 d_convertArith(convertArith),
822 d_convertToDiff(convertToDiff),
823 d_iteLiftArith(iteLiftArith),
824 d_expResult(expResult),
825 d_category(category),
826 d_convertArray(convertArray),
827 d_combineAssump(combineAssump),
828 d_dump(false), d_dumpFileOpen(false),
829 d_intIntArray(false), d_intRealArray(false), d_intIntRealArray(false),
830 d_ax(false), d_unknown(false),
831 d_realUsed(false), d_intUsed(false), d_intConstUsed(false),
832 d_langUsed(
NOT_USED), d_UFIDL_ok(true), d_arithUsed(false),
833 d_zeroVar(NULL), d_convertToBV(convertToBV)
849 if (dumpFile ==
"") {
855 throw Exception(
"cannot open a log file: "+dumpFile);
864 if (pos == string::npos) {
868 tmpName = dumpFile.substr(0,pos+1) +
"README";
873 <<
" :source {" <<
endl;
879 if ( c ==
'{' || c ==
'}' ) {
897 if (dumpFile ==
"") {
903 throw Exception(
"cannot open a log file: "+dumpFile);
914 *
d_osdump <<
"author({* CVC2SPASS translator *})." <<
endl;
918 if (dumpFile ==
"") {
927 throw Exception(
"cannot open a log file: "+dumpFile);
945 if (e[1].getKind() ==
ARRAY) {
948 throw Exception(
"convertArray failed because of nested arrays in"+
956 throw Exception(
"convertArray failed becauase of use of arrays in"+
1095 DebugAssert(e[0].arity() == 1,
"expected arity 1");
1096 if (e[0][0].getString() ==
"Index") {
1098 DebugAssert(e[1].arity() == 1,
"expected arity 1");
1099 if (e[1][0].getString() ==
"Element") {
1132 if (e.
arity() == 0)
return e;
1133 bool changed =
false;
1135 for (
int i = 0; i < e.
arity(); ++i) {
1137 if (vec.back() != e[i]) changed =
true;
1163 else if (
status() ==
"invalid" ||
1164 status() ==
"satisfiable" ||
1167 else if (
status() ==
"valid" ||
1168 status() ==
"unsatisfiable" ||
1176 vector<Expr> functions, predicates, sorts;
1178 for(vector<Expr>::reverse_iterator i =
d_dumpExprs.rbegin(), iend =
d_dumpExprs.rend(); i != iend; ++i) {
1186 if(e.
arity() == 2) {
1187 if (e[1].getKind() ==
BOOLEAN ||
1189 predicates.push_back(e);
1191 functions.push_back(e);
1195 throw SmtlibException(
"Translator::finish: SPASS_LANG: CONST not implemented for arity != 2");
1205 if (e.arity() > 1) {
1243 if(!functions.empty()) {
1245 vector<Expr>::reverse_iterator i = functions.rbegin(), iend = functions.rend();
1260 if(!predicates.empty()) {
1262 vector<Expr>::reverse_iterator i = predicates.rbegin(), iend = predicates.rend();
1272 if(!sorts.empty()) {
1274 vector<Expr>::reverse_iterator i = sorts.rbegin(), iend = sorts.rend();
1317 else if (
status() !=
"") {
1347 for (; i != iend; ++i) {
1352 if (e[0] == e2)
break;
1359 if (e[0].negate() == e2)
break;
1368 if (e[1] == e2)
break;
1407 (*d_arrayConvertMap)[
d_equalities[i][0].getName()] = (*it).second;
1421 (*d_arrayConvertMap)[
d_equalities[i][1].getName()] = (*it).second;
1439 for (; i != iend; ++i) {
1460 *i =
Expr(
CONST, e[0], (*it).second.getExpr());
1464 if (e[1] == e2)
break;
1547 if (promote && !QF) {
1553 else if (d_langUsed <=
LINEAR) {
1559 if (promote && !QF) {
1567 if (QF && !A && UF && d_langUsed <=
LINEAR) {
1578 if (promote && !QF) {
1591 else if (d_langUsed <=
LINEAR) {
1594 if (promote && QF && A && !UF) {
1614 if (promote && A && QF && !UF) {
1628 else if (promote && (!QF || (A && UF))) {
1637 qf_uf = QF && UF && (!A);
1657 *
d_osdump <<
"(set-info :smt-lib-version 2.0)" <<
endl;
1661 size_t i = 0, j = c.size();
1662 while (c[i] ==
' ') {
1665 while (j > 0 && c[i+j-1] ==
' ') --j;
1668 *
d_osdump <<
"(set-info :category \"" << c <<
"\")" <<
endl;
1683 else if (
status() !=
"") {
1713 vector<Expr> assumps;
1715 for (; i != iend; ++i) {
1720 assumps.push_back(e[0]);
1728 if (!assumps.empty()) {
1729 assumps.push_back(e[0].negate());
1753 if (e[0][0].getString() ==
"abs") {
1758 }
else if (e[0][0].getString() ==
"mod") {
1779 *
d_osdump <<
"list_of_settings(SPASS)." << endl
1781 <<
"set_flag(Auto,1). % auto configuration" << endl
1782 <<
"set_flag(Splits,-1). % enable Splitting" << endl
1783 <<
"set_flag(RVAA,1). % enable variable assignment abstraction for LA" << endl
1784 <<
"set_flag(RInput,0). % no input reduction" << endl
1785 <<
"set_flag(Sorts,0). % no Sorts" << endl
1786 <<
"set_flag(ISHy,0). % no Hyper Resolution" << endl
1787 <<
"set_flag(IOHy,0). % no Hyper Resolution" << endl
1788 <<
"set_flag(RTer,0). % no Terminator" << endl
1789 <<
"set_flag(RCon,0). % no Condensation" << endl
1790 <<
"set_flag(RFRew,1). % no Contextual Rewriting" << endl
1791 <<
"set_flag(RBRew,1). % no Contextual Rewriting" << endl
1793 <<
"end_of_list." <<
endl;
1819 if (s.length() == 0 || isdigit(s[0]))
1820 return "|" + s +
"|";
1824 if(s.find_first_not_of(
"abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789~!@$%^&*_-+=<>.?/") != string::npos)
1825 return "|" + s +
"|";
1832 if(s.find(
'|') == string::npos) {
1833 return "|" + s +
"|";
1837 for(string::const_iterator i = s.begin(); i != s.end(); ++i) {
1864 DebugAssert(e[0].arity() == 1,
"expected arity 1");
1865 if (e[0][0].getString() ==
"Index") {
1867 DebugAssert(e[1].arity() == 1,
"expected arity 1");
1868 if (e[1][0].getString() ==
"Element") {
1903 os <<
"UnknownArray";
1911 if (e[0].getKind() ==
UCONST) {
1915 else if (e[0].getKind() ==
WRITE) {
1916 throw Exception(
"READ of WRITE not implemented yet for convertArray");
1919 throw Exception(
"Unexpected case for convertArray");
1925 throw Exception(
"WRITE expression encountered while attempting "
1926 "to convert arrays to uninterpreted functions");
1931 throw Exception(
"ARRAY_LITERAL expression encountered while attempting"
1932 " to convert arrays to uninterpreted functions");
1936 throw Exception(
"Unexpected case in printArrayExpr");