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 <algorithm>
  19
  20 #include "base/check.h"
  21 #include "expr/type.h"
  22 #include "options/options.h"
  23 #include "parser/antlr_input.h"
  24 #include "parser/parser.h"
  25 #include "parser/smt2/smt2_input.h"
  26 #include "printer/sygus_print_callback.h"
  27 #include "util/bitvector.h"
  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, "extract");
 127   addIndexedOperator(kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat");
 128   addIndexedOperator(
 129       kind::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend");
 130   addIndexedOperator(
 131       kind::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend");
 132   addIndexedOperator(
 133       kind::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left");
 134   addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT,
 135                      api::BITVECTOR_ROTATE_RIGHT,
 136                      "rotate_right");
 137   addIndexedOperator(kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv");
 138 }
 139
 140 void Smt2::addDatatypesOperators()
 141 {
 142   Parser::addOperator(kind::APPLY_CONSTRUCTOR);
 143   Parser::addOperator(kind::APPLY_TESTER);
 144   Parser::addOperator(kind::APPLY_SELECTOR);
 145   Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
 146
 147   if (!strictModeEnabled())
 148   {
 149     addOperator(kind::DT_SIZE, "dt.size");
 150   }
 151 }
 152
 153 void Smt2::addStringOperators() {
 154   defineVar("re.all",
 155             getSolver()
 156                 ->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())
 157                 .getExpr());
 158
 159   addOperator(kind::STRING_CONCAT, "str.++");
 160   addOperator(kind::STRING_LENGTH, "str.len");
 161   addOperator(kind::STRING_SUBSTR, "str.substr" );
 162   addOperator(kind::STRING_STRCTN, "str.contains" );
 163   addOperator(kind::STRING_CHARAT, "str.at" );
 164   addOperator(kind::STRING_STRIDOF, "str.indexof" );
 165   addOperator(kind::STRING_STRREPL, "str.replace" );
 166   if (!strictModeEnabled())
 167   {
 168     addOperator(kind::STRING_TOLOWER, "str.tolower");
 169     addOperator(kind::STRING_TOUPPER, "str.toupper");
 170     addOperator(kind::STRING_REV, "str.rev");
 171   }
 172   addOperator(kind::STRING_PREFIX, "str.prefixof" );
 173   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
 174   addOperator(kind::STRING_FROM_CODE, "str.from_code");
 175   addOperator(kind::STRING_IS_DIGIT, "str.is_digit" );
 176
 177   // at the moment, we only use this syntax for smt2.6.1
 178   if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1
 179       || getLanguage() == language::input::LANG_SYGUS_V2)
 180   {
 181     addOperator(kind::STRING_ITOS, "str.from_int");
 182     addOperator(kind::STRING_STOI, "str.to_int");
 183     addOperator(kind::STRING_IN_REGEXP, "str.in_re");
 184     addOperator(kind::STRING_TO_REGEXP, "str.to_re");
 185     addOperator(kind::STRING_TO_CODE, "str.to_code");
 186     addOperator(kind::STRING_STRREPLALL, "str.replace_all");
 187   }
 188   else
 189   {
 190     addOperator(kind::STRING_ITOS, "int.to.str");
 191     addOperator(kind::STRING_STOI, "str.to.int");
 192     addOperator(kind::STRING_IN_REGEXP, "str.in.re");
 193     addOperator(kind::STRING_TO_REGEXP, "str.to.re");
 194     addOperator(kind::STRING_TO_CODE, "str.code");
 195     addOperator(kind::STRING_STRREPLALL, "str.replaceall");
 196   }
 197
 198   addOperator(kind::REGEXP_CONCAT, "re.++");
 199   addOperator(kind::REGEXP_UNION, "re.union");
 200   addOperator(kind::REGEXP_INTER, "re.inter");
 201   addOperator(kind::REGEXP_STAR, "re.*");
 202   addOperator(kind::REGEXP_PLUS, "re.+");
 203   addOperator(kind::REGEXP_OPT, "re.opt");
 204   addOperator(kind::REGEXP_RANGE, "re.range");
 205   addOperator(kind::REGEXP_LOOP, "re.loop");
 206   addOperator(kind::REGEXP_COMPLEMENT, "re.comp");
 207   addOperator(kind::REGEXP_DIFF, "re.diff");
 208   addOperator(kind::STRING_LT, "str.<");
 209   addOperator(kind::STRING_LEQ, "str.<=");
 210 }
 211
 212 void Smt2::addFloatingPointOperators() {
 213   addOperator(kind::FLOATINGPOINT_FP, "fp");
 214   addOperator(kind::FLOATINGPOINT_EQ, "fp.eq");
 215   addOperator(kind::FLOATINGPOINT_ABS, "fp.abs");
 216   addOperator(kind::FLOATINGPOINT_NEG, "fp.neg");
 217   addOperator(kind::FLOATINGPOINT_PLUS, "fp.add");
 218   addOperator(kind::FLOATINGPOINT_SUB, "fp.sub");
 219   addOperator(kind::FLOATINGPOINT_MULT, "fp.mul");
 220   addOperator(kind::FLOATINGPOINT_DIV, "fp.div");
 221   addOperator(kind::FLOATINGPOINT_FMA, "fp.fma");
 222   addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt");
 223   addOperator(kind::FLOATINGPOINT_REM, "fp.rem");
 224   addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral");
 225   addOperator(kind::FLOATINGPOINT_MIN, "fp.min");
 226   addOperator(kind::FLOATINGPOINT_MAX, "fp.max");
 227   addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq");
 228   addOperator(kind::FLOATINGPOINT_LT, "fp.lt");
 229   addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq");
 230   addOperator(kind::FLOATINGPOINT_GT, "fp.gt");
 231   addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal");
 232   addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal");
 233   addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero");
 234   addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite");
 235   addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN");
 236   addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative");
 237   addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
 238   addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
 239
 240   addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC,
 241                      api::FLOATINGPOINT_TO_FP_GENERIC,
 242                      "to_fp");
 243   addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
 244                      api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
 245                      "to_fp_unsigned");
 246   addIndexedOperator(
 247       kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
 248   addIndexedOperator(
 249       kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv");
 250
 251   if (!strictModeEnabled())
 252   {
 253     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
 254                        api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
 255                        "to_fp_bv");
 256     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
 257                        api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
 258                        "to_fp_fp");
 259     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL,
 260                        api::FLOATINGPOINT_TO_FP_REAL,
 261                        "to_fp_real");
 262     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
 263                        api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
 264                        "to_fp_signed");
 265   }
 266 }
 267
 268 void Smt2::addSepOperators() {
 269   addOperator(kind::SEP_STAR, "sep");
 270   addOperator(kind::SEP_PTO, "pto");
 271   addOperator(kind::SEP_WAND, "wand");
 272   addOperator(kind::SEP_EMP, "emp");
 273   Parser::addOperator(kind::SEP_STAR);
 274   Parser::addOperator(kind::SEP_PTO);
 275   Parser::addOperator(kind::SEP_WAND);
 276   Parser::addOperator(kind::SEP_EMP);
 277 }
 278
 279 void Smt2::addTheory(Theory theory) {
 280   switch(theory) {
 281   case THEORY_ARRAYS:
 282     addOperator(kind::SELECT, "select");
 283     addOperator(kind::STORE, "store");
 284     break;
 285
 286   case THEORY_BITVECTORS:
 287     addBitvectorOperators();
 288     break;
 289
 290   case THEORY_CORE:
 291     defineType("Bool", getExprManager()->booleanType());
 292     defineVar("true", getExprManager()->mkConst(true));
 293     defineVar("false", getExprManager()->mkConst(false));
 294     addOperator(kind::AND, "and");
 295     addOperator(kind::DISTINCT, "distinct");
 296     addOperator(kind::EQUAL, "=");
 297     addOperator(kind::IMPLIES, "=>");
 298     addOperator(kind::ITE, "ite");
 299     addOperator(kind::NOT, "not");
 300     addOperator(kind::OR, "or");
 301     addOperator(kind::XOR, "xor");
 302     break;
 303
 304   case THEORY_REALS_INTS:
 305     defineType("Real", getExprManager()->realType());
 306     addOperator(kind::DIVISION, "/");
 307     addOperator(kind::TO_INTEGER, "to_int");
 308     addOperator(kind::IS_INTEGER, "is_int");
 309     addOperator(kind::TO_REAL, "to_real");
 310     // falling through on purpose, to add Ints part of Reals_Ints
 311     CVC4_FALLTHROUGH;
 312   case THEORY_INTS:
 313     defineType("Int", getExprManager()->integerType());
 314     addArithmeticOperators();
 315     addOperator(kind::INTS_DIVISION, "div");
 316     addOperator(kind::INTS_MODULUS, "mod");
 317     addOperator(kind::ABS, "abs");
 318     addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE, "divisible");
 319     break;
 320
 321   case THEORY_REALS:
 322     defineType("Real", getExprManager()->realType());
 323     addArithmeticOperators();
 324     addOperator(kind::DIVISION, "/");
 325     if (!strictModeEnabled())
 326     {
 327       addOperator(kind::ABS, "abs");
 328     }
 329     break;
 330
 331   case THEORY_TRANSCENDENTALS:
 332     defineVar("real.pi",
 333               getExprManager()->mkNullaryOperator(getExprManager()->realType(),
 334                                                   CVC4::kind::PI));
 335     addTranscendentalOperators();
 336     break;
 337
 338   case THEORY_QUANTIFIERS: addQuantifiersOperators(); break;
 339
 340   case THEORY_SETS:
 341     defineVar("emptyset",
 342               d_solver->mkEmptySet(d_solver->getNullSort()).getExpr());
 343     // the Boolean sort is a placeholder here since we don't have type info
 344     // without type annotation
 345     defineVar("univset",
 346               d_solver->mkUniverseSet(d_solver->getBooleanSort()).getExpr());
 347
 348     addOperator(kind::UNION, "union");
 349     addOperator(kind::INTERSECTION, "intersection");
 350     addOperator(kind::SETMINUS, "setminus");
 351     addOperator(kind::SUBSET, "subset");
 352     addOperator(kind::MEMBER, "member");
 353     addOperator(kind::SINGLETON, "singleton");
 354     addOperator(kind::INSERT, "insert");
 355     addOperator(kind::CARD, "card");
 356     addOperator(kind::COMPLEMENT, "complement");
 357     addOperator(kind::JOIN, "join");
 358     addOperator(kind::PRODUCT, "product");
 359     addOperator(kind::TRANSPOSE, "transpose");
 360     addOperator(kind::TCLOSURE, "tclosure");
 361     break;
 362
 363   case THEORY_DATATYPES:
 364   {
 365     const std::vector<Type> types;
 366     defineType("Tuple", getExprManager()->mkTupleType(types));
 367     addDatatypesOperators();
 368     break;
 369   }
 370
 371   case THEORY_STRINGS:
 372     defineType("String", getExprManager()->stringType());
 373     defineType("RegLan", getExprManager()->regExpType());
 374     defineType("Int", getExprManager()->integerType());
 375
 376     if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
 377     {
 378       defineVar("re.none", d_solver->mkRegexpEmpty().getExpr());
 379     }
 380     else
 381     {
 382       defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr());
 383     }
 384     defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr());
 385
 386     addStringOperators();
 387     break;
 388
 389   case THEORY_UF:
 390     Parser::addOperator(kind::APPLY_UF);
 391
 392     if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
 393     {
 394       addOperator(kind::CARDINALITY_CONSTRAINT, "fmf.card");
 395       addOperator(kind::CARDINALITY_VALUE, "fmf.card.val");
 396     }
 397     break;
 398
 399   case THEORY_FP:
 400     defineType("RoundingMode", getExprManager()->roundingModeType());
 401     defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
 402     defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
 403     defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
 404     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
 405
 406     defineVar(
 407         "RNE",
 408         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
 409     defineVar(
 410         "roundNearestTiesToEven",
 411         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
 412     defineVar(
 413         "RNA",
 414         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
 415     defineVar(
 416         "roundNearestTiesToAway",
 417         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
 418     defineVar("RTP",
 419               d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
 420     defineVar("roundTowardPositive",
 421               d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
 422     defineVar("RTN",
 423               d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
 424     defineVar("roundTowardNegative",
 425               d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
 426     defineVar("RTZ",
 427               d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
 428     defineVar("roundTowardZero",
 429               d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
 430
 431     addFloatingPointOperators();
 432     break;
 433
 434   case THEORY_SEP:
 435     // the Boolean sort is a placeholder here since we don't have type info
 436     // without type annotation
 437     defineVar("sep.nil",
 438               d_solver->mkSepNil(d_solver->getBooleanSort()).getExpr());
 439
 440     addSepOperators();
 441     break;
 442
 443   default:
 444     std::stringstream ss;
 445     ss << "internal error: unsupported theory " << theory;
 446     throw ParserException(ss.str());
 447   }
 448 }
 449
 450 void Smt2::addOperator(Kind kind, const std::string& name) {
 451   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 452                   << std::endl;
 453   Parser::addOperator(kind);
 454   operatorKindMap[name] = kind;
 455 }
 456
 457 void Smt2::addIndexedOperator(Kind tKind,
 458                               api::Kind opKind,
 459                               const std::string& name)
 460 {
 461   Parser::addOperator(tKind);
 462   d_indexedOpKindMap[name] = opKind;
 463 }
 464
 465 Kind Smt2::getOperatorKind(const std::string& name) const {
 466   // precondition: isOperatorEnabled(name)
 467   return operatorKindMap.find(name)->second;
 468 }
 469
 470 bool Smt2::isOperatorEnabled(const std::string& name) const {
 471   return operatorKindMap.find(name) != operatorKindMap.end();
 472 }
 473
 474 bool Smt2::isTheoryEnabled(Theory theory) const {
 475   switch(theory) {
 476   case THEORY_ARRAYS:
 477     return d_logic.isTheoryEnabled(theory::THEORY_ARRAYS);
 478   case THEORY_BITVECTORS:
 479     return d_logic.isTheoryEnabled(theory::THEORY_BV);
 480   case THEORY_CORE:
 481     return true;
 482   case THEORY_DATATYPES:
 483     return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
 484   case THEORY_INTS:
 485     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 486       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
 487   case THEORY_REALS:
 488     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 489       ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
 490   case THEORY_REALS_INTS:
 491     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 492       d_logic.areIntegersUsed() && d_logic.areRealsUsed();
 493   case THEORY_QUANTIFIERS:
 494     return d_logic.isQuantified();
 495   case THEORY_SETS:
 496     return d_logic.isTheoryEnabled(theory::THEORY_SETS);
 497   case THEORY_STRINGS:
 498     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
 499   case THEORY_UF:
 500     return d_logic.isTheoryEnabled(theory::THEORY_UF);
 501   case THEORY_FP:
 502     return d_logic.isTheoryEnabled(theory::THEORY_FP);
 503   case THEORY_SEP:
 504     return d_logic.isTheoryEnabled(theory::THEORY_SEP);
 505   default:
 506     std::stringstream ss;
 507     ss << "internal error: unsupported theory " << theory;
 508     throw ParserException(ss.str());
 509   }
 510 }
 511
 512 bool Smt2::logicIsSet() {
 513   return d_logicSet;
 514 }
 515
 516 Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
 517   if (isAbstractValue(name))
 518   {
 519     return mkAbstractValue(name);
 520   }
 521   return Parser::getExpressionForNameAndType(name, t);
 522 }
 523
 524 api::Term Smt2::mkIndexedConstant(const std::string& name,
 525                                   const std::vector<uint64_t>& numerals)
 526 {
 527   if (isTheoryEnabled(THEORY_FP))
 528   {
 529     if (name == "+oo")
 530     {
 531       return d_solver->mkPosInf(numerals[0], numerals[1]);
 532     }
 533     else if (name == "-oo")
 534     {
 535       return d_solver->mkNegInf(numerals[0], numerals[1]);
 536     }
 537     else if (name == "NaN")
 538     {
 539       return d_solver->mkNaN(numerals[0], numerals[1]);
 540     }
 541     else if (name == "+zero")
 542     {
 543       return d_solver->mkPosZero(numerals[0], numerals[1]);
 544     }
 545     else if (name == "-zero")
 546     {
 547       return d_solver->mkNegZero(numerals[0], numerals[1]);
 548     }
 549   }
 550
 551   if (isTheoryEnabled(THEORY_BITVECTORS) && name.find("bv") == 0)
 552   {
 553     std::string bvStr = name.substr(2);
 554     return d_solver->mkBitVector(numerals[0], bvStr, 10);
 555   }
 556
 557   // NOTE: Theory parametric constants go here
 558
 559   parseError(std::string("Unknown indexed literal `") + name + "'");
 560   return api::Term();
 561 }
 562
 563 api::Op Smt2::mkIndexedOp(const std::string& name,
 564                           const std::vector<uint64_t>& numerals)
 565 {
 566   const auto& kIt = d_indexedOpKindMap.find(name);
 567   if (kIt != d_indexedOpKindMap.end())
 568   {
 569     api::Kind k = (*kIt).second;
 570     if (numerals.size() == 1)
 571     {
 572       return d_solver->mkOp(k, numerals[0]);
 573     }
 574     else if (numerals.size() == 2)
 575     {
 576       return d_solver->mkOp(k, numerals[0], numerals[1]);
 577     }
 578   }
 579
 580   parseError(std::string("Unknown indexed function `") + name + "'");
 581   return api::Op();
 582 }
 583
 584 Expr Smt2::mkDefineFunRec(
 585     const std::string& fname,
 586     const std::vector<std::pair<std::string, Type> >& sortedVarNames,
 587     Type t,
 588     std::vector<Expr>& flattenVars)
 589 {
 590   std::vector<Type> sorts;
 591   for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
 592   {
 593     sorts.push_back(svn.second);
 594   }
 595
 596   // make the flattened function type, add bound variables
 597   // to flattenVars if the defined function was given a function return type.
 598   Type ft = mkFlatFunctionType(sorts, t, flattenVars);
 599
 600   // allow overloading
 601   return mkVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
 602 }
 603
 604 void Smt2::pushDefineFunRecScope(
 605     const std::vector<std::pair<std::string, Type> >& sortedVarNames,
 606     Expr func,
 607     const std::vector<Expr>& flattenVars,
 608     std::vector<Expr>& bvs,
 609     bool bindingLevel)
 610 {
 611   pushScope(bindingLevel);
 612
 613   // bound variables are those that are explicitly named in the preamble
 614   // of the define-fun(s)-rec command, we define them here
 615   for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
 616   {
 617     Expr v = mkBoundVar(svn.first, svn.second);
 618     bvs.push_back(v);
 619   }
 620
 621   bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end());
 622 }
 623
 624 void Smt2::reset() {
 625   d_logicSet = false;
 626   d_seenSetLogic = false;
 627   d_logic = LogicInfo();
 628   operatorKindMap.clear();
 629   d_lastNamedTerm = std::pair<Expr, std::string>();
 630   this->Parser::reset();
 631
 632   if( !strictModeEnabled() ) {
 633     addTheory(Smt2::THEORY_CORE);
 634   }
 635 }
 636
 637 void Smt2::resetAssertions() {
 638   // Remove all declarations except the ones at level 0.
 639   while (this->scopeLevel() > 0) {
 640     this->popScope();
 641   }
 642 }
 643
 644 Smt2::SynthFunFactory::SynthFunFactory(
 645     Smt2* smt2,
 646     const std::string& fun,
 647     bool isInv,
 648     Type range,
 649     std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames)
 650     : d_smt2(smt2), d_fun(fun), d_isInv(isInv)
 651 {
 652   if (range.isNull())
 653   {
 654     smt2->parseError("Must supply return type for synth-fun.");
 655   }
 656   if (range.isFunction())
 657   {
 658     smt2->parseError("Cannot use synth-fun with function return type.");
 659   }
 660   std::vector<Type> varSorts;
 661   for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
 662   {
 663     varSorts.push_back(p.second);
 664   }
 665   Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
 666   Type synthFunType =
 667       varSorts.size() > 0
 668           ? d_smt2->getExprManager()->mkFunctionType(varSorts, range)
 669           : range;
 670
 671   // we do not allow overloading for synth fun
 672   d_synthFun = d_smt2->mkBoundVar(fun, synthFunType);
 673   // set the sygus type to be range by default, which is overwritten below
 674   // if a grammar is provided
 675   d_sygusType = range;
 676
 677   d_smt2->pushScope(true);
 678   d_sygusVars = d_smt2->mkBoundVars(sortedVarNames);
 679 }
 680
 681 Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); }
 682
 683 std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(Type grammar)
 684 {
 685   Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl;
 686   return std::unique_ptr<Command>(
 687       new SynthFunCommand(d_fun,
 688                           d_synthFun,
 689                           grammar.isNull() ? d_sygusType : grammar,
 690                           d_isInv,
 691                           d_sygusVars));
 692 }
 693
 694 std::unique_ptr<Command> Smt2::invConstraint(
 695     const std::vector<std::string>& names)
 696 {
 697   checkThatLogicIsSet();
 698   Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
 699   Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
 700
 701   if (names.size() != 4)
 702   {
 703     parseError(
 704         "Bad syntax for inv-constraint: expected 4 "
 705         "arguments.");
 706   }
 707
 708   std::vector<Expr> terms;
 709   for (const std::string& name : names)
 710   {
 711     if (!isDeclared(name))
 712     {
 713       std::stringstream ss;
 714       ss << "Function " << name << " in inv-constraint is not defined.";
 715       parseError(ss.str());
 716     }
 717
 718     terms.push_back(getVariable(name));
 719   }
 720
 721   return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms));
 722 }
 723
 724 Command* Smt2::setLogic(std::string name, bool fromCommand)
 725 {
 726   if (fromCommand)
 727   {
 728     if (d_seenSetLogic)
 729     {
 730       parseError("Only one set-logic is allowed.");
 731     }
 732     d_seenSetLogic = true;
 733
 734     if (logicIsForced())
 735     {
 736       // If the logic is forced, we ignore all set-logic requests from commands.
 737       return new EmptyCommand();
 738     }
 739   }
 740
 741   if (sygus_v1())
 742   {
 743     // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2)
 744     if(name == "Arrays") {
 745       name = "A";
 746     }else if(name == "Reals") {
 747       name = "LRA";
 748     }
 749   }
 750
 751   d_logicSet = true;
 752   d_logic = name;
 753
 754   // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
 755   // higher-order
 756   if(sygus()) {
 757     if (!d_logic.isQuantified())
 758     {
 759       warning("Logics in sygus are assumed to contain quantifiers.");
 760       warning("Omit QF_ from the logic to avoid this warning.");
 761     }
 762   }
 763
 764   // Core theory belongs to every logic
 765   addTheory(THEORY_CORE);
 766
 767   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 768     addTheory(THEORY_UF);
 769   }
 770
 771   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 772     if(d_logic.areIntegersUsed()) {
 773       if(d_logic.areRealsUsed()) {
 774         addTheory(THEORY_REALS_INTS);
 775       } else {
 776         addTheory(THEORY_INTS);
 777       }
 778     } else if(d_logic.areRealsUsed()) {
 779       addTheory(THEORY_REALS);
 780     }
 781
 782     if (d_logic.areTranscendentalsUsed())
 783     {
 784       addTheory(THEORY_TRANSCENDENTALS);
 785     }
 786   }
 787
 788   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
 789     addTheory(THEORY_ARRAYS);
 790   }
 791
 792   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 793     addTheory(THEORY_BITVECTORS);
 794   }
 795
 796   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
 797     addTheory(THEORY_DATATYPES);
 798   }
 799
 800   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 801     addTheory(THEORY_SETS);
 802   }
 803
 804   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 805     addTheory(THEORY_STRINGS);
 806   }
 807
 808   if(d_logic.isQuantified()) {
 809     addTheory(THEORY_QUANTIFIERS);
 810   }
 811
 812   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
 813     addTheory(THEORY_FP);
 814   }
 815
 816   if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
 817     addTheory(THEORY_SEP);
 818   }
 819
 820   Command* cmd =
 821       new SetBenchmarkLogicCommand(sygus() ? d_logic.getLogicString() : name);
 822   cmd->setMuted(!fromCommand);
 823   return cmd;
 824 } /* Smt2::setLogic() */
 825
 826 bool Smt2::sygus() const
 827 {
 828   InputLanguage ilang = getLanguage();
 829   return ilang == language::input::LANG_SYGUS
 830          || ilang == language::input::LANG_SYGUS_V2;
 831 }
 832 bool Smt2::sygus_v1() const
 833 {
 834   return getLanguage() == language::input::LANG_SYGUS;
 835 }
 836
 837 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 838   // TODO: ???
 839 }
 840
 841 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 842   // TODO: ???
 843 }
 844
 845 void Smt2::checkThatLogicIsSet()
 846 {
 847   if (!logicIsSet())
 848   {
 849     if (strictModeEnabled())
 850     {
 851       parseError("set-logic must appear before this point.");
 852     }
 853     else
 854     {
 855       Command* cmd = nullptr;
 856       if (logicIsForced())
 857       {
 858         cmd = setLogic(getForcedLogic(), false);
 859       }
 860       else
 861       {
 862         warning("No set-logic command was given before this point.");
 863         warning("CVC4 will make all theories available.");
 864         warning(
 865             "Consider setting a stricter logic for (likely) better "
 866             "performance.");
 867         warning("To suppress this warning in the future use (set-logic ALL).");
 868
 869         cmd = setLogic("ALL", false);
 870       }
 871       preemptCommand(cmd);
 872     }
 873   }
 874 }
 875
 876 /* The include are managed in the lexer but called in the parser */
 877 // Inspired by http://www.antlr3.org/api/C/interop.html
 878
 879 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 880   Debug("parser") << "Including " << filename << std::endl;
 881   // Create a new input stream and take advantage of built in stream stacking
 882   // in C target runtime.
 883   //
 884   pANTLR3_INPUT_STREAM    in;
 885 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 886   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 887 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 888   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 889 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 890   if( in == NULL ) {
 891     Debug("parser") << "Can't open " << filename << std::endl;
 892     return false;
 893   }
 894   // Same thing as the predefined PUSHSTREAM(in);
 895   lexer->pushCharStream(lexer, in);
 896   // restart it
 897   //lexer->rec->state->tokenStartCharIndex      = -10;
 898   //lexer->emit(lexer);
 899
 900   // Note that the input stream is not closed when it EOFs, I don't bother
 901   // to do it here, but it is up to you to track streams created like this
 902   // and destroy them when the whole parse session is complete. Remember that you
 903   // don't want to do this until all tokens have been manipulated all the way through
 904   // your tree parsers etc as the token does not store the text it just refers
 905   // back to the input stream and trying to get the text for it will abort if you
 906   // close the input stream too early.
 907
 908   //TODO what said before
 909   return true;
 910 }
 911
 912 void Smt2::includeFile(const std::string& filename) {
 913   // security for online version
 914   if(!canIncludeFile()) {
 915     parseError("include-file feature was disabled for this run.");
 916   }
 917
 918   // Get the lexer
 919   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 920   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 921   // get the name of the current stream "Does it work inside an include?"
 922   const std::string inputName = ai->getInputStreamName();
 923
 924   // Find the directory of the current input file
 925   std::string path;
 926   size_t pos = inputName.rfind('/');
 927   if(pos != std::string::npos) {
 928     path = std::string(inputName, 0, pos + 1);
 929   }
 930   path.append(filename);
 931   if(!newInputStream(path, lexer)) {
 932     parseError("Couldn't open include file `" + path + "'");
 933   }
 934 }
 935
 936 bool Smt2::isAbstractValue(const std::string& name)
 937 {
 938   return name.length() >= 2 && name[0] == '@' && name[1] != '0'
 939          && name.find_first_not_of("0123456789", 1) == std::string::npos;
 940 }
 941
 942 Expr Smt2::mkAbstractValue(const std::string& name)
 943 {
 944   assert(isAbstractValue(name));
 945   // remove the '@'
 946   return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1))));
 947 }
 948
 949 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
 950   if( type.isInteger() ){
 951     ops.push_back(getExprManager()->mkConst(Rational(0)));
 952     ops.push_back(getExprManager()->mkConst(Rational(1)));
 953   }else if( type.isBitVector() ){
 954     unsigned sz = ((BitVectorType)type).getSize();
 955     BitVector bval0(sz, (unsigned int)0);
 956     ops.push_back( getExprManager()->mkConst(bval0) );
 957     BitVector bval1(sz, (unsigned int)1);
 958     ops.push_back( getExprManager()->mkConst(bval1) );
 959   }else if( type.isBoolean() ){
 960     ops.push_back(getExprManager()->mkConst(true));
 961     ops.push_back(getExprManager()->mkConst(false));
 962   }
 963   //TODO : others?
 964 }
 965
 966 //  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)
 967 //  This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
 968 void Smt2::processSygusGTerm(
 969     CVC4::SygusGTerm& sgt,
 970     int index,
 971     std::vector<CVC4::Datatype>& datatypes,
 972     std::vector<CVC4::Type>& sorts,
 973     std::vector<std::vector<ParseOp>>& ops,
 974     std::vector<std::vector<std::string>>& cnames,
 975     std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
 976     std::vector<bool>& allow_const,
 977     std::vector<std::vector<std::string>>& unresolved_gterm_sym,
 978     const std::vector<CVC4::Expr>& sygus_vars,
 979     std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
 980     std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
 981     CVC4::Type& ret,
 982     bool isNested)
 983 {
 984   if (sgt.d_gterm_type == SygusGTerm::gterm_op)
 985   {
 986     Debug("parser-sygus") << "Add " << sgt.d_op << " to datatype "
 987                           << index << std::endl;
 988     Kind oldKind;
 989     Kind newKind = kind::UNDEFINED_KIND;
 990     //convert to UMINUS if one child of MINUS
 991     if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == kind::MINUS)
 992     {
 993       oldKind = kind::MINUS;
 994       newKind = kind::UMINUS;
 995     }
 996     if( newKind!=kind::UNDEFINED_KIND ){
 997       Debug("parser-sygus")
 998           << "Replace " << sgt.d_op.d_kind << " with " << newKind << std::endl;
 999       sgt.d_op.d_kind = newKind;
1000       std::string oldName = kind::kindToString(oldKind);
1001       std::string newName = kind::kindToString(newKind);
1002       size_t pos = 0;
1003       if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){
1004         sgt.d_name.replace(pos, oldName.length(), newName);
1005       }
1006     }
1007     ops[index].push_back(sgt.d_op);
1008     cnames[index].push_back( sgt.d_name );
1009     cargs[index].push_back( std::vector< CVC4::Type >() );
1010     for( unsigned i=0; i<sgt.d_children.size(); i++ ){
1011       std::stringstream ss;
1012       ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
1013       std::string sub_dname = ss.str();
1014       //add datatype for child
1015       Type null_type;
1016       pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
1017       int sub_dt_index = datatypes.size()-1;
1018       //process child
1019       Type sub_ret;
1020       processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
1021                          sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
1022       //process the nested gterm (either pop the last datatype, or flatten the argument)
1023       Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
1024                                          sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
1025       cargs[index].back().push_back(tt);
1026     }
1027   }
1028   else if (sgt.d_gterm_type == SygusGTerm::gterm_constant)
1029   {
1030     if( sgt.getNumChildren()!=0 ){
1031       parseError("Bad syntax for Sygus Constant.");
1032     }
1033     std::vector< Expr > consts;
1034     mkSygusConstantsForType( sgt.d_type, consts );
1035     Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
1036     for( unsigned i=0; i<consts.size(); i++ ){
1037       std::stringstream ss;
1038       ss << consts[i];
1039       Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
1040       ParseOp constOp;
1041       constOp.d_expr = consts[i];
1042       ops[index].push_back(constOp);
1043       cnames[index].push_back( ss.str() );
1044       cargs[index].push_back( std::vector< CVC4::Type >() );
1045     }
1046     allow_const[index] = true;
1047   }
1048   else if (sgt.d_gterm_type == SygusGTerm::gterm_variable
1049            || sgt.d_gterm_type == SygusGTerm::gterm_input_variable)
1050   {
1051     if( sgt.getNumChildren()!=0 ){
1052       parseError("Bad syntax for Sygus Variable.");
1053     }
1054     Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
1055     for( unsigned i=0; i<sygus_vars.size(); i++ ){
1056       if( sygus_vars[i].getType()==sgt.d_type ){
1057         std::stringstream ss;
1058         ss << sygus_vars[i];
1059         Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
1060         ParseOp varOp;
1061         varOp.d_expr = sygus_vars[i];
1062         ops[index].push_back(varOp);
1063         cnames[index].push_back( ss.str() );
1064         cargs[index].push_back( std::vector< CVC4::Type >() );
1065       }
1066     }
1067   }
1068   else if (sgt.d_gterm_type == SygusGTerm::gterm_nested_sort)
1069   {
1070     ret = sgt.d_type;
1071   }
1072   else if (sgt.d_gterm_type == SygusGTerm::gterm_unresolved)
1073   {
1074     if( isNested ){
1075       if( isUnresolvedType(sgt.d_name) ){
1076         ret = getSort(sgt.d_name);
1077       }else{
1078         //nested, unresolved symbol...fail
1079         std::stringstream ss;
1080         ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl;
1081         parseError(ss.str());
1082       }
1083     }else{
1084       //will resolve when adding constructors
1085       unresolved_gterm_sym[index].push_back(sgt.d_name);
1086     }
1087   }
1088   else if (sgt.d_gterm_type == SygusGTerm::gterm_ignore)
1089   {
1090     // do nothing
1091   }
1092 }
1093
1094 bool Smt2::pushSygusDatatypeDef(
1095     Type t,
1096     std::string& dname,
1097     std::vector<CVC4::Datatype>& datatypes,
1098     std::vector<CVC4::Type>& sorts,
1099     std::vector<std::vector<ParseOp>>& ops,
1100     std::vector<std::vector<std::string>>& cnames,
1101     std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
1102     std::vector<bool>& allow_const,
1103     std::vector<std::vector<std::string>>& unresolved_gterm_sym)
1104 {
1105   sorts.push_back(t);
1106   datatypes.push_back(Datatype(getExprManager(), dname));
1107   ops.push_back(std::vector<ParseOp>());
1108   cnames.push_back(std::vector<std::string>());
1109   cargs.push_back(std::vector<std::vector<CVC4::Type> >());
1110   allow_const.push_back(false);
1111   unresolved_gterm_sym.push_back(std::vector< std::string >());
1112   return true;
1113 }
1114
1115 bool Smt2::popSygusDatatypeDef(
1116     std::vector<CVC4::Datatype>& datatypes,
1117     std::vector<CVC4::Type>& sorts,
1118     std::vector<std::vector<ParseOp>>& ops,
1119     std::vector<std::vector<std::string>>& cnames,
1120     std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
1121     std::vector<bool>& allow_const,
1122     std::vector<std::vector<std::string>>& unresolved_gterm_sym)
1123 {
1124   sorts.pop_back();
1125   datatypes.pop_back();
1126   ops.pop_back();
1127   cnames.pop_back();
1128   cargs.pop_back();
1129   allow_const.pop_back();
1130   unresolved_gterm_sym.pop_back();
1131   return true;
1132 }
1133
1134 Type Smt2::processSygusNestedGTerm(
1135     int sub_dt_index,
1136     std::string& sub_dname,
1137     std::vector<CVC4::Datatype>& datatypes,
1138     std::vector<CVC4::Type>& sorts,
1139     std::vector<std::vector<ParseOp>>& ops,
1140     std::vector<std::vector<std::string>>& cnames,
1141     std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
1142     std::vector<bool>& allow_const,
1143     std::vector<std::vector<std::string>>& unresolved_gterm_sym,
1144     std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
1145     std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
1146     Type sub_ret)
1147 {
1148   Type t = sub_ret;
1149   Debug("parser-sygus") << "Argument is ";
1150   if( t.isNull() ){
1151     //then, it is the datatype we constructed, which should have a single constructor
1152     t = mkUnresolvedType(sub_dname);
1153     Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t << std::endl;
1154     Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs[sub_dt_index].size() << std::endl;
1155     if( cargs[sub_dt_index].empty() ){
1156       parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
1157     }
1158     ParseOp op = ops[sub_dt_index][0];
1159     Type curr_t;
1160     if (!op.d_expr.isNull()
1161         && (op.d_expr.isConst() || cargs[sub_dt_index][0].empty()))
1162     {
1163       Expr sop = op.d_expr;
1164       curr_t = sop.getType();
1165       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;
1166       // only cache if it is a singleton datatype (has unique expr)
1167       if (ops[sub_dt_index].size() == 1)
1168       {
1169         sygus_to_builtin_expr[t] = sop;
1170         // store that term sop has dedicated sygus type t
1171         if (d_sygus_bound_var_type.find(sop) == d_sygus_bound_var_type.end())
1172         {
1173           d_sygus_bound_var_type[sop] = t;
1174         }
1175       }
1176     }
1177     else
1178     {
1179       std::vector< Expr > children;
1180       for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
1181         std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
1182         if( it==sygus_to_builtin_expr.end() ){
1183           if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){
1184             std::stringstream ss;
1185             ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl;
1186             ss << "Builtin types are currently : " << std::endl;
1187             for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){
1188               ss << "  " << itb->first << " -> " << itb->second << std::endl;
1189             }
1190             parseError(ss.str());
1191           }
1192           Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
1193           Debug("parser-sygus") << ":  child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
1194           std::stringstream ss;
1195           ss << t << "_x_" << i;
1196           Expr bv = mkBoundVar(ss.str(), bt);
1197           children.push_back( bv );
1198           d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i];
1199         }else{
1200           Debug("parser-sygus") << ":  child " << i << " existing sygus to builtin expr : " << it->second << std::endl;
1201           children.push_back( it->second );
1202         }
1203       }
1204       Expr e = applyParseOp(op, children);
1205       Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
1206       curr_t = e.getType();
1207       sygus_to_builtin_expr[t] = e;
1208     }
1209     sorts[sub_dt_index] = curr_t;
1210     sygus_to_builtin[t] = curr_t;
1211   }else{
1212     Debug("parser-sygus") << "simple argument " << t << std::endl;
1213     Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl;
1214     //otherwise, datatype was unecessary
1215     //pop argument datatype definition
1216     popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
1217   }
1218   return t;
1219 }
1220
1221 void Smt2::setSygusStartIndex(const std::string& fun,
1222                               int startIndex,
1223                               std::vector<CVC4::Datatype>& datatypes,
1224                               std::vector<CVC4::Type>& sorts,
1225                               std::vector<std::vector<ParseOp>>& ops)
1226 {
1227   if( startIndex>0 ){
1228     CVC4::Datatype tmp_dt = datatypes[0];
1229     Type tmp_sort = sorts[0];
1230     std::vector<ParseOp> tmp_ops;
1231     tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
1232     datatypes[0] = datatypes[startIndex];
1233     sorts[0] = sorts[startIndex];
1234     ops[0].clear();
1235     ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
1236     datatypes[startIndex] = tmp_dt;
1237     sorts[startIndex] = tmp_sort;
1238     ops[startIndex].clear();
1239     ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
1240   }else if( startIndex<0 ){
1241     std::stringstream ss;
1242     ss << "warning: no symbol named Start for synth-fun " << fun << std::endl;
1243     warning(ss.str());
1244   }
1245 }
1246
1247 void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
1248                            std::vector<ParseOp>& ops,
1249                            std::vector<std::string>& cnames,
1250                            std::vector<std::vector<CVC4::Type>>& cargs,
1251                            std::vector<std::string>& unresolved_gterm_sym,
1252                            std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin)
1253 {
1254   Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
1255   Debug("parser-sygus") << "  add constructors..." << std::endl;
1256
1257   Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl;
1258   Debug("parser-sygus") << "  add constructors..." << std::endl;
1259   // size of cnames changes, this loop must check size
1260   for (unsigned i = 0; i < cnames.size(); i++)
1261   {
1262     bool is_dup = false;
1263     bool is_dup_op = false;
1264     for (unsigned j = 0; j < i; j++)
1265     {
1266       if( ops[i]==ops[j] ){
1267         is_dup_op = true;
1268         if( cargs[i].size()==cargs[j].size() ){
1269           is_dup = true;
1270           for( unsigned k=0; k<cargs[i].size(); k++ ){
1271             if( cargs[i][k]!=cargs[j][k] ){
1272               is_dup = false;
1273               break;
1274             }
1275           }
1276         }
1277         if( is_dup ){
1278           break;
1279         }
1280       }
1281     }
1282     Debug("parser-sygus") << "SYGUS CONS " << i << " : ";
1283     if( is_dup ){
1284       Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl;
1285       ops.erase( ops.begin() + i, ops.begin() + i + 1 );
1286       cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 );
1287       cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 );
1288       i--;
1289     }
1290     else
1291     {
1292       std::shared_ptr<SygusPrintCallback> spc;
1293       if (is_dup_op)
1294       {
1295         Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i]
1296                               << std::endl;
1297         // make into define-fun
1298         std::vector<Type> ltypes;
1299         for (unsigned j = 0, size = cargs[i].size(); j < size; j++)
1300         {
1301           ltypes.push_back(sygus_to_builtin[cargs[i][j]]);
1302         }
1303         std::vector<Expr> largs;
1304         Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
1305
1306         // make the let_body
1307         Expr body = applyParseOp(ops[i], largs);
1308         // replace by lambda
1309         ParseOp pLam;
1310         pLam.d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
1311         ops[i] = pLam;
1312         Debug("parser-sygus") << "  ...replace op : " << ops[i] << std::endl;
1313         // callback prints as the expression
1314         spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs);
1315       }
1316       else
1317       {
1318         Expr sop = ops[i].d_expr;
1319         if (!sop.isNull() && sop.getType().isBitVector() && sop.isConst())
1320         {
1321           Debug("parser-sygus") << "--> Bit-vector constant " << sop << " ("
1322                                 << cnames[i] << ")" << std::endl;
1323           // Since there are multiple output formats for bit-vectors and
1324           // we are required by sygus standards to print in the exact input
1325           // format given by the user, we use a print callback to custom print
1326           // the given name.
1327           spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
1328         }
1329         else if (!sop.isNull() && sop.getKind() == kind::VARIABLE)
1330         {
1331           Debug("parser-sygus") << "--> Defined function " << ops[i]
1332                                 << std::endl;
1333           // turn f into (lammbda (x) (f x))
1334           // in a degenerate case, ops[i] may be a defined constant,
1335           // in which case we do not replace by a lambda.
1336           if (sop.getType().isFunction())
1337           {
1338             std::vector<Type> ftypes =
1339                 static_cast<FunctionType>(sop.getType()).getArgTypes();
1340             std::vector<Expr> largs;
1341             Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
1342             largs.insert(largs.begin(), sop);
1343             Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs);
1344             ops[i].d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
1345             Debug("parser-sygus") << "  ...replace op : " << ops[i]
1346                                   << std::endl;
1347           }
1348           else
1349           {
1350             Debug("parser-sygus") << "  ...replace op : " << ops[i]
1351                                   << std::endl;
1352           }
1353           // keep a callback to say it should be printed with the defined name
1354           spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
1355         }
1356         else
1357         {
1358           Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl;
1359         }
1360       }
1361       // must rename to avoid duplication
1362       std::stringstream ss;
1363       ss << dt.getName() << "_" << i << "_" << cnames[i];
1364       cnames[i] = ss.str();
1365       Debug("parser-sygus") << "  construct the datatype " << cnames[i] << "..."
1366                             << std::endl;
1367       // Add the sygus constructor, either using the expression operator of
1368       // ops[i], or the kind.
1369       if (!ops[i].d_expr.isNull())
1370       {
1371         dt.addSygusConstructor(ops[i].d_expr, cnames[i], cargs[i], spc);
1372       }
1373       else if (ops[i].d_kind != kind::NULL_EXPR)
1374       {
1375         dt.addSygusConstructor(ops[i].d_kind, cnames[i], cargs[i], spc);
1376       }
1377       else
1378       {
1379         std::stringstream ss;
1380         ss << "unexpected parse operator for sygus constructor" << ops[i];
1381         parseError(ss.str());
1382       }
1383       Debug("parser-sygus") << "  finished constructing the datatype"
1384                             << std::endl;
1385     }
1386   }
1387
1388   Debug("parser-sygus") << "  add constructors for unresolved symbols..." << std::endl;
1389   if( !unresolved_gterm_sym.empty() ){
1390     std::vector< Type > types;
1391     Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl;
1392     for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){
1393       Debug("parser-sygus") << "  resolve : " << unresolved_gterm_sym[i] << std::endl;
1394       if( isUnresolvedType(unresolved_gterm_sym[i]) ){
1395         Debug("parser-sygus") << "    it is an unresolved type." << std::endl;
1396         Type t = getSort(unresolved_gterm_sym[i]);
1397         if( std::find( types.begin(), types.end(), t )==types.end() ){
1398           types.push_back( t );
1399           //identity element
1400           Type bt = dt.getSygusType();
1401           Debug("parser-sygus") << ":  make identity function for " << bt << ", argument type " << t << std::endl;
1402
1403           std::stringstream ss;
1404           ss << t << "_x";
1405           Expr var = mkBoundVar(ss.str(), bt);
1406           std::vector<Expr> lchildren;
1407           lchildren.push_back(
1408               getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var));
1409           lchildren.push_back(var);
1410           Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren);
1411
1412           // empty sygus callback (should not be printed)
1413           std::shared_ptr<SygusPrintCallback> sepc =
1414               std::make_shared<printer::SygusEmptyPrintCallback>();
1415
1416           //make the sygus argument list
1417           std::vector< Type > id_carg;
1418           id_carg.push_back( t );
1419           dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc);
1420
1421           //add to operators
1422           ParseOp idOp;
1423           idOp.d_expr = id_op;
1424           ops.push_back(idOp);
1425         }
1426       }else{
1427         std::stringstream ss;
1428         ss << "Unhandled sygus constructor " << unresolved_gterm_sym[i];
1429         throw ParserException(ss.str());
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   // Ensure that we do type checking here to catch sygus constructors with
1456   // malformed builtin operators. The argument "true" to getType here forces
1457   // a recursive well-typedness check.
1458   term.getType(true);
1459   // purify each occurrence of a non-terminal symbol in term, replace by
1460   // free variables. These become arguments to constructors. Notice we must do
1461   // a tree traversal in this function, since unique paths to the same term
1462   // should be treated as distinct terms.
1463   // Notice that let expressions are forbidden in the input syntax of term, so
1464   // this does not lead to exponential behavior with respect to input size.
1465   std::vector<api::Term> args;
1466   std::vector<api::Sort> cargs;
1467   api::Term op = purifySygusGTerm(api::Term(term), ntsToUnres, args, cargs);
1468   std::stringstream ssCName;
1469   ssCName << op.getKind();
1470   Trace("parser-sygus2") << "Purified operator " << op
1471                          << ", #args/cargs=" << args.size() << "/"
1472                          << cargs.size() << std::endl;
1473   std::shared_ptr<SygusPrintCallback> spc;
1474   // callback prints as the expression
1475   spc = std::make_shared<printer::SygusExprPrintCallback>(
1476       op.getExpr(), api::termVectorToExprs(args));
1477   if (!args.empty())
1478   {
1479     api::Term lbvl = d_solver->mkTerm(api::BOUND_VAR_LIST, args);
1480     // its operator is a lambda
1481     op = d_solver->mkTerm(api::LAMBDA, lbvl, op);
1482   }
1483   Trace("parser-sygus2") << "addSygusConstructor:  operator " << op
1484                          << std::endl;
1485   dt.addSygusConstructor(
1486       op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs), spc);
1487 }
1488
1489 api::Term Smt2::purifySygusGTerm(api::Term term,
1490                                  std::map<Expr, Type>& ntsToUnres,
1491                                  std::vector<api::Term>& args,
1492                                  std::vector<api::Sort>& cargs) const
1493 {
1494   Trace("parser-sygus2-debug")
1495       << "purifySygusGTerm: " << term
1496       << " #nchild=" << term.getExpr().getNumChildren() << std::endl;
1497   std::map<Expr, Type>::iterator itn = ntsToUnres.find(term.getExpr());
1498   if (itn != ntsToUnres.end())
1499   {
1500     api::Term ret = d_solver->mkVar(term.getSort());
1501     Trace("parser-sygus2-debug")
1502         << "...unresolved non-terminal, intro " << ret << std::endl;
1503     args.push_back(ret.getExpr());
1504     cargs.push_back(itn->second);
1505     return ret;
1506   }
1507   std::vector<api::Term> pchildren;
1508   bool childChanged = false;
1509   for (unsigned i = 0, nchild = term.getNumChildren(); i < nchild; i++)
1510   {
1511     Trace("parser-sygus2-debug")
1512         << "......purify child " << i << " : " << term[i] << std::endl;
1513     api::Term ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs);
1514     pchildren.push_back(ptermc);
1515     childChanged = childChanged || ptermc != term[i];
1516   }
1517   if (!childChanged)
1518   {
1519     Trace("parser-sygus2-debug") << "...no child changed" << std::endl;
1520     return term;
1521   }
1522   api::Term nret = d_solver->mkTerm(term.getOp(), pchildren);
1523   Trace("parser-sygus2-debug")
1524       << "...child changed, return " << nret << std::endl;
1525   return nret;
1526 }
1527
1528 void Smt2::addSygusConstructorVariables(Datatype& dt,
1529                                         const std::vector<Expr>& sygusVars,
1530                                         Type type) const
1531 {
1532   // each variable of appropriate type becomes a sygus constructor in dt.
1533   for (unsigned i = 0, size = sygusVars.size(); i < size; i++)
1534   {
1535     Expr v = sygusVars[i];
1536     if (v.getType() == type)
1537     {
1538       std::stringstream ss;
1539       ss << v;
1540       std::vector<CVC4::Type> cargs;
1541       dt.addSygusConstructor(v, ss.str(), cargs);
1542     }
1543   }
1544 }
1545
1546 InputLanguage Smt2::getLanguage() const
1547 {
1548   ExprManager* em = getExprManager();
1549   return em->getOptions().getInputLanguage();
1550 }
1551
1552 void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type)
1553 {
1554   Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type
1555                   << std::endl;
1556   // (as const (Array T1 T2))
1557   if (p.d_kind == kind::STORE_ALL)
1558   {
1559     if (!type.isArray())
1560     {
1561       std::stringstream ss;
1562       ss << "expected array constant term, but cast is not of array type"
1563          << std::endl
1564          << "cast type: " << type;
1565       parseError(ss.str());
1566     }
1567     p.d_type = type;
1568     return;
1569   }
1570   if (p.d_expr.isNull())
1571   {
1572     Trace("parser-overloading")
1573         << "Getting variable expression with name " << p.d_name << " and type "
1574         << type << std::endl;
1575     // get the variable expression for the type
1576     if (isDeclared(p.d_name, SYM_VARIABLE))
1577     {
1578       p.d_expr = getExpressionForNameAndType(p.d_name, type);
1579     }
1580     if (p.d_expr.isNull())
1581     {
1582       std::stringstream ss;
1583       ss << "Could not resolve expression with name " << p.d_name
1584          << " and type " << type << std::endl;
1585       parseError(ss.str());
1586     }
1587   }
1588   Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr;
1589   Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getType();
1590   Trace("parser-qid") << std::endl;
1591   // otherwise, we process the type ascription
1592   p.d_expr =
1593       applyTypeAscription(api::Term(p.d_expr), api::Sort(type)).getExpr();
1594 }
1595
1596 Expr Smt2::parseOpToExpr(ParseOp& p)
1597 {
1598   Expr expr;
1599   if (p.d_kind != kind::NULL_EXPR || !p.d_type.isNull())
1600   {
1601     parseError(
1602         "Bad syntax for qualified identifier operator in term position.");
1603   }
1604   else if (!p.d_expr.isNull())
1605   {
1606     expr = p.d_expr;
1607   }
1608   else if (!isDeclared(p.d_name, SYM_VARIABLE))
1609   {
1610     if (sygus_v1() && p.d_name[0] == '-'
1611         && p.d_name.find_first_not_of("0123456789", 1) == std::string::npos)
1612     {
1613       // allow unary minus in sygus version 1
1614       expr = getExprManager()->mkConst(Rational(p.d_name));
1615     }
1616     else
1617     {
1618       std::stringstream ss;
1619       ss << "Symbol " << p.d_name << " is not declared.";
1620       parseError(ss.str());
1621     }
1622   }
1623   else
1624   {
1625     expr = getExpressionForName(p.d_name);
1626   }
1627   assert(!expr.isNull());
1628   return expr;
1629 }
1630
1631 Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
1632 {
1633   bool isBuiltinOperator = false;
1634   // the builtin kind of the overall return expression
1635   Kind kind = kind::NULL_EXPR;
1636   // First phase: process the operator
1637   if (Debug.isOn("parser"))
1638   {
1639     Debug("parser") << "applyParseOp: " << p << " to:" << std::endl;
1640     for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
1641     {
1642       Debug("parser") << "++ " << *i << std::endl;
1643     }
1644   }
1645   api::Op op;
1646   if (p.d_kind != kind::NULL_EXPR)
1647   {
1648     // It is a special case, e.g. tupSel or array constant specification.
1649     // We have to wait until the arguments are parsed to resolve it.
1650   }
1651   else if (!p.d_expr.isNull())
1652   {
1653     // An explicit operator, e.g. an indexed symbol.
1654     args.insert(args.begin(), p.d_expr);
1655     Kind fkind = getKindForFunction(p.d_expr);
1656     if (fkind != kind::UNDEFINED_KIND)
1657     {
1658       // Some operators may require a specific kind.
1659       // Testers are handled differently than other indexed operators,
1660       // since they require a kind.
1661       kind = fkind;
1662     }
1663   }
1664   else if (!p.d_op.isNull())
1665   {
1666     // it was given an operator
1667     op = p.d_op;
1668   }
1669   else
1670   {
1671     isBuiltinOperator = isOperatorEnabled(p.d_name);
1672     if (isBuiltinOperator)
1673     {
1674       // a builtin operator, convert to kind
1675       kind = getOperatorKind(p.d_name);
1676     }
1677     else
1678     {
1679       // A non-built-in function application, get the expression
1680       checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE);
1681       Expr v = getVariable(p.d_name);
1682       if (!v.isNull())
1683       {
1684         checkFunctionLike(v);
1685         kind = getKindForFunction(v);
1686         args.insert(args.begin(), v);
1687       }
1688       else
1689       {
1690         // Overloaded symbol?
1691         // Could not find the expression. It may be an overloaded symbol,
1692         // in which case we may find it after knowing the types of its
1693         // arguments.
1694         std::vector<Type> argTypes;
1695         for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
1696         {
1697           argTypes.push_back((*i).getType());
1698         }
1699         Expr op = getOverloadedFunctionForTypes(p.d_name, argTypes);
1700         if (!op.isNull())
1701         {
1702           checkFunctionLike(op);
1703           kind = getKindForFunction(op);
1704           args.insert(args.begin(), op);
1705         }
1706         else
1707         {
1708           parseError(
1709               "Cannot find unambiguous overloaded function for argument "
1710               "types.");
1711         }
1712       }
1713     }
1714   }
1715   // Second phase: apply the arguments to the parse op
1716   ExprManager* em = getExprManager();
1717   // handle special cases
1718   if (p.d_kind == kind::STORE_ALL && !p.d_type.isNull())
1719   {
1720     if (args.size() != 1)
1721     {
1722       parseError("Too many arguments to array constant.");
1723     }
1724     Expr constVal = args[0];
1725     if (!constVal.isConst())
1726     {
1727       // To parse array constants taking reals whose values are specified by
1728       // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
1729       // the fact that (/ 1 3) is the division of constants 1 and 3, and not
1730       // the resulting constant rational value. Thus, we must construct the
1731       // resulting rational here. This also is applied for integral real values
1732       // like 5.0 which are converted to (/ 5 1) to distinguish them from
1733       // integer constants. We must ensure numerator and denominator are
1734       // constant and the denominator is non-zero.
1735       if (constVal.getKind() == kind::DIVISION && constVal[0].isConst()
1736           && constVal[1].isConst()
1737           && !constVal[1].getConst<Rational>().isZero())
1738       {
1739         constVal = em->mkConst(constVal[0].getConst<Rational>()
1740                                / constVal[1].getConst<Rational>());
1741       }
1742       if (!constVal.isConst())
1743       {
1744         std::stringstream ss;
1745         ss << "expected constant term inside array constant, but found "
1746            << "nonconstant term:" << std::endl
1747            << "the term: " << constVal;
1748         parseError(ss.str());
1749       }
1750     }
1751     ArrayType aqtype = static_cast<ArrayType>(p.d_type);
1752     if (!aqtype.getConstituentType().isComparableTo(constVal.getType()))
1753     {
1754       std::stringstream ss;
1755       ss << "type mismatch inside array constant term:" << std::endl
1756          << "array type:          " << p.d_type << std::endl
1757          << "expected const type: " << aqtype.getConstituentType() << std::endl
1758          << "computed const type: " << constVal.getType();
1759       parseError(ss.str());
1760     }
1761     return em->mkConst(ArrayStoreAll(p.d_type, constVal));
1762   }
1763   else if (p.d_kind == kind::APPLY_SELECTOR && !p.d_expr.isNull())
1764   {
1765     // tuple selector case
1766     Integer x = p.d_expr.getConst<Rational>().getNumerator();
1767     if (!x.fitsUnsignedInt())
1768     {
1769       parseError("index of tupSel is larger than size of unsigned int");
1770     }
1771     unsigned int n = x.toUnsignedInt();
1772     if (args.size() > 1)
1773     {
1774       parseError("tupSel applied to more than one tuple argument");
1775     }
1776     Type t = args[0].getType();
1777     if (!t.isTuple())
1778     {
1779       parseError("tupSel applied to non-tuple");
1780     }
1781     size_t length = ((DatatypeType)t).getTupleLength();
1782     if (n >= length)
1783     {
1784       std::stringstream ss;
1785       ss << "tuple is of length " << length << "; cannot access index " << n;
1786       parseError(ss.str());
1787     }
1788     const Datatype& dt = ((DatatypeType)t).getDatatype();
1789     return em->mkExpr(kind::APPLY_SELECTOR, dt[0][n].getSelector(), args);
1790   }
1791   else if (p.d_kind != kind::NULL_EXPR)
1792   {
1793     // it should not have an expression or type specified at this point
1794     if (!p.d_expr.isNull() || !p.d_type.isNull())
1795     {
1796       std::stringstream ss;
1797       ss << "Could not process parsed qualified identifier kind " << p.d_kind;
1798       parseError(ss.str());
1799     }
1800     // otherwise it is a simple application
1801     kind = p.d_kind;
1802   }
1803   else if (isBuiltinOperator)
1804   {
1805     if (!em->getOptions().getUfHo()
1806         && (kind == kind::EQUAL || kind == kind::DISTINCT))
1807     {
1808       // need --uf-ho if these operators are applied over function args
1809       for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
1810       {
1811         if ((*i).getType().isFunction())
1812         {
1813           parseError(
1814               "Cannot apply equalty to functions unless --uf-ho is set.");
1815         }
1816       }
1817     }
1818     if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR)
1819         && args.size() == 1)
1820     {
1821       // Unary AND/OR can be replaced with the argument.
1822       return args[0];
1823     }
1824     else if (kind == kind::MINUS && args.size() == 1)
1825     {
1826       return em->mkExpr(kind::UMINUS, args[0]);
1827     }
1828     api::Term ret =
1829         d_solver->mkTerm(intToExtKind(kind), api::exprVectorToTerms(args));
1830     Debug("parser") << "applyParseOp: return default builtin " << ret
1831                     << std::endl;
1832     return ret.getExpr();
1833   }
1834
1835   if (args.size() >= 2)
1836   {
1837     // may be partially applied function, in this case we use HO_APPLY
1838     Type argt = args[0].getType();
1839     if (argt.isFunction())
1840     {
1841       unsigned arity = static_cast<FunctionType>(argt).getArity();
1842       if (args.size() - 1 < arity)
1843       {
1844         if (!em->getOptions().getUfHo())
1845         {
1846           parseError("Cannot partially apply functions unless --uf-ho is set.");
1847         }
1848         Debug("parser") << "Partial application of " << args[0];
1849         Debug("parser") << " : #argTypes = " << arity;
1850         Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
1851         // must curry the partial application
1852         return em->mkLeftAssociative(kind::HO_APPLY, args);
1853       }
1854     }
1855   }
1856   if (!op.isNull())
1857   {
1858     api::Term ret = d_solver->mkTerm(op, api::exprVectorToTerms(args));
1859     Debug("parser") << "applyParseOp: return op : " << ret << std::endl;
1860     return ret.getExpr();
1861   }
1862   if (kind == kind::NULL_EXPR)
1863   {
1864     std::vector<Expr> eargs(args.begin() + 1, args.end());
1865     return em->mkExpr(args[0], eargs);
1866   }
1867   return em->mkExpr(kind, args);
1868 }
1869
1870 Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr)
1871 {
1872   if (!sexpr.isKeyword())
1873   {
1874     parseError("improperly formed :named annotation");
1875   }
1876   std::string name = sexpr.getValue();
1877   checkUserSymbol(name);
1878   // ensure expr is a closed subterm
1879   if (expr.hasFreeVariable())
1880   {
1881     std::stringstream ss;
1882     ss << ":named annotations can only name terms that are closed";
1883     parseError(ss.str());
1884   }
1885   // check that sexpr is a fresh function symbol, and reserve it
1886   reserveSymbolAtAssertionLevel(name);
1887   // define it
1888   Expr func = mkVar(name, expr.getType(), ExprManager::VAR_FLAG_DEFINED);
1889   // remember the last term to have been given a :named attribute
1890   setLastNamedTerm(expr, name);
1891   return func;
1892 }
1893
1894 Expr Smt2::mkAnd(const std::vector<Expr>& es)
1895 {
1896   ExprManager* em = getExprManager();
1897
1898   if (es.size() == 0)
1899   {
1900     return em->mkConst(true);
1901   }
1902   else if (es.size() == 1)
1903   {
1904     return es[0];
1905   }
1906   else
1907   {
1908     return em->mkExpr(kind::AND, es);
1909   }
1910 }
1911
1912 }  // namespace parser
1913 }/* CVC4 namespace */