src/parser/smt2/smt2.cpp

   1 /*********************                                                        */
   2 /*! \file smt2.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Kshitij Bansal, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Definitions of SMT2 constants.
  13  **
  14  ** Definitions of SMT2 constants.
  15  **/
  16 #include "parser/smt2/smt2.h"
  17
  18 #include "expr/type.h"
  19 #include "options/options.h"
  20 #include "parser/antlr_input.h"
  21 #include "parser/parser.h"
  22 #include "parser/smt1/smt1.h"
  23 #include "parser/smt2/smt2_input.h"
  24 #include "printer/sygus_print_callback.h"
  25 #include "util/bitvector.h"
  26
  27 #include <algorithm>
  28
  29 // ANTLR defines these, which is really bad!
  30 #undef true
  31 #undef false
  32
  33 namespace CVC4 {
  34 namespace parser {
  35
  36 Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
  37     : Parser(solver, input, strictMode, parseOnly),
  38       d_logicSet(false),
  39       d_seenSetLogic(false)
  40 {
  41   if (!strictModeEnabled())
  42   {
  43     addTheory(Smt2::THEORY_CORE);
  44   }
  45 }
  46
  47 void Smt2::addArithmeticOperators() {
  48   addOperator(kind::PLUS, "+");
  49   addOperator(kind::MINUS, "-");
  50   // kind::MINUS is converted to kind::UMINUS if there is only a single operand
  51   Parser::addOperator(kind::UMINUS);
  52   addOperator(kind::MULT, "*");
  53   addOperator(kind::LT, "<");
  54   addOperator(kind::LEQ, "<=");
  55   addOperator(kind::GT, ">");
  56   addOperator(kind::GEQ, ">=");
  57
  58   if (!strictModeEnabled())
  59   {
  60     // NOTE: this operator is non-standard
  61     addOperator(kind::POW, "^");
  62   }
  63 }
  64
  65 void Smt2::addTranscendentalOperators()
  66 {
  67   addOperator(kind::EXPONENTIAL, "exp");
  68   addOperator(kind::SINE, "sin");
  69   addOperator(kind::COSINE, "cos");
  70   addOperator(kind::TANGENT, "tan");
  71   addOperator(kind::COSECANT, "csc");
  72   addOperator(kind::SECANT, "sec");
  73   addOperator(kind::COTANGENT, "cot");
  74   addOperator(kind::ARCSINE, "arcsin");
  75   addOperator(kind::ARCCOSINE, "arccos");
  76   addOperator(kind::ARCTANGENT, "arctan");
  77   addOperator(kind::ARCCOSECANT, "arccsc");
  78   addOperator(kind::ARCSECANT, "arcsec");
  79   addOperator(kind::ARCCOTANGENT, "arccot");
  80   addOperator(kind::SQRT, "sqrt");
  81 }
  82
  83 void Smt2::addQuantifiersOperators()
  84 {
  85   if (!strictModeEnabled())
  86   {
  87     addOperator(kind::INST_CLOSURE, "inst-closure");
  88   }
  89 }
  90
  91 void Smt2::addBitvectorOperators() {
  92   addOperator(kind::BITVECTOR_CONCAT, "concat");
  93   addOperator(kind::BITVECTOR_NOT, "bvnot");
  94   addOperator(kind::BITVECTOR_AND, "bvand");
  95   addOperator(kind::BITVECTOR_OR, "bvor");
  96   addOperator(kind::BITVECTOR_NEG, "bvneg");
  97   addOperator(kind::BITVECTOR_PLUS, "bvadd");
  98   addOperator(kind::BITVECTOR_MULT, "bvmul");
  99   addOperator(kind::BITVECTOR_UDIV, "bvudiv");
 100   addOperator(kind::BITVECTOR_UREM, "bvurem");
 101   addOperator(kind::BITVECTOR_SHL, "bvshl");
 102   addOperator(kind::BITVECTOR_LSHR, "bvlshr");
 103   addOperator(kind::BITVECTOR_ULT, "bvult");
 104   addOperator(kind::BITVECTOR_NAND, "bvnand");
 105   addOperator(kind::BITVECTOR_NOR, "bvnor");
 106   addOperator(kind::BITVECTOR_XOR, "bvxor");
 107   addOperator(kind::BITVECTOR_XNOR, "bvxnor");
 108   addOperator(kind::BITVECTOR_COMP, "bvcomp");
 109   addOperator(kind::BITVECTOR_SUB, "bvsub");
 110   addOperator(kind::BITVECTOR_SDIV, "bvsdiv");
 111   addOperator(kind::BITVECTOR_SREM, "bvsrem");
 112   addOperator(kind::BITVECTOR_SMOD, "bvsmod");
 113   addOperator(kind::BITVECTOR_ASHR, "bvashr");
 114   addOperator(kind::BITVECTOR_ULE, "bvule");
 115   addOperator(kind::BITVECTOR_UGT, "bvugt");
 116   addOperator(kind::BITVECTOR_UGE, "bvuge");
 117   addOperator(kind::BITVECTOR_SLT, "bvslt");
 118   addOperator(kind::BITVECTOR_SLE, "bvsle");
 119   addOperator(kind::BITVECTOR_SGT, "bvsgt");
 120   addOperator(kind::BITVECTOR_SGE, "bvsge");
 121   addOperator(kind::BITVECTOR_REDOR, "bvredor");
 122   addOperator(kind::BITVECTOR_REDAND, "bvredand");
 123   addOperator(kind::BITVECTOR_TO_NAT, "bv2nat");
 124
 125   addIndexedOperator(
 126       kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT_OP, "extract");
 127   addIndexedOperator(
 128       kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT_OP, "repeat");
 129   addIndexedOperator(kind::BITVECTOR_ZERO_EXTEND,
 130                      api::BITVECTOR_ZERO_EXTEND_OP,
 131                      "zero_extend");
 132   addIndexedOperator(kind::BITVECTOR_SIGN_EXTEND,
 133                      api::BITVECTOR_SIGN_EXTEND_OP,
 134                      "sign_extend");
 135   addIndexedOperator(kind::BITVECTOR_ROTATE_LEFT,
 136                      api::BITVECTOR_ROTATE_LEFT_OP,
 137                      "rotate_left");
 138   addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT,
 139                      api::BITVECTOR_ROTATE_RIGHT_OP,
 140                      "rotate_right");
 141   addIndexedOperator(
 142       kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR_OP, "int2bv");
 143 }
 144
 145 void Smt2::addDatatypesOperators()
 146 {
 147   Parser::addOperator(kind::APPLY_CONSTRUCTOR);
 148   Parser::addOperator(kind::APPLY_TESTER);
 149   Parser::addOperator(kind::APPLY_SELECTOR);
 150   Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
 151
 152   if (!strictModeEnabled())
 153   {
 154     addOperator(kind::DT_SIZE, "dt.size");
 155   }
 156 }
 157
 158 void Smt2::addStringOperators() {
 159   defineVar("re.all",
 160             getSolver()
 161                 ->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())
 162                 .getExpr());
 163
 164   addOperator(kind::STRING_CONCAT, "str.++");
 165   addOperator(kind::STRING_LENGTH, "str.len");
 166   addOperator(kind::STRING_SUBSTR, "str.substr" );
 167   addOperator(kind::STRING_STRCTN, "str.contains" );
 168   addOperator(kind::STRING_CHARAT, "str.at" );
 169   addOperator(kind::STRING_STRIDOF, "str.indexof" );
 170   addOperator(kind::STRING_STRREPL, "str.replace" );
 171   addOperator(kind::STRING_STRREPLALL, "str.replaceall");
 172   if (!strictModeEnabled())
 173   {
 174     addOperator(kind::STRING_TOLOWER, "str.tolower");
 175     addOperator(kind::STRING_TOUPPER, "str.toupper");
 176   }
 177   addOperator(kind::STRING_PREFIX, "str.prefixof" );
 178   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
 179   // at the moment, we only use this syntax for smt2.6.1
 180   if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
 181   {
 182     addOperator(kind::STRING_ITOS, "str.from-int");
 183     addOperator(kind::STRING_STOI, "str.to-int");
 184     addOperator(kind::STRING_IN_REGEXP, "str.in-re");
 185     addOperator(kind::STRING_TO_REGEXP, "str.to-re");
 186   }
 187   else
 188   {
 189     addOperator(kind::STRING_ITOS, "int.to.str");
 190     addOperator(kind::STRING_STOI, "str.to.int");
 191     addOperator(kind::STRING_IN_REGEXP, "str.in.re");
 192     addOperator(kind::STRING_TO_REGEXP, "str.to.re");
 193   }
 194
 195   addOperator(kind::REGEXP_CONCAT, "re.++");
 196   addOperator(kind::REGEXP_UNION, "re.union");
 197   addOperator(kind::REGEXP_INTER, "re.inter");
 198   addOperator(kind::REGEXP_STAR, "re.*");
 199   addOperator(kind::REGEXP_PLUS, "re.+");
 200   addOperator(kind::REGEXP_OPT, "re.opt");
 201   addOperator(kind::REGEXP_RANGE, "re.range");
 202   addOperator(kind::REGEXP_LOOP, "re.loop");
 203   addOperator(kind::STRING_CODE, "str.code");
 204   addOperator(kind::STRING_LT, "str.<");
 205   addOperator(kind::STRING_LEQ, "str.<=");
 206 }
 207
 208 void Smt2::addFloatingPointOperators() {
 209   addOperator(kind::FLOATINGPOINT_FP, "fp");
 210   addOperator(kind::FLOATINGPOINT_EQ, "fp.eq");
 211   addOperator(kind::FLOATINGPOINT_ABS, "fp.abs");
 212   addOperator(kind::FLOATINGPOINT_NEG, "fp.neg");
 213   addOperator(kind::FLOATINGPOINT_PLUS, "fp.add");
 214   addOperator(kind::FLOATINGPOINT_SUB, "fp.sub");
 215   addOperator(kind::FLOATINGPOINT_MULT, "fp.mul");
 216   addOperator(kind::FLOATINGPOINT_DIV, "fp.div");
 217   addOperator(kind::FLOATINGPOINT_FMA, "fp.fma");
 218   addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt");
 219   addOperator(kind::FLOATINGPOINT_REM, "fp.rem");
 220   addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral");
 221   addOperator(kind::FLOATINGPOINT_MIN, "fp.min");
 222   addOperator(kind::FLOATINGPOINT_MAX, "fp.max");
 223   addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq");
 224   addOperator(kind::FLOATINGPOINT_LT, "fp.lt");
 225   addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq");
 226   addOperator(kind::FLOATINGPOINT_GT, "fp.gt");
 227   addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal");
 228   addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal");
 229   addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero");
 230   addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite");
 231   addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN");
 232   addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative");
 233   addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
 234   addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
 235
 236   addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC,
 237                      api::FLOATINGPOINT_TO_FP_GENERIC_OP,
 238                      "to_fp");
 239   addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
 240                      api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
 241                      "to_fp_unsigned");
 242   addIndexedOperator(
 243       kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV_OP, "fp.to_ubv");
 244   addIndexedOperator(
 245       kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV_OP, "fp.to_sbv");
 246
 247   if (!strictModeEnabled())
 248   {
 249     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
 250                        api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
 251                        "to_fp_bv");
 252     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
 253                        api::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
 254                        "to_fp_fp");
 255     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL,
 256                        api::FLOATINGPOINT_TO_FP_REAL_OP,
 257                        "to_fp_real");
 258     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
 259                        api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
 260                        "to_fp_signed");
 261   }
 262 }
 263
 264 void Smt2::addSepOperators() {
 265   addOperator(kind::SEP_STAR, "sep");
 266   addOperator(kind::SEP_PTO, "pto");
 267   addOperator(kind::SEP_WAND, "wand");
 268   addOperator(kind::SEP_EMP, "emp");
 269   Parser::addOperator(kind::SEP_STAR);
 270   Parser::addOperator(kind::SEP_PTO);
 271   Parser::addOperator(kind::SEP_WAND);
 272   Parser::addOperator(kind::SEP_EMP);
 273 }
 274
 275 void Smt2::addTheory(Theory theory) {
 276   switch(theory) {
 277   case THEORY_ARRAYS:
 278     addOperator(kind::SELECT, "select");
 279     addOperator(kind::STORE, "store");
 280     break;
 281
 282   case THEORY_BITVECTORS:
 283     addBitvectorOperators();
 284     break;
 285
 286   case THEORY_CORE:
 287     defineType("Bool", getExprManager()->booleanType());
 288     defineVar("true", getExprManager()->mkConst(true));
 289     defineVar("false", getExprManager()->mkConst(false));
 290     addOperator(kind::AND, "and");
 291     addOperator(kind::DISTINCT, "distinct");
 292     addOperator(kind::EQUAL, "=");
 293     addOperator(kind::IMPLIES, "=>");
 294     addOperator(kind::ITE, "ite");
 295     addOperator(kind::NOT, "not");
 296     addOperator(kind::OR, "or");
 297     addOperator(kind::XOR, "xor");
 298     break;
 299
 300   case THEORY_REALS_INTS:
 301     defineType("Real", getExprManager()->realType());
 302     addOperator(kind::DIVISION, "/");
 303     addOperator(kind::TO_INTEGER, "to_int");
 304     addOperator(kind::IS_INTEGER, "is_int");
 305     addOperator(kind::TO_REAL, "to_real");
 306     // falling through on purpose, to add Ints part of Reals_Ints
 307   case THEORY_INTS:
 308     defineType("Int", getExprManager()->integerType());
 309     addArithmeticOperators();
 310     addOperator(kind::INTS_DIVISION, "div");
 311     addOperator(kind::INTS_MODULUS, "mod");
 312     addOperator(kind::ABS, "abs");
 313     addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE_OP, "divisible");
 314     break;
 315
 316   case THEORY_REALS:
 317     defineType("Real", getExprManager()->realType());
 318     addArithmeticOperators();
 319     addOperator(kind::DIVISION, "/");
 320     if (!strictModeEnabled())
 321     {
 322       addOperator(kind::ABS, "abs");
 323     }
 324     break;
 325
 326   case THEORY_TRANSCENDENTALS:
 327     defineVar("real.pi",
 328               getExprManager()->mkNullaryOperator(getExprManager()->realType(),
 329                                                   CVC4::kind::PI));
 330     addTranscendentalOperators();
 331     break;
 332
 333   case THEORY_QUANTIFIERS: addQuantifiersOperators(); break;
 334
 335   case THEORY_SETS:
 336     defineVar("emptyset",
 337               d_solver->mkEmptySet(d_solver->getNullSort()).getExpr());
 338     // the Boolean sort is a placeholder here since we don't have type info
 339     // without type annotation
 340     defineVar("univset",
 341               d_solver->mkUniverseSet(d_solver->getBooleanSort()).getExpr());
 342
 343     addOperator(kind::UNION, "union");
 344     addOperator(kind::INTERSECTION, "intersection");
 345     addOperator(kind::SETMINUS, "setminus");
 346     addOperator(kind::SUBSET, "subset");
 347     addOperator(kind::MEMBER, "member");
 348     addOperator(kind::SINGLETON, "singleton");
 349     addOperator(kind::INSERT, "insert");
 350     addOperator(kind::CARD, "card");
 351     addOperator(kind::COMPLEMENT, "complement");
 352     addOperator(kind::JOIN, "join");
 353     addOperator(kind::PRODUCT, "product");
 354     addOperator(kind::TRANSPOSE, "transpose");
 355     addOperator(kind::TCLOSURE, "tclosure");
 356     break;
 357
 358   case THEORY_DATATYPES:
 359   {
 360     const std::vector<Type> types;
 361     defineType("Tuple", getExprManager()->mkTupleType(types));
 362     addDatatypesOperators();
 363     break;
 364   }
 365
 366   case THEORY_STRINGS:
 367     defineType("String", getExprManager()->stringType());
 368     defineType("RegLan", getExprManager()->regExpType());
 369     defineType("Int", getExprManager()->integerType());
 370
 371     defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr());
 372     defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr());
 373
 374     addStringOperators();
 375     break;
 376
 377   case THEORY_UF:
 378     Parser::addOperator(kind::APPLY_UF);
 379
 380     if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
 381     {
 382       addOperator(kind::CARDINALITY_CONSTRAINT, "fmf.card");
 383       addOperator(kind::CARDINALITY_VALUE, "fmf.card.val");
 384     }
 385     break;
 386
 387   case THEORY_FP:
 388     defineType("RoundingMode", getExprManager()->roundingModeType());
 389     defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
 390     defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
 391     defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
 392     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
 393
 394     defineVar(
 395         "RNE",
 396         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
 397     defineVar(
 398         "roundNearestTiesToEven",
 399         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
 400     defineVar(
 401         "RNA",
 402         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
 403     defineVar(
 404         "roundNearestTiesToAway",
 405         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
 406     defineVar("RTP",
 407               d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
 408     defineVar("roundTowardPositive",
 409               d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
 410     defineVar("RTN",
 411               d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
 412     defineVar("roundTowardNegative",
 413               d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
 414     defineVar("RTZ",
 415               d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
 416     defineVar("roundTowardZero",
 417               d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
 418
 419     addFloatingPointOperators();
 420     break;
 421
 422   case THEORY_SEP:
 423     // the Boolean sort is a placeholder here since we don't have type info
 424     // without type annotation
 425     defineVar("sep.nil",
 426               d_solver->mkSepNil(d_solver->getBooleanSort()).getExpr());
 427
 428     addSepOperators();
 429     break;
 430
 431   default:
 432     std::stringstream ss;
 433     ss << "internal error: unsupported theory " << theory;
 434     throw ParserException(ss.str());
 435   }
 436 }
 437
 438 void Smt2::addOperator(Kind kind, const std::string& name) {
 439   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 440                   << std::endl;
 441   Parser::addOperator(kind);
 442   operatorKindMap[name] = kind;
 443 }
 444
 445 void Smt2::addIndexedOperator(Kind tKind,
 446                               api::Kind opKind,
 447                               const std::string& name)
 448 {
 449   Parser::addOperator(tKind);
 450   d_indexedOpKindMap[name] = opKind;
 451 }
 452
 453 Kind Smt2::getOperatorKind(const std::string& name) const {
 454   // precondition: isOperatorEnabled(name)
 455   return operatorKindMap.find(name)->second;
 456 }
 457
 458 bool Smt2::isOperatorEnabled(const std::string& name) const {
 459   return operatorKindMap.find(name) != operatorKindMap.end();
 460 }
 461
 462 bool Smt2::isTheoryEnabled(Theory theory) const {
 463   switch(theory) {
 464   case THEORY_ARRAYS:
 465     return d_logic.isTheoryEnabled(theory::THEORY_ARRAYS);
 466   case THEORY_BITVECTORS:
 467     return d_logic.isTheoryEnabled(theory::THEORY_BV);
 468   case THEORY_CORE:
 469     return true;
 470   case THEORY_DATATYPES:
 471     return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
 472   case THEORY_INTS:
 473     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 474       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
 475   case THEORY_REALS:
 476     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 477       ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
 478   case THEORY_REALS_INTS:
 479     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 480       d_logic.areIntegersUsed() && d_logic.areRealsUsed();
 481   case THEORY_QUANTIFIERS:
 482     return d_logic.isQuantified();
 483   case THEORY_SETS:
 484     return d_logic.isTheoryEnabled(theory::THEORY_SETS);
 485   case THEORY_STRINGS:
 486     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
 487   case THEORY_UF:
 488     return d_logic.isTheoryEnabled(theory::THEORY_UF);
 489   case THEORY_FP:
 490     return d_logic.isTheoryEnabled(theory::THEORY_FP);
 491   case THEORY_SEP:
 492     return d_logic.isTheoryEnabled(theory::THEORY_SEP);
 493   default:
 494     std::stringstream ss;
 495     ss << "internal error: unsupported theory " << theory;
 496     throw ParserException(ss.str());
 497   }
 498 }
 499
 500 bool Smt2::logicIsSet() {
 501   return d_logicSet;
 502 }
 503
 504 Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
 505   if (sygus_v1() && name[0] == '-'
 506       && name.find_first_not_of("0123456789", 1) == std::string::npos)
 507   {
 508     // allow unary minus in sygus version 1
 509     return getExprManager()->mkConst(Rational(name));
 510   }
 511   else if (isAbstractValue(name))
 512   {
 513     return mkAbstractValue(name);
 514   }
 515   return Parser::getExpressionForNameAndType(name, t);
 516 }
 517
 518 api::Term Smt2::mkIndexedConstant(const std::string& name,
 519                                   const std::vector<uint64_t>& numerals)
 520 {
 521   if (isTheoryEnabled(THEORY_FP))
 522   {
 523     if (name == "+oo")
 524     {
 525       return d_solver->mkPosInf(numerals[0], numerals[1]);
 526     }
 527     else if (name == "-oo")
 528     {
 529       return d_solver->mkNegInf(numerals[0], numerals[1]);
 530     }
 531     else if (name == "NaN")
 532     {
 533       return d_solver->mkNaN(numerals[0], numerals[1]);
 534     }
 535     else if (name == "+zero")
 536     {
 537       return d_solver->mkPosZero(numerals[0], numerals[1]);
 538     }
 539     else if (name == "-zero")
 540     {
 541       return d_solver->mkNegZero(numerals[0], numerals[1]);
 542     }
 543   }
 544
 545   if (isTheoryEnabled(THEORY_BITVECTORS) && name.find("bv") == 0)
 546   {
 547     std::string bvStr = name.substr(2);
 548     return d_solver->mkBitVector(numerals[0], bvStr, 10);
 549   }
 550
 551   // NOTE: Theory parametric constants go here
 552
 553   parseError(std::string("Unknown indexed literal `") + name + "'");
 554   return api::Term();
 555 }
 556
 557 api::OpTerm Smt2::mkIndexedOp(const std::string& name,
 558                               const std::vector<uint64_t>& numerals)
 559 {
 560   const auto& kIt = d_indexedOpKindMap.find(name);
 561   if (kIt != d_indexedOpKindMap.end())
 562   {
 563     api::Kind k = (*kIt).second;
 564     if (numerals.size() == 1)
 565     {
 566       return d_solver->mkOpTerm(k, numerals[0]);
 567     }
 568     else if (numerals.size() == 2)
 569     {
 570       return d_solver->mkOpTerm(k, numerals[0], numerals[1]);
 571     }
 572   }
 573
 574   parseError(std::string("Unknown indexed function `") + name + "'");
 575   return api::OpTerm();
 576 }
 577
 578 Expr Smt2::mkDefineFunRec(
 579     const std::string& fname,
 580     const std::vector<std::pair<std::string, Type> >& sortedVarNames,
 581     Type t,
 582     std::vector<Expr>& flattenVars)
 583 {
 584   std::vector<Type> sorts;
 585   for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
 586   {
 587     sorts.push_back(svn.second);
 588   }
 589
 590   // make the flattened function type, add bound variables
 591   // to flattenVars if the defined function was given a function return type.
 592   Type ft = mkFlatFunctionType(sorts, t, flattenVars);
 593
 594   // allow overloading
 595   return mkVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
 596 }
 597
 598 void Smt2::pushDefineFunRecScope(
 599     const std::vector<std::pair<std::string, Type> >& sortedVarNames,
 600     Expr func,
 601     const std::vector<Expr>& flattenVars,
 602     std::vector<Expr>& bvs,
 603     bool bindingLevel)
 604 {
 605   pushScope(bindingLevel);
 606
 607   // bound variables are those that are explicitly named in the preamble
 608   // of the define-fun(s)-rec command, we define them here
 609   for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
 610   {
 611     Expr v = mkBoundVar(svn.first, svn.second);
 612     bvs.push_back(v);
 613   }
 614
 615   bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end());
 616 }
 617
 618 void Smt2::reset() {
 619   d_logicSet = false;
 620   d_logic = LogicInfo();
 621   operatorKindMap.clear();
 622   d_lastNamedTerm = std::pair<Expr, std::string>();
 623   this->Parser::reset();
 624
 625   if( !strictModeEnabled() ) {
 626     addTheory(Smt2::THEORY_CORE);
 627   }
 628 }
 629
 630 void Smt2::resetAssertions() {
 631   // Remove all declarations except the ones at level 0.
 632   while (this->scopeLevel() > 0) {
 633     this->popScope();
 634   }
 635 }
 636
 637 Command* Smt2::setLogic(std::string name, bool fromCommand)
 638 {
 639   if (fromCommand)
 640   {
 641     if (d_seenSetLogic)
 642     {
 643       parseError("Only one set-logic is allowed.");
 644     }
 645     d_seenSetLogic = true;
 646
 647     if (logicIsForced())
 648     {
 649       // If the logic is forced, we ignore all set-logic requests from commands.
 650       return new EmptyCommand();
 651     }
 652   }
 653
 654   if (sygus_v1())
 655   {
 656     // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2)
 657     if(name == "Arrays") {
 658       name = "A";
 659     }else if(name == "Reals") {
 660       name = "LRA";
 661     }
 662   }
 663
 664   d_logicSet = true;
 665   d_logic = name;
 666
 667   // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
 668   // higher-order
 669   if(sygus()) {
 670     if (!d_logic.isQuantified())
 671     {
 672       warning("Logics in sygus are assumed to contain quantifiers.");
 673       warning("Omit QF_ from the logic to avoid this warning.");
 674     }
 675     // get unlocked copy, modify, copy and relock
 676     LogicInfo log(d_logic.getUnlockedCopy());
 677     // enable everything needed for sygus
 678     log.enableSygus();
 679     d_logic = log;
 680     d_logic.lock();
 681   }
 682
 683   // Core theory belongs to every logic
 684   addTheory(THEORY_CORE);
 685
 686   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 687     addTheory(THEORY_UF);
 688   }
 689
 690   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 691     if(d_logic.areIntegersUsed()) {
 692       if(d_logic.areRealsUsed()) {
 693         addTheory(THEORY_REALS_INTS);
 694       } else {
 695         addTheory(THEORY_INTS);
 696       }
 697     } else if(d_logic.areRealsUsed()) {
 698       addTheory(THEORY_REALS);
 699     }
 700
 701     if (d_logic.areTranscendentalsUsed())
 702     {
 703       addTheory(THEORY_TRANSCENDENTALS);
 704     }
 705   }
 706
 707   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
 708     addTheory(THEORY_ARRAYS);
 709   }
 710
 711   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 712     addTheory(THEORY_BITVECTORS);
 713   }
 714
 715   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
 716     addTheory(THEORY_DATATYPES);
 717   }
 718
 719   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 720     addTheory(THEORY_SETS);
 721   }
 722
 723   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 724     addTheory(THEORY_STRINGS);
 725   }
 726
 727   if(d_logic.isQuantified()) {
 728     addTheory(THEORY_QUANTIFIERS);
 729   }
 730
 731   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
 732     addTheory(THEORY_FP);
 733   }
 734
 735   if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
 736     addTheory(THEORY_SEP);
 737   }
 738
 739   if (sygus())
 740   {
 741     return new SetBenchmarkLogicCommand(d_logic.getLogicString());
 742   }
 743   else
 744   {
 745     return new SetBenchmarkLogicCommand(name);
 746   }
 747 } /* Smt2::setLogic() */
 748
 749 bool Smt2::sygus() const
 750 {
 751   InputLanguage ilang = getLanguage();
 752   return ilang == language::input::LANG_SYGUS
 753          || ilang == language::input::LANG_SYGUS_V2;
 754 }
 755 bool Smt2::sygus_v1() const
 756 {
 757   return getLanguage() == language::input::LANG_SYGUS;
 758 }
 759
 760 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 761   // TODO: ???
 762 }
 763
 764 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 765   // TODO: ???
 766 }
 767
 768 void Smt2::checkThatLogicIsSet()
 769 {
 770   if (!logicIsSet())
 771   {
 772     if (strictModeEnabled())
 773     {
 774       parseError("set-logic must appear before this point.");
 775     }
 776     else
 777     {
 778       Command* cmd = nullptr;
 779       if (logicIsForced())
 780       {
 781         cmd = setLogic(getForcedLogic(), false);
 782       }
 783       else
 784       {
 785         warning("No set-logic command was given before this point.");
 786         warning("CVC4 will make all theories available.");
 787         warning(
 788             "Consider setting a stricter logic for (likely) better "
 789             "performance.");
 790         warning("To suppress this warning in the future use (set-logic ALL).");
 791
 792         cmd = setLogic("ALL", false);
 793       }
 794       preemptCommand(cmd);
 795     }
 796   }
 797 }
 798
 799 /* The include are managed in the lexer but called in the parser */
 800 // Inspired by http://www.antlr3.org/api/C/interop.html
 801
 802 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 803   Debug("parser") << "Including " << filename << std::endl;
 804   // Create a new input stream and take advantage of built in stream stacking
 805   // in C target runtime.
 806   //
 807   pANTLR3_INPUT_STREAM    in;
 808 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 809   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 810 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 811   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 812 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 813   if( in == NULL ) {
 814     Debug("parser") << "Can't open " << filename << std::endl;
 815     return false;
 816   }
 817   // Same thing as the predefined PUSHSTREAM(in);
 818   lexer->pushCharStream(lexer, in);
 819   // restart it
 820   //lexer->rec->state->tokenStartCharIndex      = -10;
 821   //lexer->emit(lexer);
 822
 823   // Note that the input stream is not closed when it EOFs, I don't bother
 824   // to do it here, but it is up to you to track streams created like this
 825   // and destroy them when the whole parse session is complete. Remember that you
 826   // don't want to do this until all tokens have been manipulated all the way through
 827   // your tree parsers etc as the token does not store the text it just refers
 828   // back to the input stream and trying to get the text for it will abort if you
 829   // close the input stream too early.
 830
 831   //TODO what said before
 832   return true;
 833 }
 834
 835 void Smt2::includeFile(const std::string& filename) {
 836   // security for online version
 837   if(!canIncludeFile()) {
 838     parseError("include-file feature was disabled for this run.");
 839   }
 840
 841   // Get the lexer
 842   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 843   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 844   // get the name of the current stream "Does it work inside an include?"
 845   const std::string inputName = ai->getInputStreamName();
 846
 847   // Find the directory of the current input file
 848   std::string path;
 849   size_t pos = inputName.rfind('/');
 850   if(pos != std::string::npos) {
 851     path = std::string(inputName, 0, pos + 1);
 852   }
 853   path.append(filename);
 854   if(!newInputStream(path, lexer)) {
 855     parseError("Couldn't open include file `" + path + "'");
 856   }
 857 }
 858
 859 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
 860   if( type.isInteger() ){
 861     ops.push_back(getExprManager()->mkConst(Rational(0)));
 862     ops.push_back(getExprManager()->mkConst(Rational(1)));
 863   }else if( type.isBitVector() ){
 864     unsigned sz = ((BitVectorType)type).getSize();
 865     BitVector bval0(sz, (unsigned int)0);
 866     ops.push_back( getExprManager()->mkConst(bval0) );
 867     BitVector bval1(sz, (unsigned int)1);
 868     ops.push_back( getExprManager()->mkConst(bval1) );
 869   }else if( type.isBoolean() ){
 870     ops.push_back(getExprManager()->mkConst(true));
 871     ops.push_back(getExprManager()->mkConst(false));
 872   }
 873   //TODO : others?
 874 }
 875
 876 //  This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
 877 //  This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
 878 void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
 879                               std::vector< CVC4::Datatype >& datatypes,
 880                               std::vector< CVC4::Type>& sorts,
 881                               std::vector< std::vector<CVC4::Expr> >& ops,
 882                               std::vector< std::vector<std::string> >& cnames,
 883                               std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 884                               std::vector< bool >& allow_const,
 885                               std::vector< std::vector< std::string > >& unresolved_gterm_sym,
 886                               std::vector<CVC4::Expr>& sygus_vars,
 887                               std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
 888                               CVC4::Type& ret, bool isNested ){
 889   if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){
 890     Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index
 891                           << ", isLet = "
 892                           << (sgt.d_gterm_type == SygusGTerm::gterm_let)
 893                           << std::endl;
 894     Kind oldKind;
 895     Kind newKind = kind::UNDEFINED_KIND;
 896     //convert to UMINUS if one child of MINUS
 897     if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){
 898       oldKind = kind::MINUS;
 899       newKind = kind::UMINUS;
 900     }
 901     if( newKind!=kind::UNDEFINED_KIND ){
 902       Expr newExpr = getExprManager()->operatorOf(newKind);
 903       Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl;
 904       sgt.d_expr = newExpr;
 905       std::string oldName = kind::kindToString(oldKind);
 906       std::string newName = kind::kindToString(newKind);
 907       size_t pos = 0;
 908       if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){
 909         sgt.d_name.replace(pos, oldName.length(), newName);
 910       }
 911     }
 912     ops[index].push_back( sgt.d_expr );
 913     cnames[index].push_back( sgt.d_name );
 914     cargs[index].push_back( std::vector< CVC4::Type >() );
 915     for( unsigned i=0; i<sgt.d_children.size(); i++ ){
 916       std::stringstream ss;
 917       ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
 918       std::string sub_dname = ss.str();
 919       //add datatype for child
 920       Type null_type;
 921       pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
 922       int sub_dt_index = datatypes.size()-1;
 923       //process child
 924       Type sub_ret;
 925       processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
 926                          sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
 927       //process the nested gterm (either pop the last datatype, or flatten the argument)
 928       Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
 929                                          sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
 930       cargs[index].back().push_back(tt);
 931     }
 932     //if let, must create operator
 933     if( sgt.d_gterm_type==SygusGTerm::gterm_let ){
 934       processSygusLetConstructor( sgt.d_let_vars, index, datatypes, sorts, ops, cnames, cargs,
 935                                   sygus_vars, sygus_to_builtin, sygus_to_builtin_expr );
 936     }
 937   }else if( sgt.d_gterm_type==SygusGTerm::gterm_constant ){
 938     if( sgt.getNumChildren()!=0 ){
 939       parseError("Bad syntax for Sygus Constant.");
 940     }
 941     std::vector< Expr > consts;
 942     mkSygusConstantsForType( sgt.d_type, consts );
 943     Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
 944     for( unsigned i=0; i<consts.size(); i++ ){
 945       std::stringstream ss;
 946       ss << consts[i];
 947       Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
 948       ops[index].push_back( consts[i] );
 949       cnames[index].push_back( ss.str() );
 950       cargs[index].push_back( std::vector< CVC4::Type >() );
 951     }
 952     allow_const[index] = true;
 953   }else if( sgt.d_gterm_type==SygusGTerm::gterm_variable || sgt.d_gterm_type==SygusGTerm::gterm_input_variable ){
 954     if( sgt.getNumChildren()!=0 ){
 955       parseError("Bad syntax for Sygus Variable.");
 956     }
 957     Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
 958     for( unsigned i=0; i<sygus_vars.size(); i++ ){
 959       if( sygus_vars[i].getType()==sgt.d_type ){
 960         std::stringstream ss;
 961         ss << sygus_vars[i];
 962         Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
 963         ops[index].push_back( sygus_vars[i] );
 964         cnames[index].push_back( ss.str() );
 965         cargs[index].push_back( std::vector< CVC4::Type >() );
 966       }
 967     }
 968   }else if( sgt.d_gterm_type==SygusGTerm::gterm_nested_sort ){
 969     ret = sgt.d_type;
 970   }else if( sgt.d_gterm_type==SygusGTerm::gterm_unresolved ){
 971     if( isNested ){
 972       if( isUnresolvedType(sgt.d_name) ){
 973         ret = getSort(sgt.d_name);
 974       }else{
 975         //nested, unresolved symbol...fail
 976         std::stringstream ss;
 977         ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl;
 978         parseError(ss.str());
 979       }
 980     }else{
 981       //will resolve when adding constructors
 982       unresolved_gterm_sym[index].push_back(sgt.d_name);
 983     }
 984   }else if( sgt.d_gterm_type==SygusGTerm::gterm_ignore ){
 985
 986   }
 987 }
 988
 989 bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
 990                                   std::vector< CVC4::Datatype >& datatypes,
 991                                   std::vector< CVC4::Type>& sorts,
 992                                   std::vector< std::vector<CVC4::Expr> >& ops,
 993                                   std::vector< std::vector<std::string> >& cnames,
 994                                   std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 995                                   std::vector< bool >& allow_const,
 996                                   std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
 997   sorts.push_back(t);
 998   datatypes.push_back(Datatype(dname));
 999   ops.push_back(std::vector<Expr>());
