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