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