CVC3  2.4.1
translator.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file translator.cpp
4  * \brief Description: Code for translation between languages
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Sat Jun 25 18:06:52 2005
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 
23 #include <cctype>
24 
25 #include "translator.h"
26 #include "expr.h"
27 #include "theory_core.h"
28 #include "theory_uf.h"
29 #include "theory_arith.h"
30 #include "theory_bitvector.h"
31 #include "theory_array.h"
32 #include "theory_quant.h"
33 #include "theory_records.h"
34 #include "theory_simulate.h"
35 #include "theory_datatype.h"
36 #include "theory_datatype_lazy.h"
37 #include "smtlib_exception.h"
38 #include "command_line_flags.h"
39 
40 
41 using namespace std;
42 using namespace CVC3;
43 
44 
45 string Translator::fileToSMTLIBIdentifier(const string& filename)
46 {
47  string tmpName;
48  string::size_type pos = filename.rfind("/");
49  if (pos == string::npos) {
50  tmpName = filename;
51  }
52  else {
53  tmpName = filename.substr(pos+1);
54  }
55  char c = tmpName[0];
56  string res;
57  if ((c < 'A' || c > 'Z') && (c < 'a' || c > 'z')) {
58  res = "B_";
59  }
60  for (unsigned i = 0; i < tmpName.length(); ++i) {
61  c = tmpName[i];
62  if ((c < 'A' || c > 'Z') && (c < 'a' || c > 'z') &&
63  (c < '0' || c > '9') && (c != '.' && c != '_')) {
64  c = '_';
65  }
66  res += c;
67  }
68  return res;
69 }
70 
71 
72 Expr Translator::preprocessRec(const Expr& e, ExprMap<Expr>& cache)
73 {
74  ExprMap<Expr>::iterator i(cache.find(e));
75  if(i != cache.end()) {
76  return (*i).second;
77  }
78 
79  if (d_theoryCore->getFlags()["liftITE"].getBool() &&
80  e.isPropAtom() && e.containsTermITE()) {
81  Theorem thm = d_theoryCore->getCommonRules()->liftOneITE(e);
82  return preprocessRec(thm.getRHS(), cache);
83  }
84 
85  if (e.isClosure()) {
86  Expr newBody = preprocessRec(e.getBody(), cache);
87  Expr e2(e);
88  if (newBody != e.getBody()) {
89  e2 = d_em->newClosureExpr(e.getKind(), e.getVars(), newBody);
90  }
91  d_theoryCore->theoryOf(e2)->setUsed();
92  cache[e] = e2;
93  return e2;
94  }
95 
96  Expr e2(e);
97  vector<Expr> children;
98  bool diff = false;
99 
100  for(int k = 0; k < e.arity(); ++k) {
101  // Recursively preprocess the kids
102  Expr child = preprocessRec(e[k], cache);
103  if (child != e[k]) diff = true;
104  children.push_back(child);
105  }
106  if (diff) {
107  e2 = Expr(e.getOp(), children);
108  }
109 
110  Rational r;
111  switch (e2.getKind()) {
112  case RATIONAL_EXPR:
113  if (d_convertToBV) {
114  Rational r = e2.getRational();
115  if (!r.isInteger()) {
116  FatalAssert(false, "Cannot convert non-integer constant to BV");
117  }
118  Rational limit = pow(d_convertToBV-1, (Rational)2);
119  if (r >= limit) {
120  FatalAssert(false, "Cannot convert to BV: integer too big");
121  }
122  else if (r < -limit) {
123  FatalAssert(false, "Cannot convert to BV: integer too small");
124  }
125  e2 = d_theoryBitvector->signed_newBVConstExpr(r, d_convertToBV);
126  break;
127  }
128 
129  case READ:
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;
135  }
136  else {
137  if ((*i).second != (*d_indexType)) {
138  d_unknown = true;
139  }
140  }
141  }
142  break;
143 
144  case WRITE:
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;
151  }
152  else {
153  if ((*i).second != (*d_indexType)) {
154  d_unknown = true;
155  break;
156  }
157  }
158  }
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;
163  }
164  else {
165  if ((*i).second != (*d_elementType)) {
166  d_unknown = true;
167  }
168  }
169  }
170  break;
171 
172  case APPLY:
173  // Expand lambda applications
174  if (e2.getOpKind() == LAMBDA) {
175  Expr lambda(e2.getOpExpr());
176  Expr body(lambda.getBody());
177  const vector<Expr>& vars = lambda.getVars();
178  FatalAssert(vars.size() == (size_t)e2.arity(),
179  "wrong number of arguments applied to lambda\n");
180  body = body.substExpr(vars, e2.getKids());
181  e2 = preprocessRec(body, cache);
182  }
183  break;
184 
185  case EQ:
186  if (d_theoryArith->getBaseType(e2[0]) != d_theoryArith->realType())
187  break;
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);
192  }
193  goto arith_rewrites;
194 
195  case UMINUS:
196  if (d_convertToBV) {
197  e2 = Expr(BVUMINUS, e2[0]);
198  break;
199  }
200  if (d_theoryArith->isSyntacticRational(e2, r)) {
201  e2 = preprocessRec(d_em->newRatExpr(r), cache);
202  break;
203  }
204  goto arith_rewrites;
205 
206  case DIVIDE:
207  if (d_convertToBV) {
208  FatalAssert(false, "Conversion of DIVIDE to BV not implemented yet");
209  break;
210  }
211  if (d_theoryArith->isSyntacticRational(e2, r)) {
212  e2 = preprocessRec(d_em->newRatExpr(r), cache);
213  break;
214  }
215  else if (d_convertArith && e2[1].isRational()) {
216  r = e2[1].getRational();
217  if (r != 0) {
218  e2 = d_em->newRatExpr(1/r) * e2[0];
219  e2 = preprocessRec(e2, cache);
220  break;
221  }
222  }
223  goto arith_rewrites;
224 
225  case MINUS:
226  if (d_convertToBV) {
227  e2 = Expr(BVSUB, e2[0], e2[1]);
228  break;
229  }
230  if (d_convertArith) {
231  if (e2[0].isRational() && e2[1].isRational()) {
232  e2 = d_em->newRatExpr(e2[0].getRational() - e2[1].getRational());
233  break;
234  }
235  }
236  goto arith_rewrites;
237 
238  case PLUS:
239  if (d_convertToBV) {
240  e2 = Expr(Expr(BVPLUS, d_em->newRatExpr(d_convertToBV)).mkOp(), e2.getKids());
241  break;
242  }
243  if (d_convertArith) {
244  // Flatten and combine constants
245  vector<Expr> terms;
246  bool changed = false;
247  int numConst = 0;
248  r = 0;
249  Expr::iterator i = e2.begin(), iend = e2.end();
250  for(; i!=iend; ++i) {
251  if ((*i).getKind() == PLUS) {
252  changed = true;
253  Expr::iterator i2 = (*i).begin(), i2end = (*i).end();
254  for (; i2 != i2end; ++i2) {
255  if ((*i2).isRational()) {
256  r += (*i2).getRational();
257  numConst++;
258  }
259  else terms.push_back(*i2);
260  }
261  }
262  else {
263  if ((*i).isRational()) {
264  r += (*i).getRational();
265  numConst++;
266  if (numConst > 1) changed = true;
267  }
268  else terms.push_back(*i);
269  }
270  }
271  if (terms.size() == 0) {
272  e2 = preprocessRec(d_em->newRatExpr(r), cache);
273  break;
274  }
275  else if (terms.size() == 1) {
276  if (r == 0) {
277  e2 = terms[0];
278  break;
279  }
280  else if (r < 0) {
281  e2 = preprocessRec(Expr(MINUS, terms[0], d_em->newRatExpr(-r)), cache);
282  break;
283  }
284  }
285  if (changed) {
286  if (r != 0) terms.push_back(d_em->newRatExpr(r));
287  e2 = preprocessRec(Expr(PLUS, terms), cache);
288  break;
289  }
290  }
291  goto arith_rewrites;
292 
293  case MULT:
294  if (d_convertToBV) {
295  e2 = Expr(Expr(BVMULT, d_em->newRatExpr(d_convertToBV)).mkOp(), e2.getKids());
296  break;
297  }
298  if (d_convertArith) {
299  // Flatten and combine constants
300  vector<Expr> terms;
301  bool changed = false;
302  int numConst = 0;
303  r = 1;
304  Expr::iterator i = e2.begin(), iend = e2.end();
305  for(; i!=iend; ++i) {
306  if ((*i).getKind() == MULT) {
307  changed = true;
308  Expr::iterator i2 = (*i).begin(), i2end = (*i).end();
309  for (; i2 != i2end; ++i2) {
310  if ((*i2).isRational()) {
311  r *= (*i2).getRational();
312  numConst++;
313  }
314  else terms.push_back(*i2);
315  }
316  }
317  else {
318  if ((*i).isRational()) {
319  r *= (*i).getRational();
320  numConst++;
321  if (numConst > 1) changed = true;
322  }
323  else terms.push_back(*i);
324  }
325  }
326  if (r == 0) {
327  e2 = preprocessRec(d_em->newRatExpr(0), cache);
328  break;
329  }
330  else if (terms.size() == 0) {
331  e2 = preprocessRec(d_em->newRatExpr(r), cache);
332  break;
333  }
334  else if (terms.size() == 1) {
335  if (r == 1) {
336  e2 = terms[0];
337  break;
338  }
339  }
340  if (changed) {
341  if (r != 1) terms.push_back(d_em->newRatExpr(r));
342  e2 = preprocessRec(Expr(MULT, terms), cache);
343  break;
344  }
345  }
346  goto arith_rewrites;
347 
348  case POW:
349  if (d_convertToBV) {
350  FatalAssert(false, "Conversion of POW to BV not implemented");
351  break;
352  }
353  if (d_convertArith && e2[0].isRational()) {
354  r = e2[0].getRational();
355  if (r.isInteger() && r.getNumerator() == 2) {
356  e2 = preprocessRec(e2[1] * e2[1], cache);
357  break;
358  }
359  }
360  // fall through
361 
362  case LT:
363  if (d_convertToBV) {
364  e2 = Expr(BVSLT, e2[0], e2[1]);
365  break;
366  }
367 
368  case GT:
369  if (d_convertToBV) {
370  e2 = Expr(BVSLT, e2[1], e2[0]);
371  break;
372  }
373 
374  case LE:
375  if (d_convertToBV) {
376  e2 = Expr(BVSLE, e2[0], e2[1]);
377  break;
378  }
379 
380  case GE:
381  if (d_convertToBV) {
382  e2 = Expr(BVSLE, e2[1], e2[0]);
383  break;
384  }
385 
386 
387  case INTDIV:
388  case MOD:
389 
390  arith_rewrites:
391  if (d_iteLiftArith) {
392  diff = false;
393  children.clear();
394  vector<Expr> children2;
395  Expr cond;
396  for (int k = 0; k < e2.arity(); ++k) {
397  if (e2[k].getKind() == ITE && !diff) {
398  diff = true;
399  cond = e2[k][0];
400  children.push_back(e2[k][1]);
401  children2.push_back(e2[k][2]);
402  }
403  else {
404  children.push_back(e2[k]);
405  children2.push_back(e2[k]);
406  }
407  }
408  if (diff) {
409  Expr thenpart = Expr(e2.getOp(), children);
410  Expr elsepart = Expr(e2.getOp(), children2);
411  e2 = cond.iteExpr(thenpart, elsepart);
412  e2 = preprocessRec(e2, cache);
413  break;
414  }
415  }
416 
417  if (d_convertToDiff != "" && d_theoryArith->isAtomicArithFormula(e2)) {
418  Expr e3 = d_theoryArith->rewriteToDiff(e2);
419  if (e2 != e3) {
420  DebugAssert(e3 == d_theoryArith->rewriteToDiff(e3), "Expected idempotent rewrite");
421  e2 = preprocessRec(e3, cache);
422  }
423  break;
424  }
425 
426  break;
427  default:
428  if (d_convertToBV && isInt(e2.getType())) {
429  FatalAssert(e2.isVar(), "Cannot convert non-variables yet");
430  e2 = d_theoryCore->newVar(e2.getName()+"_bv", d_theoryBitvector->newBitvectorType(d_convertToBV));
431  }
432 
433  break;
434  }
435 
436  // Figure out language
437  switch (e2.getKind()) {
438  case RATIONAL_EXPR:
439  r = e2.getRational();
440  if (r.isInteger()) {
441  d_intConstUsed = true;
442  }
443  else {
444  d_realUsed = true;
445  }
446  if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
447  break;
448  case IS_INTEGER:
449  d_realUsed = true;
450  d_intUsed = true;
451  break;
452  case PLUS: {
453  if (e2.arity() == 2) {
454  int nonconst = 0, isconst = 0;
455  Expr::iterator i = e2.begin(), iend = e2.end();
456  for(; i!=iend; ++i) {
457  if ((*i).isRational()) {
458  if ((*i).getRational() <= 0) {
459  d_UFIDL_ok = false;
460  break;
461  }
462  else ++isconst;
463  }
464  else ++nonconst;
465  }
466  if (nonconst > 1 || isconst > 1)
467  d_UFIDL_ok = false;
468  }
469  else d_UFIDL_ok = false;
470  if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
471  break;
472  }
473  case MINUS:
474  if (!e2[1].isRational() || e2[1].getRational() <= 0) {
475  d_UFIDL_ok = false;
476  }
477  if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
478  break;
479  case UMINUS:
480  d_UFIDL_ok = false;
481  if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
482  break;
483  case MULT: {
484  d_UFIDL_ok = false;
485  if (d_langUsed == NONLINEAR) break;
486  d_langUsed = LINEAR;
487  bool nonconst = false;
488  for (int i=0; i!=e2.arity(); ++i) {
489  if (e2[i].isRational()) continue;
490  if (nonconst) {
491  d_langUsed = NONLINEAR;
492  break;
493  }
494  nonconst = true;
495  }
496  break;
497  }
498  case POW:
499  case DIVIDE:
500  d_unknown = true;
501  break;
502 
503  case EQ:
504  if (d_theoryArith->getBaseType(e2[0]) != d_theoryArith->realType() ||
505  (e2[0].getType() == d_theoryArith->intType() && d_theoryCore->getFlags()["convert2array"].getBool()))
506  break;
507  case LT:
508  case GT:
509  case LE:
510  case GE:
511  if (d_langUsed >= LINEAR) break;
512  if (!d_theoryArith->isAtomicArithFormula(e2)) {
513  d_langUsed = LINEAR;
514  break;
515  }
516  if (e2[0].getKind() == MINUS &&
517  d_theoryArith->isLeaf(e2[0][0]) &&
518  d_theoryArith->isLeaf(e2[0][1]) &&
519  e2[1].isRational()) {
520  d_langUsed = DIFF_ONLY;
521  break;
522  }
523  if (d_theoryArith->isLeaf(e2[0]) &&
524  d_theoryArith->isLeaf(e2[1])) {
525  d_langUsed = DIFF_ONLY;
526  break;
527  }
528  d_langUsed = LINEAR;
529  break;
530  default:
531  break;
532  }
533 
534  switch (e2.getKind()) {
535  case EQ:
536  case NOT:
537  break;
538  case UCONST:
539  if (e2.arity() == 0) break;
540  default:
541  d_theoryCore->theoryOf(e2)->setUsed();
542  }
543 
544  cache[e] = e2;
545  return e2;
546 }
547 
548 
549 Expr Translator::preprocess(const Expr& e, ExprMap<Expr>& cache)
550 {
551  Expr result;
552  try {
553  result = preprocessRec(e, cache);
554  } catch (SmtlibException& ex) {
555  cerr << "Error while processing the formula:\n"
556  << e.toString() << endl;
557  throw ex;
558  }
559  return result;
560 }
561 
562 
563 Expr Translator::preprocess2Rec(const Expr& e, ExprMap<Expr>& cache, Type desiredType)
564 {
565  TRACE("smtlib2-linear", "preprocess2Rec: ", e, "");
566  ExprMap<Expr>::iterator i(cache.find(e));
567  if(i != cache.end()) {
568  if ((desiredType.isNull() &&
569  (*i).second.getType() != d_theoryArith->realType()) ||
570  (*i).second.getType() == desiredType) {
571  return (*i).second;
572  }
573  }
574 
575  if (e.isClosure()) {
576  Expr newBody = preprocess2Rec(e.getBody(), cache, Type());
577  Expr e2(e);
578  if (newBody != e.getBody()) {
579  e2 = d_em->newClosureExpr(e.getKind(), e.getVars(), newBody);
580  }
581  cache[e] = e2;
582  return e2;
583  }
584 
585  bool forceReal = false;
586  if (desiredType == d_theoryArith->intType() &&
587  e.getType() != d_theoryArith->intType()) {
588  d_unknown = true;
589 // throw SmtlibException("Unable to separate int and real "+
590 // e.getType().getExpr().toString()+
591 // "\n\nwhile processing the term:\n"+
592 // e.toString(PRESENTATION_LANG));
593  }
594 
595  // Try to force type-compliance
596  switch (e.getKind()) {
597  case EQ:
598  case LT:
599  case GT:
600  case LE:
601  case GE:
602  if (e[0].getType() != e[1].getType()) {
603  if (e[0].getType() != d_theoryArith->intType() &&
604  e[1].getType() != d_theoryArith->intType()) {
605  d_unknown = true;
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"+
610  e.toString());
611  }
612  forceReal = true;
613  break;
614  case ITE:
615  case UMINUS:
616  case PLUS:
617  case MINUS:
618  case MULT:
619  if (desiredType == d_theoryArith->realType())
620  forceReal = true;
621  break;
622  case DIVIDE:
623  forceReal = true;
624  break;
625  default:
626  break;
627  }
628  }
629 
630  Expr e2(e);
631  vector<Expr> children;
632  bool diff = false;
633 
634  Type funType;
635  if (e.isApply()) {
636  funType = e.getOpExpr().getType();
637  if (funType.getExpr().getKind() == ANY_TYPE) funType = Type();
638  }
639  else if (e.getKind() == WRITE) {
640  // an array store is like a function ARRAY -> INDEX -> ELEMENT -> ARRAY
641  vector<Type> kids;
642  kids.push_back(e.getType());
643  kids.push_back(e.getType()[0]);
644  kids.push_back(e.getType()[1]);
645  funType = Type::funType(kids, e.getType());
646  }
647 
648  for(int k = 0; k < e.arity(); ++k) {
649  Type t;
650  if (forceReal && e[k].getType() == d_theoryArith->intType())
651  t = d_theoryArith->realType();
652  else if (!funType.isNull()) t = funType[k];
653  // Recursively preprocess the kids
654  Expr child = preprocess2Rec(e[k], cache, t);
655  if (child != e[k]) diff = true;
656  children.push_back(child);
657  }
658  if (diff) {
659  e2 = Expr(e.getOp(), children);
660  }
661  else if (e2.getKind() == RATIONAL_EXPR && d_realUsed && d_intUsed) {
662  if (e2.getType() == d_theoryArith->realType() ||
663  (e2.getType() == d_theoryArith->intType() &&
664  desiredType == d_theoryArith->realType()))
665  e2 = Expr(REAL_CONST, e2);
666  }
667  if (e2.getKind() == MULT) {
668  // SMT-LIBv2 is strict about where * is permitted in linear logics
669  if (d_langUsed > NOT_USED && d_langUsed <= LINEAR &&
670  d_em->getOutputLang() == SMTLIB_V2_LANG) {
671  Expr e2save = e2;
672  TRACE("smtlib2-linear", "SMT-LIBv2 linearizing: ", e2save, "");
673  FatalAssert(e2.arity() > 1, "Unary MULT not permitted here");
674  // combine constants to form a linear term
675  Expr trm;// the singular, non-constant term in the MULT
676  Rational constCoef = 1;// constant coefficient
677  bool realConst = false;
678  bool trmFirst = false;
679  for(int i = 0; i < e2.arity(); ++i) {
680  Expr x = e2[i];
681  if(x.getKind() == REAL_CONST) {
682  x = x[0];
683  realConst = true;
684  DebugAssert(x.isRational(), "unexpected REAL_CONST-wrapped kind");
685  }
686  if(x.isRational()) {
687  constCoef *= x.getRational();
688  } else {
689  FatalAssert(trm.isNull(), "translating with LINEAR restriction, but found > 1 non-constant under MULT");
690  trm = x;
691  trmFirst = (i == 0);
692  }
693  }
694 
695  // First, do no harm: if it was a binary MULT already in correct shape
696  // for SMT-LIBv2 linear logics, use it.
697  if( !( e2.arity() == 2 && !trm.isNull() &&
698  (trm.isApply() || trm.getKind() == READ || trm.isVar()) ) ) {
699  // Otherwise, there are several cases, enumerated below.
700 
701  Expr coef = d_em->newRatExpr(constCoef);
702  if(realConst) {
703  // if any part of the coefficient was wrapped with REAL_CONST to
704  // force printing as a real (e.g. "1.0"), then wrap the combined
705  // coefficient
706  coef = Expr(REAL_CONST, coef);
707  }
708 
709  if(trm.isNull()) {
710  // Case 1: entirely constant; the mult goes away
711  TRACE("smtlib2-linear", "(1) constant", "", "");
712  e2 = coef;
713  } else if(constCoef == 1) {
714  // Case 2: unit coefficient; the mult goes away
715  TRACE("smtlib2-linear", "(2) unit coefficient: ", trm, "");
716  e2 = trm;
717  } else if(trm.getKind() == PLUS || trm.getKind() == MINUS) {
718  // Case 3: have to distribute the MULT over PLUS/MINUS
719  TRACE("smtlib2-linear", "(3) mult over plus/minus: ", trm, "");
720  vector<Expr> kids;
721  for(int i = 0; i < trm.arity(); ++i) {
722  Expr trmi(MULT, coef, trm[i]);
723  trmi = preprocess2Rec(trmi, cache, desiredType);
724  kids.push_back(trmi);
725  }
726  e2 = Expr(trm.getKind(), kids);
727  } else if(trm.getKind() == MULT) {
728  // Case 4: have to distribute MULT over MULT
729  TRACE("smtlib2-linear", "(4) mult over mult: ", trm, "");
730  vector<Expr> kids;
731  kids.push_back(coef);
732  for(int i = 0; i < trm.arity(); ++i) {
733  kids.push_back(trm[i]);
734  }
735  e2 = Expr(MULT, kids);
736  e2 = preprocess2Rec(e2, cache, desiredType);
737  } else if(trm.getKind() == ITE) {
738  // Case 5: have to distribute MULT over ITE
739  TRACE("smtlib2-linear", "(5) mult over ite: ", trm, "");
740  Expr thn = Expr(MULT, coef, trm[1]);
741  Expr els = Expr(MULT, coef, trm[2]);
742  thn = preprocess2Rec(thn, cache, desiredType);
743  els = preprocess2Rec(els, cache, desiredType);
744  e2 = Expr(ITE, trm[0], thn, els);
745  } else {
746  // Default case:
747  TRACE("smtlib2-linear", "(*) coef, trm: ", coef, trm);
748  // don't change order if not necessary (makes it easier to inspect the translation)
749  if(trmFirst) {
750  e2 = Expr(MULT, trm, coef);
751  } else {
752  e2 = Expr(MULT, coef, trm);
753  }
754  FatalAssert(trm.isVar(), string("translating with LINEAR restriction, but found malformed MULT over term that's not a free constant: ") + e2.toString());
755  }
756  } else {
757  TRACE("smtlib2-linear", "(x) no handling necessary: ", trm, "");
758  }
759  TRACE("smtlib2-linear", "SMT-LIBv2 linearized: ", e2save, "");
760  TRACE("smtlib2-linear", " into: ", e2, "");
761  }
762  }
763 
764  if (!desiredType.isNull() && e2.getType() != desiredType) {
765  if(isInt(e2.getType()) && isReal(desiredType) && !d_intUsed) {
766  // the implicit cast is ok here
767  } else {
768  d_unknown = true;
769  throw SmtlibException("Type error: expected "+
770  desiredType.getExpr().toString()+
771  " but instead got "+
772  e2.getType().getExpr().toString()+
773  "\n\nwhile processing term:\n"+
774  e.toString());
775  }
776  }
777 
778  cache[e] = e2;
779  return e2;
780 }
781 
782 
783 Expr Translator::preprocess2(const Expr& e, ExprMap<Expr>& cache)
784 {
785  Expr result;
786  try {
787  result = preprocess2Rec(e, cache, Type());
788  } catch (SmtlibException& ex) {
789  cerr << "Error while processing the formula:\n"
790  << e.toString() << endl;
791  throw ex;
792  }
793  return result;
794 }
795 
796 
797 
798 
799 bool Translator::containsArray(const Expr& e)
800 {
801  if (e.getKind() == ARRAY) return true;
802  Expr::iterator i = e.begin(), iend=e.end();
803  for(; i!=iend; ++i) if (containsArray(*i)) return true;
804  return false;
805 }
806 
807 
808 Translator::Translator(ExprManager* em,
809  const bool& translate,
810  const bool& real2int,
811  const bool& convertArith,
812  const string& convertToDiff,
813  bool iteLiftArith,
814  const string& expResult,
815  const string& category,
816  bool convertArray,
817  bool combineAssump,
818  int convertToBV)
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)
834 {
835  d_arrayConvertMap = new map<string, Type>;
836 }
837 
838 
840 {
841  delete d_arrayConvertMap;
842 }
843 
844 
845 bool Translator::start(const string& dumpFile)
846 {
847  if (d_translate && (d_em->getOutputLang() == SMTLIB_LANG)) {
848  d_dump = true;
849  if (dumpFile == "") {
850  d_osdump = &cout;
851  }
852  else {
853  d_osdumpFile.open(dumpFile.c_str());
854  if(!d_osdumpFile)
855  throw Exception("cannot open a log file: "+dumpFile);
856  else {
857  d_dumpFileOpen = true;
859  }
860  }
861 
862  string tmpName;
863  string::size_type pos = dumpFile.rfind("/");
864  if (pos == string::npos) {
865  tmpName = "README";
866  }
867  else {
868  tmpName = dumpFile.substr(0,pos+1) + "README";
869  }
870  d_tmpFile.open(tmpName.c_str());
871 
872  *d_osdump << "(benchmark " << fileToSMTLIBIdentifier(dumpFile) << endl
873  << " :source {" << endl;
874 
875  char c;
876  if (d_tmpFile.is_open()) {
877  d_tmpFile.get(c);
878  while (!d_tmpFile.eof()) {
879  if ( c == '{' || c == '}' ) {
880  *d_osdump << '\\';
881  }
882  *d_osdump << c;
883  d_tmpFile.get(c);
884  }
885  }
886  else {
887  *d_osdump << "Source unknown";
888  }
889  *d_osdump << endl;
890 
891  *d_osdump << "}" << endl;
892 
893  d_tmpFile.close();
894  }
895  else if (d_translate && d_em->getOutputLang() == SPASS_LANG) {
896  d_dump = true;
897  if (dumpFile == "") {
898  d_osdump = &cout;
899  }
900  else {
901  d_osdumpFile.open(dumpFile.c_str());
902  if(!d_osdumpFile)
903  throw Exception("cannot open a log file: "+dumpFile);
904  else {
905  d_dumpFileOpen = true;
907  }
908  }
909 
910  *d_osdump << "begin_problem(Unknown). " << endl;
911  *d_osdump << endl;
912  *d_osdump << "list_of_descriptions. " << endl;
913  *d_osdump << "name({* " << fileToSMTLIBIdentifier(dumpFile) << " *}). " << endl;
914  *d_osdump << "author({* CVC2SPASS translator *})." << endl;
915  //end of SPASS
916  }
917  else {
918  if (dumpFile == "") {
919  if (d_translate) {
920  d_osdump = &cout;
921  d_dump = true;
922  }
923  }
924  else {
925  d_osdumpFile.open(dumpFile.c_str());
926  if(!d_osdumpFile)
927  throw Exception("cannot open a log file: "+dumpFile);
928  else {
929  d_dump = true;
930  d_dumpFileOpen = true;
932  }
933  }
934  }
935  return d_dump;
936 }
937 
938 
939 void Translator::dump(const Expr& e, bool dumpOnly)
940 {
941  DebugAssert(d_dump, "dump called unexpectedly");
942  if (!dumpOnly || !d_translate) {
943  if (d_convertArray && e.getKind() == CONST &&
944  e.arity() == 2) {
945  if (e[1].getKind() == ARRAY) {
946  if (containsArray(e[1][0]) ||
947  containsArray(e[1][1])) {
948  throw Exception("convertArray failed because of nested arrays in"+
949  e[1].toString());
950  }
951  Expr funType = Expr(ARROW, e[1][0], e[1][1]);
952  Expr outExpr = Expr(CONST, e[0], funType);
953  d_dumpExprs.push_back(outExpr);
954  }
955  else if (containsArray(e[1])) {
956  throw Exception("convertArray failed becauase of use of arrays in"+
957  e[1].toString());
958  }
959  else {
960  d_dumpExprs.push_back(e);
961  }
962  }
963  else {
964  d_dumpExprs.push_back(e);
965  }
966  }
967 }
968 
969 
971 {
972  Expr outExpr = Expr(ASSERT, e);
973  d_dumpExprs.push_back(outExpr);
974  return d_translate;
975 }
976 
977 
979 {
980  Expr outExpr = Expr(QUERY, e);
981  d_dumpExprs.push_back(outExpr);
982  return d_translate;
983 }
984 
985 
987 {
988  if( d_translate && d_em->getOutputLang() == SMTLIB_LANG ) {
989  *d_osdump << " :status ";
990  switch( qres ) {
991  case UNSATISFIABLE:
992  *d_osdump << "unsat" << endl;
993  break;
994  case SATISFIABLE:
995  *d_osdump << "sat" << endl;
996  break;
997  default:
998  *d_osdump << "unknown" << endl;
999  break;
1000  }
1001  } else if( d_translate && d_em->getOutputLang() == SMTLIB_V2_LANG ) {
1002  *d_osdump << "(set-info :status ";
1003  switch( qres ) {
1004  case UNSATISFIABLE:
1005  *d_osdump << "unsat";
1006  break;
1007  case SATISFIABLE:
1008  *d_osdump << "sat";
1009  break;
1010  default:
1011  *d_osdump << "unknown";
1012  break;
1013  }
1014  *d_osdump << ")" << endl;
1015  } else if( d_translate && d_em->getOutputLang() == SPASS_LANG ) {
1016  *d_osdump << "status(";
1017  switch( qres ) {
1018  case UNSATISFIABLE:
1019  *d_osdump << "unsatisfiable";
1020  break;
1021  case SATISFIABLE:
1022  *d_osdump << "satisfiable";
1023  break;
1024  default:
1025  *d_osdump << "unknown";
1026  break;
1027  }
1028  *d_osdump << ")." << endl;
1029  }
1030 }
1031 
1032 
1033 /*
1034 Expr Translator::spassPreprocess(const Expr& e, ExprMap<Expr>& mapping,
1035  vector<Expr>& functions,
1036  vector<Expr>& predicates)
1037 {
1038  if(e.getKind() == LET) {
1039  if(e.arity() != 2) {
1040  throw SmtlibException("Translator::spassPreprocess(): LET with arity != 2 not supported");
1041  }
1042  char name[80];
1043  snprintf(name, sizeof(name), "_cvc3_let%u", mapping.size());
1044  Expr id(ID, d_em->newStringExpr(name));
1045  cout << "ENCOUNTERED A LET:" << endl << id << endl;
1046  mapping.insert(e[0][0], e[0][1]);
1047  functions.push_back(Expr(CONST, id, e[1].getType().getExpr()));
1048  return spassPreprocess(e[1], mapping, functions, predicates);
1049  //} else if(e.getKind() == x) {
1050  } else if(e.arity() > 0) {
1051  vector<Expr> args;
1052  for(int i = 0, iend = e.arity(); i < iend; ++i) {
1053  args.push_back(spassPreprocess(e[i], mapping, functions, predicates));
1054  }
1055  Expr out(e.getOp(), args);
1056  return out;
1057  }
1058  return e;
1059 }
1060 */
1061 
1062 
1064 {
1065  switch (e.getKind()) {
1066  case TYPEDECL:
1067  return e;
1068  case INT:
1069  if (d_convertToBV) {
1071  }
1072  if (d_theoryCore->getFlags()["convert2array"].getBool()) {
1073  return d_elementType->getExpr();
1074  }
1075  d_intUsed = true;
1076  break;
1077  case REAL:
1078  if (d_real2int) {
1079  d_intUsed = true;
1080  return d_theoryArith->intType().getExpr();
1081  }
1082  else {
1083  d_realUsed = true;
1084  }
1085  break;
1086  case SUBRANGE:
1087  d_unknown = true;
1088  break;
1089  case ARRAY:
1090  if (d_theoryCore->getFlags()["convert2array"].getBool()) {
1091  d_ax = true;
1092  return d_arrayType->getExpr();
1093  }
1094  if (e[0].getKind() == TYPEDECL) {
1095  DebugAssert(e[0].arity() == 1, "expected arity 1");
1096  if (e[0][0].getString() == "Index") {
1097  if (e[1].getKind() == TYPEDECL) {
1098  DebugAssert(e[1].arity() == 1, "expected arity 1");
1099  if (e[1][0].getString() == "Element") {
1100  d_ax = true;
1101  break;
1102  }
1103  }
1104  }
1105  }
1106  else if (isInt(Type(e[0]))) {
1107  if (isInt(Type(e[1]))) {
1108  d_intIntArray = true;
1109  break;
1110  }
1111  else if (isReal(Type(e[1]))) {
1112  d_intRealArray = true;
1113  break;
1114  }
1115  else if (isArray(Type(e[1])) &&
1116  isInt(Type(e[1][0])) &&
1117  isReal(Type(e[1][1]))) {
1118  d_intIntRealArray = true;
1119  break;
1120  }
1121  }
1122  else if (e[0].getKind() == BITVECTOR &&
1123  e[1].getKind() == BITVECTOR) {
1124  break;
1125  }
1126  d_unknown = true;
1127  break;
1128  default:
1129  break;
1130  }
1131  d_theoryCore->theoryOf(e)->setUsed();
1132  if (e.arity() == 0) return e;
1133  bool changed = false;
1134  vector<Expr> vec;
1135  for (int i = 0; i < e.arity(); ++i) {
1136  vec.push_back(processType(e[i]));
1137  if (vec.back() != e[i]) changed = true;
1138  }
1139  if (changed)
1140  return Expr(e.getOp(), vec);
1141  return e;
1142 }
1143 
1144 
1146 {
1147  bool qf_uf = false;
1148 
1149  if (d_translate) {
1150 
1151  if (d_em->getOutputLang() == SPASS_LANG) {
1152  *d_osdump << "status(";
1153  if (d_expResult == "invalid" ||
1154  d_expResult == "satisfiable" ||
1155  d_expResult == "sat")
1156  *d_osdump << "satisfiable";
1157  else if (d_expResult == "valid" ||
1158  d_expResult == "unsatisfiable" ||
1159  d_expResult == "unsat")
1160  *d_osdump << "unsatisfiable";
1161  else if (d_expResult != "")
1162  *d_osdump << "unknown";
1163  else if (status() == "invalid" ||
1164  status() == "satisfiable" ||
1165  status() == "sat")
1166  *d_osdump << "satisfiable";
1167  else if (status() == "valid" ||
1168  status() == "unsatisfiable" ||
1169  status() == "unsat")
1170  *d_osdump << "unsatisfiable";
1171  else *d_osdump << "unknown";
1172  *d_osdump << ")." << endl;
1173  *d_osdump << "description({* Unknown *})." << endl;
1174  *d_osdump << "end_of_list." << endl;
1175 
1176  vector<Expr> functions, predicates, sorts;
1177 
1178  for(vector<Expr>::reverse_iterator i = d_dumpExprs.rbegin(), iend = d_dumpExprs.rend(); i != iend; ++i) {
1179  Expr e = *i;
1180  switch(e.getKind()) {
1181  case TYPE:
1182  sorts.push_back(e);
1183  d_dumpExprs.erase(i.base() - 1);
1184  break;
1185  case CONST:
1186  if(e.arity() == 2) {
1187  if (e[1].getKind() == BOOLEAN ||
1188  (e[1].getKind() == ARROW && e[1][e[1].arity()-1].getKind() == BOOLEAN)) {
1189  predicates.push_back(e);
1190  } else {
1191  functions.push_back(e);
1192  }
1193  d_dumpExprs.erase(i.base() - 1);
1194  } else {
1195  throw SmtlibException("Translator::finish: SPASS_LANG: CONST not implemented for arity != 2");
1196  }
1197  break;
1198  case ANNOTATION:
1199  if (d_theoryCore->getFlags()["trans-skip-difficulty"].getBool() &&
1200  e[0].getKind() == STRING_EXPR && e[0].getString() == "difficulty") {
1201  // do nothing; skip the difficulty annotation
1202  } else {
1203  *d_osdump << "%% ";
1204  *d_osdump << e[0];
1205  if (e.arity() > 1) {
1206  *d_osdump << ": " << e[1];
1207  }
1208  }
1209  d_dumpExprs.erase(i.base() - 1);
1210  break;
1211 
1212  /*
1213  case ASSERT:
1214  case QUERY: {
1215  ExprMap<Expr> m;
1216  *i = Expr(e.getKind(), spassPreprocess(e[0], m, functions, predicates));
1217  break;
1218  }
1219  */
1220 
1221  default:
1222  //*d_osdump << "DOING NOTHING FOR: " << e << endl;
1223  break;
1224  }
1225  }
1226 
1227  // add some built-ins for the translation
1228  // only arity matters for SPASS; the real type of _cvc3_ite is Bool -> 'a -> 'a -> 'a
1229  //Expr cvc3ite(CONST, Expr(ID, d_em->newStringExpr("_cvc3_ite")),
1230  //Expr(ARROW, vector<Expr>(4, d_theoryArith->intType().getExpr())));
1231  // only arity matters for SPASS; the real type of _cvc3_xor is
1232  // Bool -> Bool -> Bool, but we can't represent Bool-arg'ed
1233  // functions
1234  /*
1235  Expr cvc3xor(CONST, Expr(ID, d_em->newStringExpr("_cvc3_xor")),
1236  Expr(ARROW, vector<Expr>(2, d_theoryArith->intType().getExpr())));
1237  //functions.push_back(cvc3ite);
1238  predicates.push_back(cvc3xor);
1239  */
1240 
1241  *d_osdump << endl;
1242  *d_osdump << "list_of_symbols." << endl;
1243  if(!functions.empty()) {
1244  *d_osdump << "functions[";
1245  vector<Expr>::reverse_iterator i = functions.rbegin(), iend = functions.rend();
1246  while(i != iend) {
1247  Expr e = *i;
1248  string name = e[0][0].getString();
1249  if(isReal(d_theoryCore->getBaseType(Type(e[1])))) {
1250  // SPASS guys want "np" prefix on arith vars
1251  name = "np" + name;
1252  }
1253  *d_osdump << "(" << name << "," << ( e[1].getKind() == ARROW ? e[1].arity()-1 : e[1].arity() ) << ")";
1254  if(++i != iend) {
1255  *d_osdump << ",";
1256  }
1257  }
1258  *d_osdump << "]." << endl;
1259  }
1260  if(!predicates.empty()) {
1261  *d_osdump << "predicates[";
1262  vector<Expr>::reverse_iterator i = predicates.rbegin(), iend = predicates.rend();
1263  while(i != iend) {
1264  Expr e = *i;
1265  *d_osdump << "(" << e[0][0].getString() << "," << e[1].arity() << ")";
1266  if(++i != iend) {
1267  *d_osdump << ",";
1268  }
1269  }
1270  *d_osdump << "]." << endl;
1271  }
1272  if(!sorts.empty()) {
1273  *d_osdump << "sorts[";
1274  vector<Expr>::reverse_iterator i = sorts.rbegin(), iend = sorts.rend();
1275  while(i != iend) {
1276  Expr e = *i;
1277  *d_osdump << e[0][0].getString();
1278  if(++i != iend) {
1279  *d_osdump << ",";
1280  }
1281  }
1282  *d_osdump << "]." << endl;
1283  }
1284  *d_osdump << "end_of_list." << endl;
1285 
1286  /*
1287  *d_osdump << endl;
1288  *d_osdump << "list_of_declarations." << endl;
1289  *d_osdump << "end_of_list." << endl;
1290  */
1291 
1292  // define an ITE operator for the translation
1293  /*
1294  *d_osdump << endl;
1295  *d_osdump << "list_of_formulae(axioms)." << endl;
1296  *d_osdump << "formula( forall([A,B],equiv(_cvc3_xor(A,B),not(equal(A,B)))) )." << endl;
1297  // *d_osdump << "formula(forall([A,B],equal(_cvc3_ite(\ntrue\n,A,B),A)))." << endl;
1298  // *d_osdump << "formula(forall([A,B],equal(_cvc3_ite(\nfalse\n,A,B),B)))." << endl;
1299  *d_osdump << "end_of_list." << endl;
1300  */
1301 
1302  *d_osdump << endl;
1303  *d_osdump << "list_of_formulae(conjectures)." << endl;
1304  }
1305 
1306  if (d_em->getOutputLang() == SMTLIB_LANG) {
1307  // Print the rest of the preamble for smt-lib benchmarks
1308 
1309  // Get status from expResult flag
1310  *d_osdump << " :status ";
1311  if (d_expResult == "invalid" ||
1312  d_expResult == "satisfiable")
1313  *d_osdump << "sat";
1314  else if (d_expResult == "valid" ||
1315  d_expResult == "unsatisfiable")
1316  *d_osdump << "unsat";
1317  else if (status() != "") {
1318  *d_osdump << status();
1319  }
1320  else *d_osdump << "unknown";
1321  *d_osdump << endl;
1322 
1323  // difficulty
1324  // *d_osdump << " :difficulty { unknown }" << endl;
1325 
1326  // category
1327  if (category() != "") {
1328  *d_osdump << " :category { ";
1329  *d_osdump << category() << " }" << endl;
1330  }
1331 
1332  // Create types for theory QF_AX if needed
1333  if (d_theoryCore->getFlags()["convert2array"].getBool()) {
1334  d_indexType = new Type(d_theoryCore->newTypeExpr("Index"));
1335  d_elementType = new Type(d_theoryCore->newTypeExpr("Element"));
1336  d_arrayType = new Type(arrayType(*d_indexType, *d_elementType));
1337  }
1338  }
1339 
1340  // Preprocess and compute logic for smt-lib
1341 
1342  if (!d_theoryCore->getFlags()["trans-skip-pp"].getBool())
1343  {
1344  ExprMap<Expr> cache;
1345  // Step 1: preprocess asserts, queries, and types
1346  vector<Expr>::iterator i = d_dumpExprs.begin(), iend = d_dumpExprs.end();
1347  for (; i != iend; ++i) {
1348  Expr e = *i;
1349  switch (e.getKind()) {
1350  case ASSERT: {
1351  Expr e2 = preprocess(e[0], cache);
1352  if (e[0] == e2) break;
1353  e2.getType();
1354  *i = Expr(ASSERT, e2);
1355  break;
1356  }
1357  case QUERY: {
1358  Expr e2 = preprocess(e[0].negate(), cache);
1359  if (e[0].negate() == e2) break;
1360  e2.getType();
1361  *i = Expr(QUERY, e2.negate());
1362  break;
1363  }
1364  case CONST: {
1365  DebugAssert(e.arity() == 2, "Expected CONST with arity 2");
1366  if (d_theoryCore->getFlags()["convert2array"].getBool()) break;
1367  Expr e2 = processType(e[1]);
1368  if (e[1] == e2) break;
1369  if (d_convertToBV) {
1370  Expr newName = Expr(ID, d_em->newStringExpr(e[0][0].getString()+"_bv"));
1371  *i = Expr(CONST, newName, e2);
1372  }
1373  else {
1374  *i = Expr(CONST, e[0], e2);
1375  }
1376  break;
1377  }
1378  default:
1379  break;
1380  }
1381  }
1382  }
1383 
1384  if (d_zeroVar) {
1385  d_dumpExprs.insert(d_dumpExprs.begin(),
1386  Expr(CONST, Expr(ID, d_em->newStringExpr("cvc3Zero")),
1388  }
1389 
1390  // Type inference over equality
1391  if (!d_unknown && d_theoryCore->getFlags()["convert2array"].getBool()) {
1392  bool changed;
1393  do {
1394  changed = false;
1395  unsigned i;
1396  for (i = 0; i < d_equalities.size(); ++i) {
1397  if (d_equalities[i][0].getKind() == UCONST &&
1398  d_arrayConvertMap->find(d_equalities[i][0].getName()) == d_arrayConvertMap->end()) {
1399  if (d_equalities[i][1].getKind() == READ) {
1400  changed = true;
1401  (*d_arrayConvertMap)[d_equalities[i][0].getName()] = *d_elementType;
1402  }
1403  else if (d_equalities[i][1].getKind() == UCONST) {
1404  map<string, Type>::iterator it = d_arrayConvertMap->find(d_equalities[i][1].getName());
1405  if (it != d_arrayConvertMap->end()) {
1406  changed = true;
1407  (*d_arrayConvertMap)[d_equalities[i][0].getName()] = (*it).second;
1408  }
1409  }
1410  }
1411  else if (d_equalities[i][1].getKind() == UCONST &&
1412  d_arrayConvertMap->find(d_equalities[i][1].getName()) == d_arrayConvertMap->end()) {
1413  if (d_equalities[i][0].getKind() == READ) {
1414  changed = true;
1415  (*d_arrayConvertMap)[d_equalities[i][1].getName()] = *d_elementType;
1416  }
1417  else if (d_equalities[i][0].getKind() == UCONST) {
1418  map<string, Type>::iterator it = d_arrayConvertMap->find(d_equalities[i][0].getName());
1419  if (it != d_arrayConvertMap->end()) {
1420  changed = true;
1421  (*d_arrayConvertMap)[d_equalities[i][1].getName()] = (*it).second;
1422  }
1423  }
1424  }
1425  }
1426  } while (changed);
1427  }
1428 
1429  if (d_em->getOutputLang() == SMTLIB_LANG ||
1431 
1432  // Step 2: If both int and real are used, try to separate them
1433  if ((!d_unknown && (d_intUsed && d_realUsed)) ||
1434  d_theoryCore->getFlags()["convert2array"].getBool() ||
1435  ( d_em->getOutputLang() == SMTLIB_V2_LANG &&
1436  d_langUsed > NOT_USED && d_langUsed <= LINEAR )) {
1437  ExprMap<Expr> cache;
1438  vector<Expr>::iterator i = d_dumpExprs.begin(), iend = d_dumpExprs.end();
1439  for (; i != iend; ++i) {
1440  Expr e = *i;
1441  switch (e.getKind()) {
1442  case ASSERT: {
1443  if (d_theoryCore->getFlags()["convert2array"].getBool()) break;
1444  Expr e2 = preprocess2(e[0], cache);
1445  e2.getType();
1446  *i = Expr(ASSERT, e2);
1447  break;
1448  }
1449  case QUERY: {
1450  if (d_theoryCore->getFlags()["convert2array"].getBool()) break;
1451  Expr e2 = preprocess2(e[0].negate(), cache);
1452  e2.getType();
1453  *i = Expr(QUERY, e2.negate());
1454  break;
1455  }
1456  case CONST: {
1457  if (!d_theoryCore->getFlags()["convert2array"].getBool()) break;
1458  map<string, Type>::iterator it = d_arrayConvertMap->find(e[0][0].getString());
1459  if (it != d_arrayConvertMap->end()) {
1460  *i = Expr(CONST, e[0], (*it).second.getExpr());
1461  }
1462  else {
1463  Expr e2 = processType(e[1]);
1464  if (e[1] == e2) break;
1465  *i = Expr(CONST, e[0], e2);
1466  }
1467  break;
1468  }
1469  default:
1470  break;
1471  }
1472  }
1473  }
1474  d_arithUsed = d_realUsed || d_intUsed || d_intConstUsed || (d_langUsed != NOT_USED);
1475 
1476  // Step 3: Go through the cases and figure out the right logic
1477  if (d_em->getOutputLang() == SMTLIB_LANG) {
1478  *d_osdump << " :logic ";
1479  }
1480  else {// d_em->getOutputLang() == SMTLIB_V2_LANG
1481  *d_osdump << "(set-logic ";
1482  }
1483  if (d_unknown ||
1487  *d_osdump << "unknown";
1488  }
1489  else {
1490  if ((d_ax && (d_arithUsed ||
1492  d_theoryUF->theoryUsed())) ||
1493  (d_intIntArray && d_realUsed) ||
1495  *d_osdump << "unknown";
1496  }
1497  else {
1498  bool QF = false;
1499  bool A = false;
1500  bool UF = false;
1501  bool promote = d_theoryCore->getFlags()["promote"].getBool();
1502 
1503  if (!d_theoryQuant->theoryUsed()) {
1504  QF = true;
1505  *d_osdump << "QF_";
1506  }
1507 
1509  A = true;
1510  *d_osdump << "A";
1511  }
1512 
1513  // Promote undefined subset logics
1514  else if (promote &&
1515  !QF &&
1516  !(d_arithUsed && d_realUsed && !d_intUsed && d_langUsed <= LINEAR) &&
1517  !(d_arithUsed && !d_realUsed && d_intUsed && d_langUsed == NONLINEAR)) {
1518  A = true;
1519  *d_osdump << "A";
1520  }
1521 
1522  if (d_theoryUF->theoryUsed() ||
1524  UF = true;
1525  *d_osdump << "UF";
1526  }
1527 
1528  // Promote undefined subset logics
1529  else if (promote &&
1530  !QF &&
1531  !(d_arithUsed && d_realUsed && !d_intUsed && d_langUsed <= LINEAR)) {
1532  UF = true;
1533  *d_osdump << "UF";
1534  }
1535 
1536  if (d_arithUsed) {
1537  if (d_intUsed && d_realUsed) {
1538  if (d_langUsed < NONLINEAR) {
1539  *d_osdump << "LIRA";
1540  }
1541  else *d_osdump << "NIRA";
1542  }
1543  else if (d_realUsed) {
1544  if (d_langUsed <= DIFF_ONLY) {
1545 
1546  // Promote undefined subset logics
1547  if (promote && !QF) {
1548  *d_osdump << "LRA";
1549  } else
1550 
1551  *d_osdump << "RDL";
1552  }
1553  else if (d_langUsed <= LINEAR) {
1554  *d_osdump << "LRA";
1555  }
1556  else {
1557 
1558  // Promote undefined subset logics
1559  if (promote && !QF) {
1560  *d_osdump << "NIRA";
1561  } else
1562 
1563  *d_osdump << "NRA";
1564  }
1565  }
1566  else {
1567  if (QF && !A && UF && d_langUsed <= LINEAR) {
1568  if (!d_realUsed && d_langUsed <= LINEAR && d_UFIDL_ok) {
1569  *d_osdump << "IDL";
1570  }
1571  else {
1572  *d_osdump << "LIA";
1573  }
1574  }
1575  else if (d_langUsed <= DIFF_ONLY) {
1576 
1577  // Promote undefined subset logics
1578  if (promote && !QF) {
1579  *d_osdump << "LIA";
1580  }
1581  else if (A) {
1582  if (!UF) {
1583  UF = true;
1584  *d_osdump << "UF";
1585  }
1586  *d_osdump << "LIA";
1587  } else
1588 
1589  *d_osdump << "IDL";
1590  }
1591  else if (d_langUsed <= LINEAR) {
1592 
1593  // Promote undefined subset logics
1594  if (promote && QF && A && !UF) {
1595  UF = true;
1596  *d_osdump << "UF";
1597  }
1598 
1599  if (QF && !A && (!d_realUsed && d_langUsed <= LINEAR && d_UFIDL_ok)) {
1600  *d_osdump << "UFIDL";
1601  }
1602  else {
1603  *d_osdump << "LIA";
1604  }
1605  }
1606  else {
1607  *d_osdump << "NIA";
1608  }
1609  }
1610  }
1611  else if (d_theoryBitvector->theoryUsed()) {
1612 
1613  // Promote undefined subset logics
1614  if (promote && A && QF && !UF) {
1615  UF = true;
1616  *d_osdump << "UF";
1617  }
1618 
1619  *d_osdump << "BV";
1620  }
1621  else {
1622 
1623  if (d_ax) {
1624  *d_osdump << "X";
1625  }
1626 
1627  // Promote undefined subset logics
1628  else if (promote && (!QF || (A && UF))) {
1629  *d_osdump << "LIA";
1630  } else {
1631 
1632  // Default logic
1633  if (!A && !UF) {
1634  UF = true;
1635  *d_osdump << "UF";
1636  }
1637  qf_uf = QF && UF && (!A);
1638  }
1639  }
1640  }
1641  }
1642  if (d_em->getOutputLang() == SMTLIB_V2_LANG) {
1643  *d_osdump << ")";
1644  }
1645  *d_osdump << endl;
1646  }
1647 
1648  if (d_em->getOutputLang() == SMTLIB_V2_LANG) {
1649  // Print the rest of the set-info commands
1650 
1651  if (source() != "") {
1652  *d_osdump << "(set-info :source "
1653  << quoteAnnotation(source())
1654  << ')' << endl;
1655  }
1656 
1657  *d_osdump << "(set-info :smt-lib-version 2.0)" << endl;
1658 
1659  // Remove leading and trailing spaces from category
1660  string c = category();
1661  size_t i = 0, j = c.size();
1662  while (c[i] == ' ') {
1663  ++i; --j;
1664  }
1665  while (j > 0 && c[i+j-1] == ' ') --j;
1666  if (j > 0) {
1667  c = c.substr(i,j);
1668  *d_osdump << "(set-info :category \"" << c << "\")" << endl;
1669  }
1670 
1671 // if (benchName() != "") {
1672 // *d_osdump << "(set-info :name \"" << benchName() << "\")" << endl;
1673 // }
1674 
1675  // Get status from expResult flag
1676  *d_osdump << "(set-info :status ";
1677  if (d_expResult == "invalid" ||
1678  d_expResult == "satisfiable")
1679  *d_osdump << "sat";
1680  else if (d_expResult == "valid" ||
1681  d_expResult == "unsatisfiable")
1682  *d_osdump << "unsat";
1683  else if (status() != "") {
1684  *d_osdump << status();
1685  }
1686  else *d_osdump << "unknown";
1687  *d_osdump << ")" << endl;
1688 
1689  // Create types for theory QF_AX if needed
1690  if (d_theoryCore->getFlags()["convert2array"].getBool()) {
1691  d_indexType = new Type(d_theoryCore->newTypeExpr("Index"));
1692  d_elementType = new Type(d_theoryCore->newTypeExpr("Element"));
1693  d_arrayType = new Type(arrayType(*d_indexType, *d_elementType));
1694  }
1695  }
1696 
1697  if (d_em->getOutputLang() == PRESENTATION_LANG) {
1698  // If we translate SMT-LIBv2 to PRESENTATION, we should set
1699  // "no-save-model" so that multiple-query benchmarks give
1700  // the same results in both languages.
1701  //
1702  // Translation the other way doesn't work, since SMT-LIBv2
1703  // doesn't support CVC3 presentation language semantics.
1704  if(d_theoryCore->getFlags()["no-save-model"].getBool()) {
1705  *d_osdump << "OPTION \"no-save-model\" 1;" << endl;
1706  }
1707  }
1708  }
1709 
1710  if (d_dump) {
1711  // Dump the actual expressions
1712  vector<Expr>::const_iterator i = d_dumpExprs.begin(), iend = d_dumpExprs.end();
1713  vector<Expr> assumps;
1714  bool skip_diff = d_theoryCore->getFlags()["trans-skip-difficulty"].getBool();
1715  for (; i != iend; ++i) {
1716  Expr e = *i;
1717  switch (e.getKind()) {
1718  case ASSERT: {
1719  if (d_combineAssump) {
1720  assumps.push_back(e[0]);
1721  }
1722  else {
1723  *d_osdump << e << endl;
1724  }
1725  break;
1726  }
1727  case QUERY: {
1728  if (!assumps.empty()) {
1729  assumps.push_back(e[0].negate());
1730  e = Expr(QUERY, Expr(NOT, Expr(AND, assumps)));
1731  }
1732  *d_osdump << e << endl;
1733  break;
1734  }
1735  default:
1736  if (d_em->getOutputLang() == SMTLIB_LANG &&
1737  qf_uf && e.getKind() == TYPE && e[0].getKind() == RAW_LIST &&
1738  e[0][0].getKind() == ID && e[0][0][0].getKind() == STRING_EXPR &&
1739  e[0][0][0].getString() == "U")
1740  break;
1741  if (d_em->getOutputLang() == SMTLIB_LANG &&
1742  d_ax && e.getKind() == TYPE && e[0].getKind() == RAW_LIST &&
1743  e[0][0].getKind() == ID && e[0][0][0].getKind() == STRING_EXPR &&
1744  ( e[0][0][0].getString() == "Index" ||
1745  e[0][0][0].getString() == "Element" ))
1746  break;
1747  if (skip_diff && e.getKind() == ANNOTATION && e[0].getKind() == STRING_EXPR &&
1748  e[0].getString() == "difficulty")
1749  break;
1750  if (d_em->getOutputLang() == SMTLIB_V2_LANG &&
1751  (e.getKind() == CONST && e[0].getKind() == ID) &&
1752  (d_realUsed || d_intUsed)) {
1753  if (e[0][0].getString() == "abs") {
1754  // [MGD] Some benchmarks define their own abs, but we have to
1755  // rename it in the benchmark becuase in SMTLIBv2 the Reals and
1756  // Ints and Reals_Ints theories define abs.
1757  d_replaceSymbols["abs"] = "abs_";
1758  } else if (e[0][0].getString() == "mod") {
1759  // ditto for mod
1760  d_replaceSymbols["mod"] = "mod_";
1761  }
1762  }
1763  *d_osdump << e << endl;
1764  break;
1765  }
1766  }
1767  }
1768  if (d_translate) {
1769  if (d_em->getOutputLang() == SMTLIB_LANG) {
1770  *d_osdump << ")" << endl;
1771  }
1772  else if (d_em->getOutputLang() == SMTLIB_V2_LANG) {
1773  *d_osdump << "(exit)" << endl;
1774  }
1775 
1776  if (d_em->getOutputLang() == SPASS_LANG) {
1777  *d_osdump << "end_of_list." << endl;
1778  *d_osdump << endl;
1779  *d_osdump << "list_of_settings(SPASS)." << endl
1780  << "{*" << 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
1792  << "*}" << endl
1793  << "end_of_list." << endl;
1794  *d_osdump << endl;
1795  *d_osdump << "end_problem." << endl;
1796  }
1797  }
1798 
1799  if (d_dumpFileOpen) d_osdumpFile.close();
1800  if (d_zeroVar) delete d_zeroVar;
1801 }
1802 
1803 
1804 const string Translator::fixConstName(const string& s)
1805 {
1806  if (d_em->getOutputLang() == SMTLIB_LANG) {
1807  if (s[0] == '_') {
1808  return "smt"+s;
1809  }
1810  }
1812  return (i == d_replaceSymbols.end()) ? s : (*i).second;
1813 }
1814 
1815 
1816 const string Translator::escapeSymbol(const string& s)
1817 {
1818  if (d_em->getOutputLang() == SMTLIB_V2_LANG) {
1819  if (s.length() == 0 || isdigit(s[0]))
1820  return "|" + s + "|";
1821  // This is the legal set of SMTLIB v2 symbol characters from page
1822  // 20 of the SMT-LIB v2.0 spec. If any character in the symbol
1823  // string falls outside this set, the symbol must be |-delimited.
1824  if(s.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789~!@$%^&*_-+=<>.?/") != string::npos)
1825  return "|" + s + "|";
1826  }
1827  return s;
1828 }
1829 
1830 const string Translator::quoteAnnotation(const string& s)
1831 {
1832  if(s.find('|') == string::npos) {
1833  return "|" + s + "|";
1834  } else {
1835  stringstream sb;
1836  sb << '"';
1837  for(string::const_iterator i = s.begin(); i != s.end(); ++i) {
1838  char c = *i;
1839  if(c == '"')
1840  sb << "\\\"";
1841  else
1842  sb << *i;
1843  }
1844  sb << '"';
1845  return sb.str();
1846  }
1847 }
1848 
1849 
1851 {
1852  if (e.getKind() == ARRAY) {
1853  if (d_convertArray) {
1854  os << Expr(ARROW, e[0], e[1]);
1855  return true;
1856  }
1857  if (d_em->getOutputLang() == SMTLIB_V2_LANG) {
1858  DebugAssert( e.arity() == 2, "expected arity 2");
1859  os << push << "(Array" << space << nodag << e[0] << space << nodag << e[1] << ")" << pop;
1860  return true;
1861  }
1862  if (d_em->getOutputLang() != SMTLIB_LANG) return false;
1863  if (e[0].getKind() == TYPEDECL) {
1864  DebugAssert(e[0].arity() == 1, "expected arity 1");
1865  if (e[0][0].getString() == "Index") {
1866  if (e[1].getKind() == TYPEDECL) {
1867  DebugAssert(e[1].arity() == 1, "expected arity 1");
1868  if (e[1][0].getString() == "Element") {
1869  os << "Array";
1870  return true;
1871  }
1872  }
1873  }
1874  }
1875  else if (isInt(Type(e[0]))) {
1876  if (isInt(Type(e[1]))) {
1877  d_intIntArray = true;
1878  os << "Array";
1879  return true;
1880  }
1881  else if (isReal(Type(e[1]))) {
1882  d_intRealArray = true;
1883  os << "Array1";
1884  return true;
1885  }
1886  else if (isArray(Type(e[1])) &&
1887  isInt(Type(e[1][0])) &&
1888  isReal(Type(e[1][1]))) {
1889  d_intIntRealArray = true;
1890  os << "Array2";
1891  return true;
1892  }
1893  }
1894  else if (e[0].getKind() == BITVECTOR &&
1895  e[1].getKind() == BITVECTOR) {
1896  os << "Array[";
1898  os << ":";
1900  os << "]";
1901  return true;
1902  }
1903  os << "UnknownArray";
1904  d_unknown = true;
1905  return true;
1906  }
1907 
1908  switch (e.getKind()) {
1909  case READ:
1910  if (d_convertArray) {
1911  if (e[0].getKind() == UCONST) {
1912  os << Expr(d_em->newSymbolExpr(e[0].getName(), UFUNC).mkOp(), e[1]);
1913  return true;
1914  }
1915  else if (e[0].getKind() == WRITE) {
1916  throw Exception("READ of WRITE not implemented yet for convertArray");
1917  }
1918  else {
1919  throw Exception("Unexpected case for convertArray");
1920  }
1921  }
1922  break;
1923  case WRITE:
1924  if (d_convertArray) {
1925  throw Exception("WRITE expression encountered while attempting "
1926  "to convert arrays to uninterpreted functions");
1927  }
1928  break;
1929  case ARRAY_LITERAL:
1930  if (d_convertArray) {
1931  throw Exception("ARRAY_LITERAL expression encountered while attempting"
1932  " to convert arrays to uninterpreted functions");
1933  }
1934  break;
1935  default:
1936  throw Exception("Unexpected case in printArrayExpr");
1937  break;
1938  }
1939  return false;
1940 }
1941 
1942 
1944 {
1945  if (!d_zeroVar) {
1946  d_zeroVar = new Expr();
1947  if (d_convertToDiff == "int") {
1948  *d_zeroVar = d_theoryCore->newVar("cvc3Zero", d_theoryArith->intType().getExpr());
1949  }
1950  else if (d_convertToDiff == "real") {
1952  }
1953  }
1954  return *d_zeroVar;
1955 }
const std::string & d_expResult
Definition: translator.h:67
Definition: kinds.h:48
int arity() const
Definition: expr.h:1201
ExprStream & pop(ExprStream &os)
Restore the indentation.
for output in SPASS format
Definition: lang.h:49
iterator begin() const
Begin iterator.
Definition: expr.h:1211
virtual void setUsed()
Set the "used" flag on this theory (for smtlib translator)
Definition: theory.h:102
ExprStream & nodag(ExprStream &os)
const std::string fixConstName(const std::string &s)
bool isInt(Type t)
Definition: theory_arith.h:174
Data structure of expressions in CVC3.
Definition: expr.h:133
bool printArrayExpr(ExprStream &os, const Expr &e)
Returns true if expression has been printed.
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
Definition: expr.h:961
std::vector< Expr > d_equalities
Definition: translator.h:115
void dump(const Expr &e, bool dumpOnly=false)
Definition: translator.cpp:939
TheoryUF * d_theoryUF
Definition: translator.h:100
Expr processType(const Expr &e)
Type * d_arrayType
Definition: translator.h:114
QueryResult
Definition: queryresult.h:32
const CLFlags & getFlags() const
Definition: theory_core.h:350
bool isRational() const
Definition: expr.h:431
Rational getNumerator() const
void dumpQueryResult(QueryResult qres)
Definition: translator.cpp:986
std::ofstream d_osdumpFile
Definition: translator.h:84
bool containsArray(const Expr &e)
Definition: translator.cpp:799
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
Definition: expr.h:1135
iterator find(const Expr &e)
Definition: expr_map.h:194
Expr newSymbolExpr(const std::string &s, int kind)
Definition: expr_manager.h:481
bool start(const std::string &dumpFile)
Definition: translator.cpp:845
Type arrayType(const Type &type1, const Type &type2)
Definition: theory_array.h:116
TheoryDatatype * d_theoryDatatype
Definition: translator.h:107
MS C++ specific settings.
Definition: type.h:42
bool isPropAtom() const
True iff expr is not a Bool connective.
Definition: expr.h:411
SMT-LIB v2 format.
Definition: lang.h:52
STL namespace.
bool containsTermITE() const
Return whether Expr contains a non-bool type ITE as a sub-term.
Definition: expr.cpp:525
Definition: kinds.h:66
const bool & d_translate
Definition: translator.h:62
TheoryArray * d_theoryArray
Definition: translator.h:102
ExprStream & space(ExprStream &os)
Insert a single white space separator.
Definition: kinds.h:240
Definition: kinds.h:51
#define DebugAssert(cond, str)
Definition: debug.h:408
Definition: kinds.h:56
const std::vector< Expr > & getKids() const
Definition: expr.h:1162
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
bool isRational(const Expr &e)
Definition: theory_arith.h:177
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Definition: expr.h:1191
Op getOp() const
Get operator from expression.
Definition: expr.h:1183
const Expr & getExpr() const
Definition: type.h:52
Expr * d_zeroVar
Definition: translator.h:96
bool isClosure() const
Definition: expr.h:1007
Implementation of a symbolic simulator.
Definition: kinds.h:242
int getBitvectorTypeParam(const Expr &e)
Expr newStringExpr(const std::string &s)
Definition: expr_manager.h:468
Definition: kinds.h:44
bool d_combineAssump
Definition: translator.h:70
Identifier is (ID (STRING_EXPR "name"))
Definition: kinds.h:46
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
std::string fileToSMTLIBIdentifier(const std::string &filename)
Definition: translator.cpp:45
bool isInteger() const
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
Expr newVar(const std::string &name, const Type &type)
Create a new variable given its name and type.
Definition: theory.cpp:569
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Definition: expr.h:1196
std::map< std::string, Type > * d_arrayConvertMap
Definition: translator.h:111
bool dumpAssertion(const Expr &e)
Definition: translator.cpp:970
Expr negate() const
Definition: expr.h:937
Definition: kinds.h:88
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
const Expr & getBody() const
Get the body of the closure Expr.
Definition: expr.h:1069
const Expr & getRHS() const
Definition: theorem.cpp:246
bool isNull() const
Definition: type.h:59
Type newTypeExpr(const std::string &name)
Create a new uninterpreted type with the given name.
Definition: theory.cpp:790
TheoryArith * d_theoryArith
Definition: translator.h:101
size_t size_type
Definition: hash_table.h:75
Expression Manager.
Definition: expr_manager.h:58
const std::string quoteAnnotation(const std::string &s)
bool isApply() const
Definition: expr.h:1014
bool isArray(const Type &t)
Definition: theory_array.h:109
Definition: kinds.h:90
TheoryRecords * d_theoryRecords
Definition: translator.h:104
const std::string & getName() const
Definition: expr.h:1050
Definition: kinds.h:94
virtual bool theoryUsed()
Get whether theory has been used (for smtlib translator)
Definition: theory.h:104
std::vector< Expr > d_dumpExprs
Definition: translator.h:109
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
Definition: theory.cpp:383
std::string status()
Definition: translator.h:179
TheoryQuant * d_theoryQuant
Definition: translator.h:103
bool isVar() const
Definition: expr.h:1005
An exception to be thrown by the smtlib translator.
An exception to be thrown by the smtlib translator.
Expr preprocess(const Expr &e, ExprMap< Expr > &cache)
Definition: translator.cpp:549
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Definition: expr.h:1062
Expr preprocess2(const Expr &e, ExprMap< Expr > &cache)
Definition: translator.cpp:783
SMT-LIB format.
Definition: lang.h:34
ExprManager * d_em
Definition: translator.h:61
Definition of the API to expression package. See class Expr for details.
const std::string escapeSymbol(const std::string &s)
std::ifstream d_tmpFile
Definition: translator.h:85
Definition: kinds.h:93
TheorySimulate * d_theorySimulate
Definition: translator.h:105
Definition: kinds.h:53
std::string category()
Definition: translator.h:183
Definition: kinds.h:81
Type * d_elementType
Definition: translator.h:113
const std::string & d_convertToDiff
Definition: translator.h:65
Definition: kinds.h:61
std::string source()
Definition: translator.h:181
bool dumpQuery(const Expr &e)
Definition: translator.cpp:978
bool isReal(Type t)
Definition: theory_arith.h:173
const std::string & getString() const
Definition: expr.h:1055
Definition: kinds.h:50
Rational pow(Rational pow, const Rational &base)
Raise 'base' into the power of 'pow' (pow must be an integer)
Definition: rational.h:159
Definition: expr.cpp:35
Definition: kinds.h:99
ArithLang d_langUsed
Definition: translator.h:92
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Definition: theory.cpp:252
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
bool d_intIntRealArray
Definition: translator.h:88
TheoryCore * d_theoryCore
Definition: translator.h:99
Definition: kinds.h:229
Type * d_indexType
Definition: translator.h:112
iterator end()
Definition: expr_map.h:191
Definition: kinds.h:67
std::hash_map< std::string, std::string, HashString > d_replaceSymbols
Definition: translator.h:80
std::ostream * d_osdump
The log file for top-level API calls in the CVC3 input language.
Definition: translator.h:83
const bool & d_real2int
Definition: translator.h:63
Nice SAL-like language for manually written specs.
Definition: lang.h:32
TheoryBitvector * d_theoryBitvector
Definition: translator.h:106
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
InputLanguage getOutputLang() const
Get the output language for printing.
iterator end() const
End iterator.
Definition: expr.h:1217