src/parser/smt2/smt2.cpp

   1 /*********************                                                        */
   2 /*! \file smt2.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 "util/bitvector.h"
  27
  28 // ANTLR defines these, which is really bad!
  29 #undef true
  30 #undef false
  31
  32 namespace CVC4 {
  33 namespace parser {
  34
  35 Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
  36     : Parser(solver, input, strictMode, parseOnly),
  37       d_logicSet(false),
  38       d_seenSetLogic(false)
  39 {
  40   pushScope(true);
  41 }
  42
  43 Smt2::~Smt2() { popScope(); }
  44
  45 void Smt2::addArithmeticOperators() {
  46   addOperator(api::PLUS, "+");
  47   addOperator(api::MINUS, "-");
  48   // api::MINUS is converted to api::UMINUS if there is only a single operand
  49   Parser::addOperator(api::UMINUS);
  50   addOperator(api::MULT, "*");
  51   addOperator(api::LT, "<");
  52   addOperator(api::LEQ, "<=");
  53   addOperator(api::GT, ">");
  54   addOperator(api::GEQ, ">=");
  55
  56   if (!strictModeEnabled())
  57   {
  58     // NOTE: this operator is non-standard
  59     addOperator(api::POW, "^");
  60   }
  61 }
  62
  63 void Smt2::addTranscendentalOperators()
  64 {
  65   addOperator(api::EXPONENTIAL, "exp");
  66   addOperator(api::SINE, "sin");
  67   addOperator(api::COSINE, "cos");
  68   addOperator(api::TANGENT, "tan");
  69   addOperator(api::COSECANT, "csc");
  70   addOperator(api::SECANT, "sec");
  71   addOperator(api::COTANGENT, "cot");
  72   addOperator(api::ARCSINE, "arcsin");
  73   addOperator(api::ARCCOSINE, "arccos");
  74   addOperator(api::ARCTANGENT, "arctan");
  75   addOperator(api::ARCCOSECANT, "arccsc");
  76   addOperator(api::ARCSECANT, "arcsec");
  77   addOperator(api::ARCCOTANGENT, "arccot");
  78   addOperator(api::SQRT, "sqrt");
  79 }
  80
  81 void Smt2::addQuantifiersOperators()
  82 {
  83   if (!strictModeEnabled())
  84   {
  85     addOperator(api::INST_CLOSURE, "inst-closure");
  86   }
  87 }
  88
  89 void Smt2::addBitvectorOperators() {
  90   addOperator(api::BITVECTOR_CONCAT, "concat");
  91   addOperator(api::BITVECTOR_NOT, "bvnot");
  92   addOperator(api::BITVECTOR_AND, "bvand");
  93   addOperator(api::BITVECTOR_OR, "bvor");
  94   addOperator(api::BITVECTOR_NEG, "bvneg");
  95   addOperator(api::BITVECTOR_PLUS, "bvadd");
  96   addOperator(api::BITVECTOR_MULT, "bvmul");
  97   addOperator(api::BITVECTOR_UDIV, "bvudiv");
  98   addOperator(api::BITVECTOR_UREM, "bvurem");
  99   addOperator(api::BITVECTOR_SHL, "bvshl");
 100   addOperator(api::BITVECTOR_LSHR, "bvlshr");
 101   addOperator(api::BITVECTOR_ULT, "bvult");
 102   addOperator(api::BITVECTOR_NAND, "bvnand");
 103   addOperator(api::BITVECTOR_NOR, "bvnor");
 104   addOperator(api::BITVECTOR_XOR, "bvxor");
 105   addOperator(api::BITVECTOR_XNOR, "bvxnor");
 106   addOperator(api::BITVECTOR_COMP, "bvcomp");
 107   addOperator(api::BITVECTOR_SUB, "bvsub");
 108   addOperator(api::BITVECTOR_SDIV, "bvsdiv");
 109   addOperator(api::BITVECTOR_SREM, "bvsrem");
 110   addOperator(api::BITVECTOR_SMOD, "bvsmod");
 111   addOperator(api::BITVECTOR_ASHR, "bvashr");
 112   addOperator(api::BITVECTOR_ULE, "bvule");
 113   addOperator(api::BITVECTOR_UGT, "bvugt");
 114   addOperator(api::BITVECTOR_UGE, "bvuge");
 115   addOperator(api::BITVECTOR_SLT, "bvslt");
 116   addOperator(api::BITVECTOR_SLE, "bvsle");
 117   addOperator(api::BITVECTOR_SGT, "bvsgt");
 118   addOperator(api::BITVECTOR_SGE, "bvsge");
 119   addOperator(api::BITVECTOR_REDOR, "bvredor");
 120   addOperator(api::BITVECTOR_REDAND, "bvredand");
 121
 122   addIndexedOperator(api::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract");
 123   addIndexedOperator(api::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat");
 124   addIndexedOperator(
 125       api::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend");
 126   addIndexedOperator(
 127       api::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend");
 128   addIndexedOperator(
 129       api::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left");
 130   addIndexedOperator(
 131       api::BITVECTOR_ROTATE_RIGHT, api::BITVECTOR_ROTATE_RIGHT, "rotate_right");
 132 }
 133
 134 void Smt2::addDatatypesOperators()
 135 {
 136   Parser::addOperator(api::APPLY_CONSTRUCTOR);
 137   Parser::addOperator(api::APPLY_TESTER);
 138   Parser::addOperator(api::APPLY_SELECTOR);
 139
 140   if (!strictModeEnabled())
 141   {
 142     addOperator(api::DT_SIZE, "dt.size");
 143   }
 144 }
 145
 146 void Smt2::addStringOperators() {
 147   defineVar(
 148       "re.all",
 149       getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma()));
 150   addOperator(api::STRING_CONCAT, "str.++");
 151   addOperator(api::STRING_LENGTH, "str.len");
 152   addOperator(api::STRING_SUBSTR, "str.substr");
 153   addOperator(api::STRING_CONTAINS, "str.contains");
 154   addOperator(api::STRING_CHARAT, "str.at");
 155   addOperator(api::STRING_INDEXOF, "str.indexof");
 156   addOperator(api::STRING_REPLACE, "str.replace");
 157   addOperator(api::STRING_PREFIX, "str.prefixof");
 158   addOperator(api::STRING_SUFFIX, "str.suffixof");
 159   addOperator(api::STRING_FROM_CODE, "str.from_code");
 160   addOperator(api::STRING_IS_DIGIT, "str.is_digit");
 161   addOperator(api::STRING_REPLACE_RE, "str.replace_re");
 162   addOperator(api::STRING_REPLACE_RE_ALL, "str.replace_re_all");
 163   if (!strictModeEnabled())
 164   {
 165     addOperator(api::STRING_UPDATE, "str.update");
 166     addOperator(api::STRING_TOLOWER, "str.tolower");
 167     addOperator(api::STRING_TOUPPER, "str.toupper");
 168     addOperator(api::STRING_REV, "str.rev");
 169     // sequence versions
 170     addOperator(api::SEQ_CONCAT, "seq.++");
 171     addOperator(api::SEQ_LENGTH, "seq.len");
 172     addOperator(api::SEQ_EXTRACT, "seq.extract");
 173     addOperator(api::SEQ_UPDATE, "seq.update");
 174     addOperator(api::SEQ_AT, "seq.at");
 175     addOperator(api::SEQ_CONTAINS, "seq.contains");
 176     addOperator(api::SEQ_INDEXOF, "seq.indexof");
 177     addOperator(api::SEQ_REPLACE, "seq.replace");
 178     addOperator(api::SEQ_PREFIX, "seq.prefixof");
 179     addOperator(api::SEQ_SUFFIX, "seq.suffixof");
 180     addOperator(api::SEQ_REV, "seq.rev");
 181     addOperator(api::SEQ_REPLACE_ALL, "seq.replace_all");
 182     addOperator(api::SEQ_UNIT, "seq.unit");
 183     addOperator(api::SEQ_NTH, "seq.nth");
 184   }
 185   // at the moment, we only use this syntax for smt2.6
 186   if (getLanguage() == language::input::LANG_SMTLIB_V2_6
 187       || getLanguage() == language::input::LANG_SYGUS_V2)
 188   {
 189     addOperator(api::STRING_FROM_INT, "str.from_int");
 190     addOperator(api::STRING_TO_INT, "str.to_int");
 191     addOperator(api::STRING_IN_REGEXP, "str.in_re");
 192     addOperator(api::STRING_TO_REGEXP, "str.to_re");
 193     addOperator(api::STRING_TO_CODE, "str.to_code");
 194     addOperator(api::STRING_REPLACE_ALL, "str.replace_all");
 195   }
 196   else
 197   {
 198     addOperator(api::STRING_FROM_INT, "int.to.str");
 199     addOperator(api::STRING_TO_INT, "str.to.int");
 200     addOperator(api::STRING_IN_REGEXP, "str.in.re");
 201     addOperator(api::STRING_TO_REGEXP, "str.to.re");
 202     addOperator(api::STRING_TO_CODE, "str.code");
 203     addOperator(api::STRING_REPLACE_ALL, "str.replaceall");
 204   }
 205
 206   addOperator(api::REGEXP_CONCAT, "re.++");
 207   addOperator(api::REGEXP_UNION, "re.union");
 208   addOperator(api::REGEXP_INTER, "re.inter");
 209   addOperator(api::REGEXP_STAR, "re.*");
 210   addOperator(api::REGEXP_PLUS, "re.+");
 211   addOperator(api::REGEXP_OPT, "re.opt");
 212   addIndexedOperator(api::REGEXP_REPEAT, api::REGEXP_REPEAT, "re.^");
 213   addIndexedOperator(api::REGEXP_LOOP, api::REGEXP_LOOP, "re.loop");
 214   addOperator(api::REGEXP_RANGE, "re.range");
 215   addOperator(api::REGEXP_COMPLEMENT, "re.comp");
 216   addOperator(api::REGEXP_DIFF, "re.diff");
 217   addOperator(api::STRING_LT, "str.<");
 218   addOperator(api::STRING_LEQ, "str.<=");
 219 }
 220
 221 void Smt2::addFloatingPointOperators() {
 222   addOperator(api::FLOATINGPOINT_FP, "fp");
 223   addOperator(api::FLOATINGPOINT_EQ, "fp.eq");
 224   addOperator(api::FLOATINGPOINT_ABS, "fp.abs");
 225   addOperator(api::FLOATINGPOINT_NEG, "fp.neg");
 226   addOperator(api::FLOATINGPOINT_PLUS, "fp.add");
 227   addOperator(api::FLOATINGPOINT_SUB, "fp.sub");
 228   addOperator(api::FLOATINGPOINT_MULT, "fp.mul");
 229   addOperator(api::FLOATINGPOINT_DIV, "fp.div");
 230   addOperator(api::FLOATINGPOINT_FMA, "fp.fma");
 231   addOperator(api::FLOATINGPOINT_SQRT, "fp.sqrt");
 232   addOperator(api::FLOATINGPOINT_REM, "fp.rem");
 233   addOperator(api::FLOATINGPOINT_RTI, "fp.roundToIntegral");
 234   addOperator(api::FLOATINGPOINT_MIN, "fp.min");
 235   addOperator(api::FLOATINGPOINT_MAX, "fp.max");
 236   addOperator(api::FLOATINGPOINT_LEQ, "fp.leq");
 237   addOperator(api::FLOATINGPOINT_LT, "fp.lt");
 238   addOperator(api::FLOATINGPOINT_GEQ, "fp.geq");
 239   addOperator(api::FLOATINGPOINT_GT, "fp.gt");
 240   addOperator(api::FLOATINGPOINT_ISN, "fp.isNormal");
 241   addOperator(api::FLOATINGPOINT_ISSN, "fp.isSubnormal");
 242   addOperator(api::FLOATINGPOINT_ISZ, "fp.isZero");
 243   addOperator(api::FLOATINGPOINT_ISINF, "fp.isInfinite");
 244   addOperator(api::FLOATINGPOINT_ISNAN, "fp.isNaN");
 245   addOperator(api::FLOATINGPOINT_ISNEG, "fp.isNegative");
 246   addOperator(api::FLOATINGPOINT_ISPOS, "fp.isPositive");
 247   addOperator(api::FLOATINGPOINT_TO_REAL, "fp.to_real");
 248
 249   addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC,
 250                      api::FLOATINGPOINT_TO_FP_GENERIC,
 251                      "to_fp");
 252   addIndexedOperator(api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
 253                      api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
 254                      "to_fp_unsigned");
 255   addIndexedOperator(
 256       api::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
 257   addIndexedOperator(
 258       api::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv");
 259
 260   if (!strictModeEnabled())
 261   {
 262     addIndexedOperator(api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
 263                        api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
 264                        "to_fp_bv");
 265     addIndexedOperator(api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
 266                        api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
 267                        "to_fp_fp");
 268     addIndexedOperator(api::FLOATINGPOINT_TO_FP_REAL,
 269                        api::FLOATINGPOINT_TO_FP_REAL,
 270                        "to_fp_real");
 271     addIndexedOperator(api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
 272                        api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
 273                        "to_fp_signed");
 274   }
 275 }
 276
 277 void Smt2::addSepOperators() {
 278   addOperator(api::SEP_STAR, "sep");
 279   addOperator(api::SEP_PTO, "pto");
 280   addOperator(api::SEP_WAND, "wand");
 281   addOperator(api::SEP_EMP, "emp");
 282   Parser::addOperator(api::SEP_STAR);
 283   Parser::addOperator(api::SEP_PTO);
 284   Parser::addOperator(api::SEP_WAND);
 285   Parser::addOperator(api::SEP_EMP);
 286 }
 287
 288 void Smt2::addCoreSymbols()
 289 {
 290   defineType("Bool", d_solver->getBooleanSort(), true, true);
 291   defineVar("true", d_solver->mkTrue(), true, true);
 292   defineVar("false", d_solver->mkFalse(), true, true);
 293   addOperator(api::AND, "and");
 294   addOperator(api::DISTINCT, "distinct");
 295   addOperator(api::EQUAL, "=");
 296   addOperator(api::IMPLIES, "=>");
 297   addOperator(api::ITE, "ite");
 298   addOperator(api::NOT, "not");
 299   addOperator(api::OR, "or");
 300   addOperator(api::XOR, "xor");
 301 }
 302
 303 void Smt2::addOperator(api::Kind kind, const std::string& name)
 304 {
 305   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 306                   << std::endl;
 307   Parser::addOperator(kind);
 308   operatorKindMap[name] = kind;
 309 }
 310
 311 void Smt2::addIndexedOperator(api::Kind tKind,
 312                               api::Kind opKind,
 313                               const std::string& name)
 314 {
 315   Parser::addOperator(tKind);
 316   d_indexedOpKindMap[name] = opKind;
 317 }
 318
 319 api::Kind Smt2::getOperatorKind(const std::string& name) const
 320 {
 321   // precondition: isOperatorEnabled(name)
 322   return operatorKindMap.find(name)->second;
 323 }
 324
 325 bool Smt2::isOperatorEnabled(const std::string& name) const {
 326   return operatorKindMap.find(name) != operatorKindMap.end();
 327 }
 328
 329 bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
 330 {
 331   return d_logic.isTheoryEnabled(theory);
 332 }
 333
 334 bool Smt2::isHoEnabled() const
 335 {
 336   return getLogic().isHigherOrder() && d_solver->getOptions().getUfHo();
 337 }
 338
 339 bool Smt2::logicIsSet() {
 340   return d_logicSet;
 341 }
 342
 343 api::Term Smt2::getExpressionForNameAndType(const std::string& name,
 344                                             api::Sort t)
 345 {
 346   if (isAbstractValue(name))
 347   {
 348     return mkAbstractValue(name);
 349   }
 350   return Parser::getExpressionForNameAndType(name, t);
 351 }
 352
 353 bool Smt2::getTesterName(api::Term cons, std::string& name)
 354 {
 355   if ((v2_6() || sygus_v2()) && strictModeEnabled())
 356   {
 357     // 2.6 or above uses indexed tester symbols, if we are in strict mode,
 358     // we do not automatically define is-cons for constructor cons.
 359     return false;
 360   }
 361   std::stringstream ss;
 362   ss << "is-" << cons;
 363   name = ss.str();
 364   return true;
 365 }
 366
 367 api::Term Smt2::mkIndexedConstant(const std::string& name,
 368                                   const std::vector<uint64_t>& numerals)
 369 {
 370   if (d_logic.isTheoryEnabled(theory::THEORY_FP))
 371   {
 372     if (name == "+oo")
 373     {
 374       return d_solver->mkPosInf(numerals[0], numerals[1]);
 375     }
 376     else if (name == "-oo")
 377     {
 378       return d_solver->mkNegInf(numerals[0], numerals[1]);
 379     }
 380     else if (name == "NaN")
 381     {
 382       return d_solver->mkNaN(numerals[0], numerals[1]);
 383     }
 384     else if (name == "+zero")
 385     {
 386       return d_solver->mkPosZero(numerals[0], numerals[1]);
 387     }
 388     else if (name == "-zero")
 389     {
 390       return d_solver->mkNegZero(numerals[0], numerals[1]);
 391     }
 392   }
 393
 394   if (d_logic.isTheoryEnabled(theory::THEORY_BV) && name.find("bv") == 0)
 395   {
 396     std::string bvStr = name.substr(2);
 397     return d_solver->mkBitVector(numerals[0], bvStr, 10);
 398   }
 399
 400   // NOTE: Theory parametric constants go here
 401
 402   parseError(std::string("Unknown indexed literal `") + name + "'");
 403   return api::Term();
 404 }
 405
 406 api::Op Smt2::mkIndexedOp(const std::string& name,
 407                           const std::vector<uint64_t>& numerals)
 408 {
 409   const auto& kIt = d_indexedOpKindMap.find(name);
 410   if (kIt != d_indexedOpKindMap.end())
 411   {
 412     api::Kind k = (*kIt).second;
 413     if (numerals.size() == 1)
 414     {
 415       return d_solver->mkOp(k, numerals[0]);
 416     }
 417     else if (numerals.size() == 2)
 418     {
 419       return d_solver->mkOp(k, numerals[0], numerals[1]);
 420     }
 421   }
 422
 423   parseError(std::string("Unknown indexed function `") + name + "'");
 424   return api::Op();
 425 }
 426
 427 api::Term Smt2::bindDefineFunRec(
 428     const std::string& fname,
 429     const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
 430     api::Sort t,
 431     std::vector<api::Term>& flattenVars)
 432 {
 433   std::vector<api::Sort> sorts;
 434   for (const std::pair<std::string, api::Sort>& svn : sortedVarNames)
 435   {
 436     sorts.push_back(svn.second);
 437   }
 438
 439   // make the flattened function type, add bound variables
 440   // to flattenVars if the defined function was given a function return type.
 441   api::Sort ft = mkFlatFunctionType(sorts, t, flattenVars);
 442
 443   // allow overloading
 444   return bindVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
 445 }
 446
 447 void Smt2::pushDefineFunRecScope(
 448     const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
 449     api::Term func,
 450     const std::vector<api::Term>& flattenVars,
 451     std::vector<api::Term>& bvs,
 452     bool bindingLevel)
 453 {
 454   pushScope(bindingLevel);
 455
 456   // bound variables are those that are explicitly named in the preamble
 457   // of the define-fun(s)-rec command, we define them here
 458   for (const std::pair<std::string, api::Sort>& svn : sortedVarNames)
 459   {
 460     api::Term v = bindBoundVar(svn.first, svn.second);
 461     bvs.push_back(v);
 462   }
 463
 464   bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end());
 465 }
 466
 467 void Smt2::reset() {
 468   d_logicSet = false;
 469   d_seenSetLogic = false;
 470   d_logic = LogicInfo();
 471   operatorKindMap.clear();
 472   d_lastNamedTerm = std::pair<api::Term, std::string>();
 473   this->Parser::reset();
 474   pushScope(true);
 475 }
 476
 477 void Smt2::resetAssertions() {
 478   // Remove all declarations except the ones at level 0.
 479   while (this->scopeLevel() > 0) {
 480     this->popScope();
 481   }
 482   pushScope(true);
 483 }
 484
 485 std::unique_ptr<Command> Smt2::invConstraint(
 486     const std::vector<std::string>& names)
 487 {
 488   checkThatLogicIsSet();
 489   Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
 490   Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
 491
 492   if (names.size() != 4)
 493   {
 494     parseError(
 495         "Bad syntax for inv-constraint: expected 4 "
 496         "arguments.");
 497   }
 498
 499   std::vector<api::Term> terms;
 500   for (const std::string& name : names)
 501   {
 502     if (!isDeclared(name))
 503     {
 504       std::stringstream ss;
 505       ss << "Function " << name << " in inv-constraint is not defined.";
 506       parseError(ss.str());
 507     }
 508
 509     terms.push_back(getVariable(name));
 510   }
 511
 512   return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms));
 513 }
 514
 515 Command* Smt2::setLogic(std::string name, bool fromCommand)
 516 {
 517   if (fromCommand)
 518   {
 519     if (d_seenSetLogic)
 520     {
 521       parseError("Only one set-logic is allowed.");
 522     }
 523     d_seenSetLogic = true;
 524
 525     if (logicIsForced())
 526     {
 527       // If the logic is forced, we ignore all set-logic requests from commands.
 528       return new EmptyCommand();
 529     }
 530   }
 531
 532   d_logicSet = true;
 533   d_logic = name;
 534
 535   // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
 536   // higher-order
 537   if(sygus()) {
 538     if (!d_logic.isQuantified())
 539     {
 540       warning("Logics in sygus are assumed to contain quantifiers.");
 541       warning("Omit QF_ from the logic to avoid this warning.");
 542     }
 543   }
 544
 545   // Core theory belongs to every logic
 546   addCoreSymbols();
 547
 548   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 549     Parser::addOperator(api::APPLY_UF);
 550
 551     if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
 552     {
 553       addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card");
 554       addOperator(api::CARDINALITY_VALUE, "fmf.card.val");
 555     }
 556   }
 557
 558   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 559     if(d_logic.areIntegersUsed()) {
 560       defineType("Int", d_solver->getIntegerSort(), true, true);
 561       addArithmeticOperators();
 562       addOperator(api::INTS_DIVISION, "div");
 563       addOperator(api::INTS_MODULUS, "mod");
 564       addOperator(api::ABS, "abs");
 565       addIndexedOperator(api::DIVISIBLE, api::DIVISIBLE, "divisible");
 566     }
 567
 568     if (d_logic.areRealsUsed())
 569     {
 570       defineType("Real", d_solver->getRealSort(), true, true);
 571       addArithmeticOperators();
 572       addOperator(api::DIVISION, "/");
 573       if (!strictModeEnabled())
 574       {
 575         addOperator(api::ABS, "abs");
 576       }
 577     }
 578
 579     if (d_logic.areIntegersUsed() && d_logic.areRealsUsed())
 580     {
 581       addOperator(api::TO_INTEGER, "to_int");
 582       addOperator(api::IS_INTEGER, "is_int");
 583       addOperator(api::TO_REAL, "to_real");
 584     }
 585
 586     if (d_logic.areTranscendentalsUsed())
 587     {
 588       defineVar("real.pi", d_solver->mkTerm(api::PI));
 589       addTranscendentalOperators();
 590     }
 591     if (!strictModeEnabled())
 592     {
 593       // integer version of AND
 594       addIndexedOperator(api::IAND, api::IAND, "iand");
 595     }
 596   }
 597
 598   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
 599     addOperator(api::SELECT, "select");
 600     addOperator(api::STORE, "store");
 601     addOperator(api::EQ_RANGE, "eqrange");
 602   }
 603
 604   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 605     addBitvectorOperators();
 606
 607     if (!strictModeEnabled() && d_logic.isTheoryEnabled(theory::THEORY_ARITH)
 608         && d_logic.areIntegersUsed())
 609     {
 610       // Conversions between bit-vectors and integers
 611       addOperator(api::BITVECTOR_TO_NAT, "bv2nat");
 612       addIndexedOperator(
 613           api::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv");
 614     }
 615   }
 616
 617   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
 618     const std::vector<api::Sort> types;
 619     defineType("Tuple", d_solver->mkTupleSort(types), true, true);
 620     addDatatypesOperators();
 621   }
 622
 623   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 624     defineVar("emptyset", d_solver->mkEmptySet(d_solver->getNullSort()));
 625     // the Boolean sort is a placeholder here since we don't have type info
 626     // without type annotation
 627     defineVar("univset", d_solver->mkUniverseSet(d_solver->getBooleanSort()));
 628
 629     addOperator(api::UNION, "union");
 630     addOperator(api::INTERSECTION, "intersection");
 631     addOperator(api::SETMINUS, "setminus");
 632     addOperator(api::SUBSET, "subset");
 633     addOperator(api::MEMBER, "member");
 634     addOperator(api::SINGLETON, "singleton");
 635     addOperator(api::INSERT, "insert");
 636     addOperator(api::CARD, "card");
 637     addOperator(api::COMPLEMENT, "complement");
 638     addOperator(api::CHOOSE, "choose");
 639     addOperator(api::IS_SINGLETON, "is_singleton");
 640     addOperator(api::JOIN, "join");
 641     addOperator(api::PRODUCT, "product");
 642     addOperator(api::TRANSPOSE, "transpose");
 643     addOperator(api::TCLOSURE, "tclosure");
 644   }
 645
 646   if (d_logic.isTheoryEnabled(theory::THEORY_BAGS))
 647   {
 648     defineVar("emptybag", d_solver->mkEmptyBag(d_solver->getNullSort()));
 649     addOperator(api::UNION_MAX, "union_max");
 650     addOperator(api::UNION_DISJOINT, "union_disjoint");
 651     addOperator(api::INTERSECTION_MIN, "intersection_min");
 652     addOperator(api::DIFFERENCE_SUBTRACT, "difference_subtract");
 653     addOperator(api::DIFFERENCE_REMOVE, "difference_remove");
 654     addOperator(api::SUBBAG, "bag.is_included");
 655     addOperator(api::BAG_COUNT, "bag.count");
 656     addOperator(api::DUPLICATE_REMOVAL, "duplicate_removal");
 657     addOperator(api::MK_BAG, "bag");
 658     addOperator(api::BAG_CARD, "bag.card");
 659     addOperator(api::BAG_CHOOSE, "bag.choose");
 660     addOperator(api::BAG_IS_SINGLETON, "bag.is_singleton");
 661     addOperator(api::BAG_FROM_SET, "bag.from_set");
 662     addOperator(api::BAG_TO_SET, "bag.to_set");
 663   }
 664   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 665     defineType("String", d_solver->getStringSort(), true, true);
 666     defineType("RegLan", d_solver->getRegExpSort(), true, true);
 667     defineType("Int", d_solver->getIntegerSort(), true, true);
 668
 669     if (getLanguage() == language::input::LANG_SMTLIB_V2_6
 670         || getLanguage() == language::input::LANG_SYGUS_V2)
 671     {
 672       defineVar("re.none", d_solver->mkRegexpEmpty());
 673     }
 674     else
 675     {
 676       defineVar("re.nostr", d_solver->mkRegexpEmpty());
 677     }
 678     defineVar("re.allchar", d_solver->mkRegexpSigma());
 679
 680     // Boolean is a placeholder
 681     defineVar("seq.empty",
 682               d_solver->mkEmptySequence(d_solver->getBooleanSort()));
 683
 684     addStringOperators();
 685   }
 686
 687   if(d_logic.isQuantified()) {
 688     addQuantifiersOperators();
 689   }
 690
 691   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
 692     defineType("RoundingMode", d_solver->getRoundingModeSort(), true, true);
 693     defineType("Float16", d_solver->mkFloatingPointSort(5, 11), true, true);
 694     defineType("Float32", d_solver->mkFloatingPointSort(8, 24), true, true);
 695     defineType("Float64", d_solver->mkFloatingPointSort(11, 53), true, true);
 696     defineType("Float128", d_solver->mkFloatingPointSort(15, 113), true, true);
 697
 698     defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN));
 699     defineVar("roundNearestTiesToEven",
 700               d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN));
 701     defineVar("RNA", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY));
 702     defineVar("roundNearestTiesToAway",
 703               d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY));
 704     defineVar("RTP", d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE));
 705     defineVar("roundTowardPositive",
 706               d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE));
 707     defineVar("RTN", d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE));
 708     defineVar("roundTowardNegative",
 709               d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE));
 710     defineVar("RTZ", d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO));
 711     defineVar("roundTowardZero",
 712               d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO));
 713
 714     addFloatingPointOperators();
 715   }
 716
 717   if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
 718     // the Boolean sort is a placeholder here since we don't have type info
 719     // without type annotation
 720     defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
 721
 722     addSepOperators();
 723   }
 724
 725   Command* cmd =
 726       new SetBenchmarkLogicCommand(sygus() ? d_logic.getLogicString() : name);
 727   cmd->setMuted(!fromCommand);
 728   return cmd;
 729 } /* Smt2::setLogic() */
 730
 731 api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars,
 732                               const std::vector<api::Term>& ntSymbols)
 733 {
 734   d_allocGrammars.emplace_back(
 735       new api::Grammar(d_solver->mkSygusGrammar(boundVars, ntSymbols)));
 736   return d_allocGrammars.back().get();
 737 }
 738
 739 bool Smt2::sygus() const
 740 {
 741   InputLanguage ilang = getLanguage();
 742   return ilang == language::input::LANG_SYGUS_V2;
 743 }
 744
 745 bool Smt2::sygus_v2() const
 746 {
 747   return getLanguage() == language::input::LANG_SYGUS_V2;
 748 }
 749
 750 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 751   // TODO: ???
 752 }
 753
 754 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 755   // TODO: ???
 756 }
 757
 758 void Smt2::checkThatLogicIsSet()
 759 {
 760   if (!logicIsSet())
 761   {
 762     if (strictModeEnabled())
 763     {
 764       parseError("set-logic must appear before this point.");
 765     }
 766     else
 767     {
 768       Command* cmd = nullptr;
 769       if (logicIsForced())
 770       {
 771         cmd = setLogic(getForcedLogic(), false);
 772       }
 773       else
 774       {
 775         warning("No set-logic command was given before this point.");
 776         warning("CVC4 will make all theories available.");
 777         warning(
 778             "Consider setting a stricter logic for (likely) better "
 779             "performance.");
 780         warning("To suppress this warning in the future use (set-logic ALL).");
 781
 782         cmd = setLogic("ALL", false);
 783       }
 784       preemptCommand(cmd);
 785     }
 786   }
 787 }
 788
 789 void Smt2::checkLogicAllowsFreeSorts()
 790 {
 791   if (!d_logic.isTheoryEnabled(theory::THEORY_UF)
 792       && !d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)
 793       && !d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)
 794       && !d_logic.isTheoryEnabled(theory::THEORY_SETS)
 795       && !d_logic.isTheoryEnabled(theory::THEORY_BAGS))
 796   {
 797     parseErrorLogic("Free sort symbols not allowed in ");
 798   }
 799 }
 800
 801 void Smt2::checkLogicAllowsFunctions()
 802 {
 803   if (!d_logic.isTheoryEnabled(theory::THEORY_UF))
 804   {
 805     parseError(
 806         "Functions (of non-zero arity) cannot "
 807         "be declared in logic "
 808         + d_logic.getLogicString() + " unless option --uf-ho is used");
 809   }
 810 }
 811
 812 /* The include are managed in the lexer but called in the parser */
 813 // Inspired by http://www.antlr3.org/api/C/interop.html
 814
 815 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 816   Debug("parser") << "Including " << filename << std::endl;
 817   // Create a new input stream and take advantage of built in stream stacking
 818   // in C target runtime.
 819   //
 820   pANTLR3_INPUT_STREAM    in;
 821 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 822   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 823 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 824   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 825 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 826   if( in == NULL ) {
 827     Debug("parser") << "Can't open " << filename << std::endl;
 828     return false;
 829   }
 830   // Same thing as the predefined PUSHSTREAM(in);
 831   lexer->pushCharStream(lexer, in);
 832   // restart it
 833   //lexer->rec->state->tokenStartCharIndex      = -10;
 834   //lexer->emit(lexer);
 835
 836   // Note that the input stream is not closed when it EOFs, I don't bother
 837   // to do it here, but it is up to you to track streams created like this
 838   // and destroy them when the whole parse session is complete. Remember that you
 839   // don't want to do this until all tokens have been manipulated all the way through
 840   // your tree parsers etc as the token does not store the text it just refers
 841   // back to the input stream and trying to get the text for it will abort if you
 842   // close the input stream too early.
 843
 844   //TODO what said before
 845   return true;
 846 }
 847
 848 void Smt2::includeFile(const std::string& filename) {
 849   // security for online version
 850   if(!canIncludeFile()) {
 851     parseError("include-file feature was disabled for this run.");
 852   }
 853
 854   // Get the lexer
 855   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 856   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 857   // get the name of the current stream "Does it work inside an include?"
 858   const std::string inputName = ai->getInputStreamName();
 859
 860   // Find the directory of the current input file
 861   std::string path;
 862   size_t pos = inputName.rfind('/');
 863   if(pos != std::string::npos) {
 864     path = std::string(inputName, 0, pos + 1);
 865   }
 866   path.append(filename);
 867   if(!newInputStream(path, lexer)) {
 868     parseError("Couldn't open include file `" + path + "'");
 869   }
 870 }
 871 bool Smt2::isAbstractValue(const std::string& name)
 872 {
 873   return name.length() >= 2 && name[0] == '@' && name[1] != '0'
 874          && name.find_first_not_of("0123456789", 1) == std::string::npos;
 875 }
 876
 877 api::Term Smt2::mkAbstractValue(const std::string& name)
 878 {
 879   assert(isAbstractValue(name));
 880   // remove the '@'
 881   return d_solver->mkAbstractValue(name.substr(1));
 882 }
 883
 884 InputLanguage Smt2::getLanguage() const
 885 {
 886   return d_solver->getOptions().getInputLanguage();
 887 }
 888
 889 void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
 890 {
 891   Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type
 892                   << std::endl;
 893   // (as const (Array T1 T2))
 894   if (p.d_kind == api::CONST_ARRAY)
 895   {
 896     if (!type.isArray())
 897     {
 898       std::stringstream ss;
 899       ss << "expected array constant term, but cast is not of array type"
 900          << std::endl
 901          << "cast type: " << type;
 902       parseError(ss.str());
 903     }
 904     p.d_type = type;
 905     return;
 906   }
 907   if (p.d_expr.isNull())
 908   {
 909     Trace("parser-overloading")
 910         << "Getting variable expression with name " << p.d_name << " and type "
 911         << type << std::endl;
 912     // get the variable expression for the type
 913     if (isDeclared(p.d_name, SYM_VARIABLE))
 914     {
 915       p.d_expr = getExpressionForNameAndType(p.d_name, type);
 916       p.d_name = std::string("");
 917     }
 918     if (p.d_expr.isNull())
 919     {
 920       std::stringstream ss;
 921       ss << "Could not resolve expression with name " << p.d_name
 922          << " and type " << type << std::endl;
 923       parseError(ss.str());
 924     }
 925   }
 926   Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr;
 927   Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getSort();
 928   Trace("parser-qid") << std::endl;
 929   // otherwise, we process the type ascription
 930   p.d_expr = applyTypeAscription(p.d_expr, type);
 931 }
 932
 933 api::Term Smt2::parseOpToExpr(ParseOp& p)
 934 {
 935   Debug("parser") << "parseOpToExpr: " << p << std::endl;
 936   api::Term expr;
 937   if (p.d_kind != api::NULL_EXPR || !p.d_type.isNull())
 938   {
 939     parseError(
 940         "Bad syntax for qualified identifier operator in term position.");
 941   }
 942   else if (!p.d_expr.isNull())
 943   {
 944     expr = p.d_expr;
 945   }
 946   else if (!isDeclared(p.d_name, SYM_VARIABLE))
 947   {
 948     std::stringstream ss;
 949     ss << "Symbol " << p.d_name << " is not declared.";
 950     parseError(ss.str());
 951   }
 952   else
 953   {
 954     expr = getExpressionForName(p.d_name);
 955   }
 956   assert(!expr.isNull());
 957   return expr;
 958 }
 959
 960 api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
 961 {
 962   bool isBuiltinOperator = false;
 963   // the builtin kind of the overall return expression
 964   api::Kind kind = api::NULL_EXPR;
 965   // First phase: process the operator
 966   if (Debug.isOn("parser"))
 967   {
 968     Debug("parser") << "applyParseOp: " << p << " to:" << std::endl;
 969     for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
 970          ++i)
 971     {
 972       Debug("parser") << "++ " << *i << std::endl;
 973     }
 974   }
 975   api::Op op;
 976   if (p.d_kind != api::NULL_EXPR)
 977   {
 978     // It is a special case, e.g. tupSel or array constant specification.
 979     // We have to wait until the arguments are parsed to resolve it.
 980   }
 981   else if (!p.d_expr.isNull())
 982   {
 983     // An explicit operator, e.g. an apply function
 984     api::Kind fkind = getKindForFunction(p.d_expr);
 985     if (fkind != api::UNDEFINED_KIND)
 986     {
 987       // Some operators may require a specific kind.
 988       // Testers are handled differently than other indexed operators,
 989       // since they require a kind.
 990       kind = fkind;
 991       Debug("parser") << "Got function kind " << kind << " for expression "
 992                       << std::endl;
 993     }
 994     args.insert(args.begin(), p.d_expr);
 995   }
 996   else if (!p.d_op.isNull())
 997   {
 998     // it was given an operator
 999     op = p.d_op;
1000   }
1001   else
1002   {
1003     isBuiltinOperator = isOperatorEnabled(p.d_name);
1004     if (isBuiltinOperator)
1005     {
1006       // a builtin operator, convert to kind
1007       kind = getOperatorKind(p.d_name);
1008     }
1009     else
1010     {
1011       // A non-built-in function application, get the expression
1012       checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE);
1013       api::Term v = getVariable(p.d_name);
1014       if (!v.isNull())
1015       {
1016         checkFunctionLike(v);
1017         kind = getKindForFunction(v);
1018         args.insert(args.begin(), v);
1019       }
1020       else
1021       {
1022         // Overloaded symbol?
1023         // Could not find the expression. It may be an overloaded symbol,
1024         // in which case we may find it after knowing the types of its
1025         // arguments.
1026         std::vector<api::Sort> argTypes;
1027         for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
1028              ++i)
1029         {
1030           argTypes.push_back((*i).getSort());
1031         }
1032         api::Term fop = getOverloadedFunctionForTypes(p.d_name, argTypes);
1033         if (!fop.isNull())
1034         {
1035           checkFunctionLike(fop);
1036           kind = getKindForFunction(fop);
1037           args.insert(args.begin(), fop);
1038         }
1039         else
1040         {
1041           parseError(
1042               "Cannot find unambiguous overloaded function for argument "
1043               "types.");
1044         }
1045       }
1046     }
1047   }
1048   // Second phase: apply the arguments to the parse op
1049   const Options& opts = d_solver->getOptions();
1050   // handle special cases
1051   if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull())
1052   {
1053     if (args.size() != 1)
1054     {
1055       parseError("Too many arguments to array constant.");
1056     }
1057     api::Term constVal = args[0];
1058
1059     // To parse array constants taking reals whose values are specified by
1060     // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
1061     // the fact that (/ 1 3) is the division of constants 1 and 3, and not
1062     // the resulting constant rational value. Thus, we must construct the
1063     // resulting rational here. This also is applied for integral real values
1064     // like 5.0 which are converted to (/ 5 1) to distinguish them from
1065     // integer constants. We must ensure numerator and denominator are
1066     // constant and the denominator is non-zero.
1067     if (constVal.getKind() == api::DIVISION)
1068     {
1069       std::stringstream sdiv;
1070       sdiv << constVal[0] << "/" << constVal[1];
1071       constVal = d_solver->mkReal(sdiv.str());
1072     }
1073
1074     if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort()))
1075     {
1076       std::stringstream ss;
1077       ss << "type mismatch inside array constant term:" << std::endl
1078          << "array type:          " << p.d_type << std::endl
1079          << "expected const type: " << p.d_type.getArrayElementSort()
1080          << std::endl
1081          << "computed const type: " << constVal.getSort();
1082       parseError(ss.str());
1083     }
1084     api::Term ret = d_solver->mkConstArray(p.d_type, constVal);
1085     Debug("parser") << "applyParseOp: return store all " << ret << std::endl;
1086     return ret;
1087   }
1088   else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull())
1089   {
1090     // tuple selector case
1091     Integer x = p.d_expr.getExpr().getConst<Rational>().getNumerator();
1092     if (!x.fitsUnsignedInt())
1093     {
1094       parseError("index of tupSel is larger than size of unsigned int");
1095     }
1096     unsigned int n = x.toUnsignedInt();
1097     if (args.size() != 1)
1098     {
1099       parseError("tupSel should only be applied to one tuple argument");
1100     }
1101     api::Sort t = args[0].getSort();
1102     if (!t.isTuple())
1103     {
1104       parseError("tupSel applied to non-tuple");
1105     }
1106     size_t length = t.getTupleLength();
1107     if (n >= length)
1108     {
1109       std::stringstream ss;
1110       ss << "tuple is of length " << length << "; cannot access index " << n;
1111       parseError(ss.str());
1112     }
1113     const api::Datatype& dt = t.getDatatype();
1114     api::Term ret = d_solver->mkTerm(
1115         api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]);
1116     Debug("parser") << "applyParseOp: return selector " << ret << std::endl;
1117     return ret;
1118   }
1119   else if (p.d_kind != api::NULL_EXPR)
1120   {
1121     // it should not have an expression or type specified at this point
1122     if (!p.d_expr.isNull() || !p.d_type.isNull())
1123     {
1124       std::stringstream ss;
1125       ss << "Could not process parsed qualified identifier kind " << p.d_kind;
1126       parseError(ss.str());
1127     }
1128     // otherwise it is a simple application
1129     kind = p.d_kind;
1130   }
1131   else if (isBuiltinOperator)
1132   {
1133     if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
1134     {
1135       // need --uf-ho if these operators are applied over function args
1136       for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
1137            ++i)
1138       {
1139         if ((*i).getSort().isFunction())
1140         {
1141           parseError(
1142               "Cannot apply equalty to functions unless --uf-ho is set.");
1143         }
1144       }
1145     }
1146     if (!strictModeEnabled() && (kind == api::AND || kind == api::OR)
1147         && args.size() == 1)
1148     {
1149       // Unary AND/OR can be replaced with the argument.
1150       Debug("parser") << "applyParseOp: return unary " << args[0] << std::endl;
1151       return args[0];
1152     }
1153     else if (kind == api::MINUS && args.size() == 1)
1154     {
1155       api::Term ret = d_solver->mkTerm(api::UMINUS, args[0]);
1156       Debug("parser") << "applyParseOp: return uminus " << ret << std::endl;
1157       return ret;
1158     }
1159     if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true")
1160     {
1161       parseError(
1162           "eqrange predicate requires option --arrays-exp to be enabled.");
1163     }
1164     if (kind == api::SINGLETON && args.size() == 1)
1165     {
1166       api::Term ret = d_solver->mkTerm(api::SINGLETON, args[0]);
1167       Debug("parser") << "applyParseOp: return singleton " << ret << std::endl;
1168       return ret;
1169     }
1170     api::Term ret = d_solver->mkTerm(kind, args);
1171     Debug("parser") << "applyParseOp: return default builtin " << ret
1172                     << std::endl;
1173     return ret;
1174   }
1175
1176   if (args.size() >= 2)
1177   {
1178     // may be partially applied function, in this case we use HO_APPLY
1179     api::Sort argt = args[0].getSort();
1180     if (argt.isFunction())
1181     {
1182       unsigned arity = argt.getFunctionArity();
1183       if (args.size() - 1 < arity)
1184       {
1185         if (!opts.getUfHo())
1186         {
1187           parseError("Cannot partially apply functions unless --uf-ho is set.");
1188         }
1189         Debug("parser") << "Partial application of " << args[0];
1190         Debug("parser") << " : #argTypes = " << arity;
1191         Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
1192         api::Term ret = d_solver->mkTerm(api::HO_APPLY, args);
1193         Debug("parser") << "applyParseOp: return curry higher order " << ret
1194                         << std::endl;
1195         // must curry the partial application
1196         return ret;
1197       }
1198     }
1199   }
1200   if (!op.isNull())
1201   {
1202     api::Term ret = d_solver->mkTerm(op, args);
1203     Debug("parser") << "applyParseOp: return op : " << ret << std::endl;
1204     return ret;
1205   }
1206   if (kind == api::NULL_EXPR)
1207   {
1208     // should never happen in the new API
1209     parseError("do not know how to process parse op");
1210   }
1211   Debug("parser") << "Try default term construction for kind " << kind
1212                   << " #args = " << args.size() << "..." << std::endl;
1213   api::Term ret = d_solver->mkTerm(kind, args);
1214   Debug("parser") << "applyParseOp: return : " << ret << std::endl;
1215   return ret;
1216 }
1217
1218 api::Term Smt2::setNamedAttribute(api::Term& expr, const SExpr& sexpr)
1219 {
1220   if (!sexpr.isKeyword())
1221   {
1222     parseError("improperly formed :named annotation");
1223   }
1224   std::string name = sexpr.getValue();
1225   checkUserSymbol(name);
1226   // ensure expr is a closed subterm
1227   if (expr.getExpr().hasFreeVariable())
1228   {
1229     std::stringstream ss;
1230     ss << ":named annotations can only name terms that are closed";
1231     parseError(ss.str());
1232   }
1233   // check that sexpr is a fresh function symbol, and reserve it
1234   reserveSymbolAtAssertionLevel(name);
1235   // define it
1236   api::Term func = bindVar(name, expr.getSort(), ExprManager::VAR_FLAG_DEFINED);
1237   // remember the last term to have been given a :named attribute
1238   setLastNamedTerm(expr, name);
1239   return func;
1240 }
1241
1242 api::Term Smt2::mkAnd(const std::vector<api::Term>& es)
1243 {
1244   if (es.size() == 0)
1245   {
1246     return d_solver->mkTrue();
1247   }
1248   else if (es.size() == 1)
1249   {
1250     return es[0];
1251   }
1252   else
1253   {
1254     return d_solver->mkTerm(api::AND, es);
1255   }
1256 }
1257
1258 }  // namespace parser
1259 }/* CVC4 namespace */