src/parser/smt2/smt2.cpp

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