src/parser/smt2/smt2.cpp

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