1000   cnames.push_back(std::vector<std::string>());
1001   cargs.push_back(std::vector<std::vector<CVC4::Type> >());
1002   allow_const.push_back(false);
1003   unresolved_gterm_sym.push_back(std::vector< std::string >());
1004   return true;
1005 }
1006
1007 bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
1008                                  std::vector< CVC4::Type>& sorts,
1009                                  std::vector< std::vector<CVC4::Expr> >& ops,
1010                                  std::vector< std::vector<std::string> >& cnames,
1011                                  std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
1012                                  std::vector< bool >& allow_const,
1013                                  std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
1014   sorts.pop_back();
1015   datatypes.pop_back();
1016   ops.pop_back();
1017   cnames.pop_back();
1018   cargs.pop_back();
1019   allow_const.pop_back();
1020   unresolved_gterm_sym.pop_back();
1021   return true;
1022 }
1023
1024 Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
1025                                     std::vector< CVC4::Type>& sorts,
1026                                     std::vector< std::vector<CVC4::Expr> >& ops,
1027                                     std::vector< std::vector<std::string> >& cnames,
1028                                     std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
1029                                     std::vector< bool >& allow_const,
1030                                     std::vector< std::vector< std::string > >& unresolved_gterm_sym,
1031                                     std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
1032                                     std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) {
1033   Type t = sub_ret;
1034   Debug("parser-sygus") << "Argument is ";
1035   if( t.isNull() ){
1036     //then, it is the datatype we constructed, which should have a single constructor
1037     t = mkUnresolvedType(sub_dname);
1038     Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t << std::endl;
1039     Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs[sub_dt_index].size() << std::endl;
1040     if( cargs[sub_dt_index].empty() ){
1041       parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
1042     }
1043     Expr sop = ops[sub_dt_index][0];
1044     Type curr_t;
1045     if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){
1046       curr_t = sop.getType();
1047       Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl;
1048       // only cache if it is a singleton datatype (has unique expr)
1049       if (ops[sub_dt_index].size() == 1)
1050       {
1051         sygus_to_builtin_expr[t] = sop;
1052         // store that term sop has dedicated sygus type t
1053         if (d_sygus_bound_var_type.find(sop) == d_sygus_bound_var_type.end())
1054         {
1055           d_sygus_bound_var_type[sop] = t;
1056         }
1057       }
1058     }else{
1059       std::vector< Expr > children;
1060       if( sop.getKind() != kind::BUILTIN ){
1061         children.push_back( sop );
1062       }
1063       for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
1064         std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
1065         if( it==sygus_to_builtin_expr.end() ){
1066           if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){
1067             std::stringstream ss;
1068             ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl;
1069             ss << "Builtin types are currently : " << std::endl;
1070             for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){
1071               ss << "  " << itb->first << " -> " << itb->second << std::endl;
1072             }
1073             parseError(ss.str());
1074           }
1075           Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
1076           Debug("parser-sygus") << ":  child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
1077           std::stringstream ss;
1078           ss << t << "_x_" << i;
1079           Expr bv = mkBoundVar(ss.str(), bt);
1080           children.push_back( bv );
1081           d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i];
1082         }else{
1083           Debug("parser-sygus") << ":  child " << i << " existing sygus to builtin expr : " << it->second << std::endl;
1084           children.push_back( it->second );
1085         }
1086       }
1087       Kind sk = sop.getKind() != kind::BUILTIN
1088                     ? getKindForFunction(sop)
1089                     : getExprManager()->operatorToKind(sop);
1090       Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl;
1091       Expr e = getExprManager()->mkExpr( sk, children );
1092       Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
1093       curr_t = e.getType();
1094       sygus_to_builtin_expr[t] = e;
1095     }
1096     sorts[sub_dt_index] = curr_t;
1097     sygus_to_builtin[t] = curr_t;
1098   }else{
1099     Debug("parser-sygus") << "simple argument " << t << std::endl;
1100     Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl;
1101     //otherwise, datatype was unecessary
1102     //pop argument datatype definition
1103     popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
1104   }
1105   return t;
1106 }
1107
1108 void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
1109                                        int index,
1110                                        std::vector< CVC4::Datatype >& datatypes,
1111                                        std::vector< CVC4::Type>& sorts,
1112                                        std::vector< std::vector<CVC4::Expr> >& ops,
1113                                        std::vector< std::vector<std::string> >& cnames,
1114                                        std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
1115                                        std::vector<CVC4::Expr>& sygus_vars,
1116                                        std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
1117                                        std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ) {
1118   std::vector< CVC4::Expr > let_define_args;
1119   Expr let_body;
1120   int dindex = cargs[index].size()-1;
1121   Debug("parser-sygus") << "Process let constructor for datatype " << datatypes[index].getName() << ", #subtypes = " << cargs[index][dindex].size() << std::endl;
1122   for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
1123     Debug("parser-sygus") << "  " << i << " : " << cargs[index][dindex][i] << std::endl;
1124     if( i+1==cargs[index][dindex].size() ){
1125       std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[index][dindex][i] );
1126       if( it!=sygus_to_builtin_expr.end() ){
1127         let_body = it->second;
1128       }else{
1129         std::stringstream ss;
1130         ss << datatypes[index].getName() << "_body";
1131         let_body = mkBoundVar(ss.str(), sygus_to_builtin[cargs[index][dindex][i]]);
1132         d_sygus_bound_var_type[let_body] = cargs[index][dindex][i];
1133       }
1134     }
1135   }
1136   Debug("parser-sygus") << std::endl;
1137   Debug("parser-sygus") << "Body is " << let_body << std::endl;
1138   Debug("parser-sygus") << "# let vars = " << let_vars.size() << std::endl;
1139   for( unsigned i=0; i<let_vars.size(); i++ ){
1140     Debug("parser-sygus") << "  let var " << i << " : " << let_vars[i] << " " << let_vars[i].getType() << std::endl;
1141     let_define_args.push_back( let_vars[i] );
1142   }
1143   /*
1144   Debug("parser-sygus") << "index = " << index << ", start index = " << start_index << ", #Current datatypes = " << datatypes.size() << std::endl;
1145   for( unsigned i=start_index; i<datatypes.size(); i++ ){
1146     Debug("parser-sygus") << "  datatype " << i << " : " << datatypes[i].getName() << ", #cons = " << cargs[i].size() << std::endl;
1147     if( !cargs[i].empty() ){
1148       Debug("parser-sygus") << "  operator 0 is " << ops[i][0] << std::endl;
1149       Debug("parser-sygus") << "  cons 0 has " << cargs[i][0].size() << " sub fields." << std::endl;
1150       for( unsigned j=0; j<cargs[i][0].size(); j++ ){
1151         Type bt = sygus_to_builtin[cargs[i][0][j]];
1152         Debug("parser-sygus") << "    cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl;
1153       }
1154     }
1155   }
1156   */
1157   //last argument is the return, pop
1158   cargs[index][dindex].pop_back();
1159   collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );
1160
1161   Debug("parser-sygus") << "Make define-fun with "
1162                         << cargs[index][dindex].size()
1163                         << " operator arguments and " << let_define_args.size()
1164                         << " provided arguments..." << std::endl;
1165   if (cargs[index][dindex].size() != let_define_args.size())
1166   {
1167     std::stringstream ss;
1168     ss << "Wrong number of let body terms." << std::endl;
1169     parseError(ss.str());
1170   }
1171   std::vector<CVC4::Type> fsorts;
1172   for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
1173     Debug("parser-sygus") << "  " << i << " : " << let_define_args[i] << " " << let_define_args[i].getType() << " " << cargs[index][dindex][i] << std::endl;
1174     fsorts.push_back(let_define_args[i].getType());
1175   }
1176
1177   Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
1178   std::stringstream ss;
1179   ss << datatypes[index].getName() << "_let";
1180   Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
1181   d_sygus_defined_funs.push_back( let_func );
1182   preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) );
1183
1184   ops[index].pop_back();
1185   ops[index].push_back( let_func );
1186   cnames[index].pop_back();
1187   cnames[index].push_back(ss.str());
1188
1189   //mark function as let constructor
1190   d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_define_args.begin(), let_define_args.end() );
1191   d_sygus_let_func_to_body[let_func] = let_body;
1192   d_sygus_let_func_to_num_input_vars[let_func] = let_vars.size();
1193 }
1194
1195
1196 void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ) {
1197   if( e.getKind()==kind::BOUND_VARIABLE ){
1198     if( std::find( builtinArgs.begin(), builtinArgs.end(), e )==builtinArgs.end() ){
1199       builtinArgs.push_back( e );
1200       sygusArgs.push_back( d_sygus_bound_var_type[e] );
1201       if( d_sygus_bound_var_type[e].isNull() ){
1202         std::stringstream ss;
1203         ss << "While constructing body of let gterm, can't map " << e << " to sygus type." << std::endl;
1204         parseError(ss.str());
1205       }
1206     }
1207   }else{
1208     for( unsigned i=0; i<e.getNumChildren(); i++ ){
1209       collectSygusLetArgs( e[i], sygusArgs, builtinArgs );
1210     }
1211   }
1212 }
1213
1214 void Smt2::setSygusStartIndex( std::string& fun, int startIndex,
1215                                std::vector< CVC4::Datatype >& datatypes,
1216                                std::vector< CVC4::Type>& sorts,
1217                                std::vector< std::vector<CVC4::Expr> >& ops ) {
1218   if( startIndex>0 ){
1219     CVC4::Datatype tmp_dt = datatypes[0];
1220     Type tmp_sort = sorts[0];
1221     std::vector< Expr > tmp_ops;
1222     tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
1223     datatypes[0] = datatypes[startIndex];
1224     sorts[0] = sorts[startIndex];
1225     ops[0].clear();
1226     ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
1227     datatypes[startIndex] = tmp_dt;
1228     sorts[startIndex] = tmp_sort;
1229     ops[startIndex].clear();
1230     ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
1231   }else if( startIndex<0 ){
1232     std::stringstream ss;
1233     ss << "warning: no symbol named Start for synth-fun " << fun << std::endl;
1234     warning(ss.str());
1235   }
1236 }
1237
1238 void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
1239                             std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
1240                             std::vector<std::string>& unresolved_gterm_sym,
1241                             std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
1242   Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
1243   Debug("parser-sygus") << "  add constructors..." << std::endl;
1244
1245   Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl;
1246   Debug("parser-sygus") << "  add constructors..." << std::endl;
1247   // size of cnames changes, this loop must check size
1248   for (unsigned i = 0; i < cnames.size(); i++)
1249   {
1250     bool is_dup = false;
1251     bool is_dup_op = false;
1252     for (unsigned j = 0; j < i; j++)
1253     {
1254       if( ops[i]==ops[j] ){
1255         is_dup_op = true;
1256         if( cargs[i].size()==cargs[j].size() ){
1257           is_dup = true;
1258           for( unsigned k=0; k<cargs[i].size(); k++ ){
1259             if( cargs[i][k]!=cargs[j][k] ){
1260               is_dup = false;
1261               break;
1262             }
1263           }
1264         }
1265         if( is_dup ){
1266           break;
1267         }
1268       }
1269     }
1270     Debug("parser-sygus") << "SYGUS CONS " << i << " : ";
1271     if( is_dup ){
1272       Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl;
1273       ops.erase( ops.begin() + i, ops.begin() + i + 1 );
1274       cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 );
1275       cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 );
1276       i--;
1277     }
1278     else
1279     {
1280       std::shared_ptr<SygusPrintCallback> spc;
1281       if (is_dup_op)
1282       {
1283         Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i]
1284                               << std::endl;
1285         // make into define-fun
1286         std::vector<Type> ltypes;
1287         for (unsigned j = 0, size = cargs[i].size(); j < size; j++)
1288         {
1289           ltypes.push_back(sygus_to_builtin[cargs[i][j]]);
1290         }
1291         std::vector<Expr> largs;
1292         Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
1293
1294         // make the let_body
1295         std::vector<Expr> children;
1296         if (ops[i].getKind() != kind::BUILTIN)
1297         {
1298           children.push_back(ops[i]);
1299         }
1300         children.insert(children.end(), largs.begin(), largs.end());
1301         Kind sk = ops[i].getKind() != kind::BUILTIN
1302                       ? kind::APPLY_UF
1303                       : getExprManager()->operatorToKind(ops[i]);
1304         Expr body = getExprManager()->mkExpr(sk, children);
1305         // replace by lambda
1306         ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
1307         Debug("parser-sygus") << "  ...replace op : " << ops[i] << std::endl;
1308         // callback prints as the expression
1309         spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs);
1310       }
1311       else
1312       {
1313         std::map<Expr, Expr>::iterator it =
1314             d_sygus_let_func_to_body.find(ops[i]);
1315         if (it != d_sygus_let_func_to_body.end())
1316         {
1317           Debug("parser-sygus") << "--> Let expression " << ops[i] << std::endl;
1318           Expr let_body = it->second;
1319           std::vector<Expr> let_args = d_sygus_let_func_to_vars[ops[i]];
1320           unsigned let_num_input_args =
1321               d_sygus_let_func_to_num_input_vars[ops[i]];
1322           // the operator is just the body for the arguments
1323           std::vector<Type> ltypes;
1324           for (unsigned j = 0, size = let_args.size(); j < size; j++)
1325           {
1326             ltypes.push_back(let_args[j].getType());
1327           }
1328           std::vector<Expr> largs;
1329           Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
1330           Expr sbody = let_body.substitute(let_args, largs);
1331           ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, sbody);
1332           Debug("parser-sygus") << "  ...replace op : " << ops[i] << std::endl;
1333           // callback prints as a let expression
1334           spc = std::make_shared<printer::SygusLetExprPrintCallback>(
1335               let_body, let_args, let_num_input_args);
1336         }
1337         else if (ops[i].getType().isBitVector() && ops[i].isConst())
1338         {
1339           Debug("parser-sygus") << "--> Bit-vector constant " << ops[i] << " ("
1340                                 << cnames[i] << ")" << std::endl;
1341           // Since there are multiple output formats for bit-vectors and
1342           // we are required by sygus standards to print in the exact input
1343           // format given by the user, we use a print callback to custom print
1344           // the given name.
1345           spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
1346         }
1347         else if (isDefinedFunction(ops[i]))
1348         {
1349           Debug("parser-sygus") << "--> Defined function " << ops[i]
1350                                 << std::endl;
1351           // turn f into (lammbda (x) (f x))
1352           // in a degenerate case, ops[i] may be a defined constant,
1353           // in which case we do not replace by a lambda.
1354           if (ops[i].getType().isFunction())
1355           {
1356             std::vector<Type> ftypes =
1357                 static_cast<FunctionType>(ops[i].getType()).getArgTypes();
1358             std::vector<Expr> largs;
1359             Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
1360             largs.insert(largs.begin(), ops[i]);
1361             Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs);
1362             ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
1363             Debug("parser-sygus") << "  ...replace op : " << ops[i]
1364                                   << std::endl;
1365           }
1366           else
1367           {
1368             Debug("parser-sygus") << "  ...replace op : " << ops[i]
1369                                   << std::endl;
1370           }
1371           // keep a callback to say it should be printed with the defined name
1372           spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
1373         }
1374         else
1375         {
1376           Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl;
1377         }
1378       }
1379       // must rename to avoid duplication
1380       std::stringstream ss;
1381       ss << dt.getName() << "_" << i << "_" << cnames[i];
1382       cnames[i] = ss.str();
1383       Debug("parser-sygus") << "  construct the datatype " << cnames[i] << "..."
1384                             << std::endl;
1385       // add the sygus constructor
1386       dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc);
1387       Debug("parser-sygus") << "  finished constructing the datatype"
1388                             << std::endl;
1389     }
1390   }
1391
1392   Debug("parser-sygus") << "  add constructors for unresolved symbols..." << std::endl;
1393   if( !unresolved_gterm_sym.empty() ){
1394     std::vector< Type > types;
1395     Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl;
1396     for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){
1397       Debug("parser-sygus") << "  resolve : " << unresolved_gterm_sym[i] << std::endl;
1398       if( isUnresolvedType(unresolved_gterm_sym[i]) ){
1399         Debug("parser-sygus") << "    it is an unresolved type." << std::endl;
1400         Type t = getSort(unresolved_gterm_sym[i]);
1401         if( std::find( types.begin(), types.end(), t )==types.end() ){
1402           types.push_back( t );
1403           //identity element
1404           Type bt = dt.getSygusType();
1405           Debug("parser-sygus") << ":  make identity function for " << bt << ", argument type " << t << std::endl;
1406
1407           std::stringstream ss;
1408           ss << t << "_x";
1409           Expr var = mkBoundVar(ss.str(), bt);
1410           std::vector<Expr> lchildren;
1411           lchildren.push_back(
1412               getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var));
1413           lchildren.push_back(var);
1414           Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren);
1415
1416           // empty sygus callback (should not be printed)
1417           std::shared_ptr<SygusPrintCallback> sepc =
1418               std::make_shared<printer::SygusEmptyPrintCallback>();
1419
1420           //make the sygus argument list
1421           std::vector< Type > id_carg;
1422           id_carg.push_back( t );
1423           dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc);
1424
1425           //add to operators
1426           ops.push_back( id_op );
1427         }
1428       }else{
1429         Debug("parser-sygus") << "    ignore. (likely a free let variable)" << std::endl;
1430       }
1431     }
1432   }
1433 }
1434
1435 Expr Smt2::makeSygusBoundVarList(Datatype& dt,
1436                                  unsigned i,
1437                                  const std::vector<Type>& ltypes,
1438                                  std::vector<Expr>& lvars)
1439 {
1440   for (unsigned j = 0, size = ltypes.size(); j < size; j++)
1441   {
1442     std::stringstream ss;
1443     ss << dt.getName() << "_x_" << i << "_" << j;
1444     Expr v = mkBoundVar(ss.str(), ltypes[j]);
1445     lvars.push_back(v);
1446   }
1447   return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
1448 }
1449
1450 void Smt2::addSygusConstructorTerm(Datatype& dt,
1451                                    Expr term,
1452                                    std::map<Expr, Type>& ntsToUnres) const
1453 {
1454   Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl;
1455   // purify each occurrence of a non-terminal symbol in term, replace by
1456   // free variables. These become arguments to constructors. Notice we must do
1457   // a tree traversal in this function, since unique paths to the same term
1458   // should be treated as distinct terms.
1459   // Notice that let expressions are forbidden in the input syntax of term, so
1460   // this does not lead to exponential behavior with respect to input size.
1461   std::vector<Expr> args;
1462   std::vector<Type> cargs;
1463   Expr op = purifySygusGTerm(term, ntsToUnres, args, cargs);
1464   Trace("parser-sygus2") << "Purified operator " << op
1465                          << ", #args/cargs=" << args.size() << "/"
1466                          << cargs.size() << std::endl;
1467   std::shared_ptr<SygusPrintCallback> spc;
1468   // callback prints as the expression
1469   spc = std::make_shared<printer::SygusExprPrintCallback>(op, args);
1470   if (!args.empty())
1471   {
1472     bool pureVar = false;
1473     if (op.getNumChildren() == args.size())
1474     {
1475       pureVar = true;
1476       for (unsigned i = 0, nchild = op.getNumChildren(); i < nchild; i++)
1477       {
1478         if (op[i] != args[i])
1479         {
1480           pureVar = false;
1481           break;
1482         }
1483       }
1484     }
1485     Trace("parser-sygus2") << "Pure var is " << pureVar
1486                            << ", hasOp=" << op.hasOperator() << std::endl;
1487     if (pureVar && op.hasOperator())
1488     {
1489       // optimization: use just the operator if it an application to only vars
1490       op = op.getOperator();
1491     }
1492     else
1493     {
1494       Expr lbvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, args);
1495       // its operator is a lambda
1496       op = getExprManager()->mkExpr(kind::LAMBDA, lbvl, op);
1497     }
1498   }
1499   Trace("parser-sygus2") << "Generated operator " << op << std::endl;
1500   std::stringstream ss;
1501   ss << op.getKind();
1502   dt.addSygusConstructor(op, ss.str(), cargs, spc);
1503 }
1504
1505 Expr Smt2::purifySygusGTerm(Expr term,
1506                             std::map<Expr, Type>& ntsToUnres,
1507                             std::vector<Expr>& args,
1508                             std::vector<Type>& cargs) const
1509 {
1510   Trace("parser-sygus2-debug")
1511       << "purifySygusGTerm: " << term << " #nchild=" << term.getNumChildren()
1512       << std::endl;
1513   std::map<Expr, Type>::iterator itn = ntsToUnres.find(term);
1514   if (itn != ntsToUnres.end())
1515   {
1516     Expr ret = getExprManager()->mkBoundVar(term.getType());
1517     Trace("parser-sygus2-debug")
1518         << "...unresolved non-terminal, intro " << ret << std::endl;
1519     args.push_back(ret);
1520     cargs.push_back(itn->second);
1521     return ret;
1522   }
1523   std::vector<Expr> pchildren;
1524   // To test whether the operator should be passed to mkExpr below, we check
1525   // whether this term has an operator which is not constant. This includes
1526   // APPLY_UF terms, but excludes applications of interpreted symbols.
1527   if (term.hasOperator() && !term.getOperator().isConst())
1528   {
1529     pchildren.push_back(term.getOperator());
1530   }
1531   bool childChanged = false;
1532   for (unsigned i = 0, nchild = term.getNumChildren(); i < nchild; i++)
1533   {
1534     Trace("parser-sygus2-debug")
1535         << "......purify child " << i << " : " << term[i] << std::endl;
1536     Expr ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs);
1537     pchildren.push_back(ptermc);
1538     childChanged = childChanged || ptermc != term[i];
1539   }
1540   if (!childChanged)
1541   {
1542     Trace("parser-sygus2-debug") << "...no child changed" << std::endl;
1543     return term;
1544   }
1545   Expr nret = getExprManager()->mkExpr(term.getKind(), pchildren);
1546   Trace("parser-sygus2-debug")
1547       << "...child changed, return " << nret << std::endl;
1548   return nret;
1549 }
1550
1551 void Smt2::addSygusConstructorVariables(Datatype& dt,
1552                                         std::vector<Expr>& sygusVars,
1553                                         Type type) const
1554 {
1555   // each variable of appropriate type becomes a sygus constructor in dt.
1556   for (unsigned i = 0, size = sygusVars.size(); i < size; i++)
1557   {
1558     Expr v = sygusVars[i];
1559     if (v.getType() == type)
1560     {
1561       std::stringstream ss;
1562       ss << v;
1563       std::vector<CVC4::Type> cargs;
1564       dt.addSygusConstructor(v, ss.str(), cargs);
1565     }
1566   }
1567 }
1568
1569 InputLanguage Smt2::getLanguage() const
1570 {
1571   ExprManager* em = getExprManager();
1572   return em->getOptions().getInputLanguage();
1573 }
1574
1575 }  // namespace parser
1576 }/* CVC4 namespace */