src/parser/smt2/smt2.cpp

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