src/parser/smt2/smt2.cpp

   1 /*********************                                                        */
   2 /*! \file smt2.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Kshitij Bansal, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 "printer/sygus_print_callback.h"
  27 #include "util/bitvector.h"
  28
  29 // ANTLR defines these, which is really bad!
  30 #undef true
  31 #undef false
  32
  33 namespace CVC4 {
  34 namespace parser {
  35
  36 Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
  37     : Parser(solver, input, strictMode, parseOnly),
  38       d_logicSet(false),
  39       d_seenSetLogic(false)
  40 {
  41   if (!strictModeEnabled())
  42   {
  43     addTheory(Smt2::THEORY_CORE);
  44   }
  45 }
  46
  47 void Smt2::addArithmeticOperators() {
  48   addOperator(kind::PLUS, "+");
  49   addOperator(kind::MINUS, "-");
  50   // kind::MINUS is converted to kind::UMINUS if there is only a single operand
  51   Parser::addOperator(kind::UMINUS);
  52   addOperator(kind::MULT, "*");
  53   addOperator(kind::LT, "<");
  54   addOperator(kind::LEQ, "<=");
  55   addOperator(kind::GT, ">");
  56   addOperator(kind::GEQ, ">=");
  57
  58   if (!strictModeEnabled())
  59   {
  60     // NOTE: this operator is non-standard
  61     addOperator(kind::POW, "^");
  62   }
  63 }
  64
  65 void Smt2::addTranscendentalOperators()
  66 {
  67   addOperator(kind::EXPONENTIAL, "exp");
  68   addOperator(kind::SINE, "sin");
  69   addOperator(kind::COSINE, "cos");
  70   addOperator(kind::TANGENT, "tan");
  71   addOperator(kind::COSECANT, "csc");
  72   addOperator(kind::SECANT, "sec");
  73   addOperator(kind::COTANGENT, "cot");
  74   addOperator(kind::ARCSINE, "arcsin");
  75   addOperator(kind::ARCCOSINE, "arccos");
  76   addOperator(kind::ARCTANGENT, "arctan");
  77   addOperator(kind::ARCCOSECANT, "arccsc");
  78   addOperator(kind::ARCSECANT, "arcsec");
  79   addOperator(kind::ARCCOTANGENT, "arccot");
  80   addOperator(kind::SQRT, "sqrt");
  81 }
  82
  83 void Smt2::addQuantifiersOperators()
  84 {
  85   if (!strictModeEnabled())
  86   {
  87     addOperator(kind::INST_CLOSURE, "inst-closure");
  88   }
  89 }
  90
  91 void Smt2::addBitvectorOperators() {
  92   addOperator(kind::BITVECTOR_CONCAT, "concat");
  93   addOperator(kind::BITVECTOR_NOT, "bvnot");
  94   addOperator(kind::BITVECTOR_AND, "bvand");
  95   addOperator(kind::BITVECTOR_OR, "bvor");
  96   addOperator(kind::BITVECTOR_NEG, "bvneg");
  97   addOperator(kind::BITVECTOR_PLUS, "bvadd");
  98   addOperator(kind::BITVECTOR_MULT, "bvmul");
  99   addOperator(kind::BITVECTOR_UDIV, "bvudiv");
 100   addOperator(kind::BITVECTOR_UREM, "bvurem");
 101   addOperator(kind::BITVECTOR_SHL, "bvshl");
 102   addOperator(kind::BITVECTOR_LSHR, "bvlshr");
 103   addOperator(kind::BITVECTOR_ULT, "bvult");
 104   addOperator(kind::BITVECTOR_NAND, "bvnand");
 105   addOperator(kind::BITVECTOR_NOR, "bvnor");
 106   addOperator(kind::BITVECTOR_XOR, "bvxor");
 107   addOperator(kind::BITVECTOR_XNOR, "bvxnor");
 108   addOperator(kind::BITVECTOR_COMP, "bvcomp");
 109   addOperator(kind::BITVECTOR_SUB, "bvsub");
 110   addOperator(kind::BITVECTOR_SDIV, "bvsdiv");
 111   addOperator(kind::BITVECTOR_SREM, "bvsrem");
 112   addOperator(kind::BITVECTOR_SMOD, "bvsmod");
 113   addOperator(kind::BITVECTOR_ASHR, "bvashr");
 114   addOperator(kind::BITVECTOR_ULE, "bvule");
 115   addOperator(kind::BITVECTOR_UGT, "bvugt");
 116   addOperator(kind::BITVECTOR_UGE, "bvuge");
 117   addOperator(kind::BITVECTOR_SLT, "bvslt");
 118   addOperator(kind::BITVECTOR_SLE, "bvsle");
 119   addOperator(kind::BITVECTOR_SGT, "bvsgt");
 120   addOperator(kind::BITVECTOR_SGE, "bvsge");
 121   addOperator(kind::BITVECTOR_REDOR, "bvredor");
 122   addOperator(kind::BITVECTOR_REDAND, "bvredand");
 123   addOperator(kind::BITVECTOR_TO_NAT, "bv2nat");
 124
 125   addIndexedOperator(
 126       kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract");
 127   addIndexedOperator(kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat");
 128   addIndexedOperator(
 129       kind::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend");
 130   addIndexedOperator(
 131       kind::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend");
 132   addIndexedOperator(
 133       kind::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left");
 134   addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT,
 135                      api::BITVECTOR_ROTATE_RIGHT,
 136                      "rotate_right");
 137   addIndexedOperator(kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv");
 138 }
 139
 140 void Smt2::addDatatypesOperators()
 141 {
 142   Parser::addOperator(kind::APPLY_CONSTRUCTOR);
 143   Parser::addOperator(kind::APPLY_TESTER);
 144   Parser::addOperator(kind::APPLY_SELECTOR);
 145   Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
 146
 147   if (!strictModeEnabled())
 148   {
 149     addOperator(kind::DT_SIZE, "dt.size");
 150   }
 151 }
 152
 153 void Smt2::addStringOperators() {
 154   defineVar("re.all",
 155             getSolver()
 156                 ->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())
 157                 .getExpr());
 158
 159   addOperator(kind::STRING_CONCAT, "str.++");
 160   addOperator(kind::STRING_LENGTH, "str.len");
 161   addOperator(kind::STRING_SUBSTR, "str.substr" );
 162   addOperator(kind::STRING_STRCTN, "str.contains" );
 163   addOperator(kind::STRING_CHARAT, "str.at" );
 164   addOperator(kind::STRING_STRIDOF, "str.indexof" );
 165   addOperator(kind::STRING_STRREPL, "str.replace" );
 166   addOperator(kind::STRING_STRREPLALL, "str.replaceall");
 167   if (!strictModeEnabled())
 168   {
 169     addOperator(kind::STRING_TOLOWER, "str.tolower");
 170     addOperator(kind::STRING_TOUPPER, "str.toupper");
 171     addOperator(kind::STRING_REV, "str.rev");
 172   }
 173   addOperator(kind::STRING_PREFIX, "str.prefixof" );
 174   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
 175   // at the moment, we only use this syntax for smt2.6.1
 176   if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
 177   {
 178     addOperator(kind::STRING_ITOS, "str.from-int");
 179     addOperator(kind::STRING_STOI, "str.to-int");
 180     addOperator(kind::STRING_IN_REGEXP, "str.in-re");
 181     addOperator(kind::STRING_TO_REGEXP, "str.to-re");
 182   }
 183   else
 184   {
 185     addOperator(kind::STRING_ITOS, "int.to.str");
 186     addOperator(kind::STRING_STOI, "str.to.int");
 187     addOperator(kind::STRING_IN_REGEXP, "str.in.re");
 188     addOperator(kind::STRING_TO_REGEXP, "str.to.re");
 189   }
 190
 191   addOperator(kind::REGEXP_CONCAT, "re.++");
 192   addOperator(kind::REGEXP_UNION, "re.union");
 193   addOperator(kind::REGEXP_INTER, "re.inter");
 194   addOperator(kind::REGEXP_STAR, "re.*");
 195   addOperator(kind::REGEXP_PLUS, "re.+");
 196   addOperator(kind::REGEXP_OPT, "re.opt");
 197   addOperator(kind::REGEXP_RANGE, "re.range");
 198   addOperator(kind::REGEXP_LOOP, "re.loop");
 199   addOperator(kind::STRING_CODE, "str.code");
 200   addOperator(kind::STRING_LT, "str.<");
 201   addOperator(kind::STRING_LEQ, "str.<=");
 202 }
 203
 204 void Smt2::addFloatingPointOperators() {
 205   addOperator(kind::FLOATINGPOINT_FP, "fp");
 206   addOperator(kind::FLOATINGPOINT_EQ, "fp.eq");
 207   addOperator(kind::FLOATINGPOINT_ABS, "fp.abs");
 208   addOperator(kind::FLOATINGPOINT_NEG, "fp.neg");
 209   addOperator(kind::FLOATINGPOINT_PLUS, "fp.add");
 210   addOperator(kind::FLOATINGPOINT_SUB, "fp.sub");
 211   addOperator(kind::FLOATINGPOINT_MULT, "fp.mul");
 212   addOperator(kind::FLOATINGPOINT_DIV, "fp.div");
 213   addOperator(kind::FLOATINGPOINT_FMA, "fp.fma");
 214   addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt");
 215   addOperator(kind::FLOATINGPOINT_REM, "fp.rem");
 216   addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral");
 217   addOperator(kind::FLOATINGPOINT_MIN, "fp.min");
 218   addOperator(kind::FLOATINGPOINT_MAX, "fp.max");
 219   addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq");
 220   addOperator(kind::FLOATINGPOINT_LT, "fp.lt");
 221   addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq");
 222   addOperator(kind::FLOATINGPOINT_GT, "fp.gt");
 223   addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal");
 224   addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal");
 225   addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero");
 226   addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite");
 227   addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN");
 228   addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative");
 229   addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
 230   addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
 231
 232   addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC,
 233                      api::FLOATINGPOINT_TO_FP_GENERIC,
 234                      "to_fp");
 235   addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
 236                      api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
 237                      "to_fp_unsigned");
 238   addIndexedOperator(
 239       kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
 240   addIndexedOperator(
 241       kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv");
 242
 243   if (!strictModeEnabled())
 244   {
 245     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
 246                        api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
 247                        "to_fp_bv");
 248     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
 249                        api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
 250                        "to_fp_fp");
 251     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL,
 252                        api::FLOATINGPOINT_TO_FP_REAL,
 253                        "to_fp_real");
 254     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
 255                        api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
 256                        "to_fp_signed");
 257   }
 258 }
 259
 260 void Smt2::addSepOperators() {
 261   addOperator(kind::SEP_STAR, "sep");
 262   addOperator(kind::SEP_PTO, "pto");
 263   addOperator(kind::SEP_WAND, "wand");
 264   addOperator(kind::SEP_EMP, "emp");
 265   Parser::addOperator(kind::SEP_STAR);
 266   Parser::addOperator(kind::SEP_PTO);
 267   Parser::addOperator(kind::SEP_WAND);
 268   Parser::addOperator(kind::SEP_EMP);
 269 }
 270
 271 void Smt2::addTheory(Theory theory) {
 272   switch(theory) {
 273   case THEORY_ARRAYS:
 274     addOperator(kind::SELECT, "select");
 275     addOperator(kind::STORE, "store");
 276     break;
 277
 278   case THEORY_BITVECTORS:
 279     addBitvectorOperators();
 280     break;
 281
 282   case THEORY_CORE:
 283     defineType("Bool", getExprManager()->booleanType());
 284     defineVar("true", getExprManager()->mkConst(true));
 285     defineVar("false", getExprManager()->mkConst(false));
 286     addOperator(kind::AND, "and");
 287     addOperator(kind::DISTINCT, "distinct");
 288     addOperator(kind::EQUAL, "=");
 289     addOperator(kind::IMPLIES, "=>");
 290     addOperator(kind::ITE, "ite");
 291     addOperator(kind::NOT, "not");
 292     addOperator(kind::OR, "or");
 293     addOperator(kind::XOR, "xor");
 294     break;
 295
 296   case THEORY_REALS_INTS:
 297     defineType("Real", getExprManager()->realType());
 298     addOperator(kind::DIVISION, "/");
 299     addOperator(kind::TO_INTEGER, "to_int");
 300     addOperator(kind::IS_INTEGER, "is_int");
 301     addOperator(kind::TO_REAL, "to_real");
 302     // falling through on purpose, to add Ints part of Reals_Ints
 303     CVC4_FALLTHROUGH;
 304   case THEORY_INTS:
 305     defineType("Int", getExprManager()->integerType());
 306     addArithmeticOperators();
 307     addOperator(kind::INTS_DIVISION, "div");
 308     addOperator(kind::INTS_MODULUS, "mod");
 309     addOperator(kind::ABS, "abs");
 310     addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE, "divisible");
 311     break;
 312
 313   case THEORY_REALS:
 314     defineType("Real", getExprManager()->realType());
 315     addArithmeticOperators();
 316     addOperator(kind::DIVISION, "/");
 317     if (!strictModeEnabled())
 318     {
 319       addOperator(kind::ABS, "abs");
 320     }
 321     break;
 322
 323   case THEORY_TRANSCENDENTALS:
 324     defineVar("real.pi",
 325               getExprManager()->mkNullaryOperator(getExprManager()->realType(),
 326                                                   CVC4::kind::PI));
 327     addTranscendentalOperators();
 328     break;
 329
 330   case THEORY_QUANTIFIERS: addQuantifiersOperators(); break;
 331
 332   case THEORY_SETS:
 333     defineVar("emptyset",
 334               d_solver->mkEmptySet(d_solver->getNullSort()).getExpr());
 335     // the Boolean sort is a placeholder here since we don't have type info
 336     // without type annotation
 337     defineVar("univset",
 338               d_solver->mkUniverseSet(d_solver->getBooleanSort()).getExpr());
 339
 340     addOperator(kind::UNION, "union");
 341     addOperator(kind::INTERSECTION, "intersection");
 342     addOperator(kind::SETMINUS, "setminus");
 343     addOperator(kind::SUBSET, "subset");
 344     addOperator(kind::MEMBER, "member");
 345     addOperator(kind::SINGLETON, "singleton");
 346     addOperator(kind::INSERT, "insert");
 347     addOperator(kind::CARD, "card");
 348     addOperator(kind::COMPLEMENT, "complement");
 349     addOperator(kind::JOIN, "join");
 350     addOperator(kind::PRODUCT, "product");
 351     addOperator(kind::TRANSPOSE, "transpose");
 352     addOperator(kind::TCLOSURE, "tclosure");
 353     break;
 354
 355   case THEORY_DATATYPES:
 356   {
 357     const std::vector<Type> types;
 358     defineType("Tuple", getExprManager()->mkTupleType(types));
 359     addDatatypesOperators();
 360     break;
 361   }
 362
 363   case THEORY_STRINGS:
 364     defineType("String", getExprManager()->stringType());
 365     defineType("RegLan", getExprManager()->regExpType());
 366     defineType("Int", getExprManager()->integerType());
 367
 368     defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr());
 369     defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr());
 370
 371     addStringOperators();
 372     break;
 373
 374   case THEORY_UF:
 375     Parser::addOperator(kind::APPLY_UF);
 376
 377     if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
 378     {
 379       addOperator(kind::CARDINALITY_CONSTRAINT, "fmf.card");
 380       addOperator(kind::CARDINALITY_VALUE, "fmf.card.val");
 381     }
 382     break;
 383
 384   case THEORY_FP:
 385     defineType("RoundingMode", getExprManager()->roundingModeType());
 386     defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
 387     defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
 388     defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
 389     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
 390
 391     defineVar(
 392         "RNE",
 393         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
 394     defineVar(
 395         "roundNearestTiesToEven",
 396         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
 397     defineVar(
 398         "RNA",
 399         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
 400     defineVar(
 401         "roundNearestTiesToAway",
 402         d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
 403     defineVar("RTP",
 404               d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
 405     defineVar("roundTowardPositive",
 406               d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
 407     defineVar("RTN",
 408               d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
 409     defineVar("roundTowardNegative",
 410               d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
 411     defineVar("RTZ",
 412               d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
 413     defineVar("roundTowardZero",
 414               d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
 415
 416     addFloatingPointOperators();
 417     break;
 418
 419   case THEORY_SEP:
 420     // the Boolean sort is a placeholder here since we don't have type info
 421     // without type annotation
 422     defineVar("sep.nil",
 423               d_solver->mkSepNil(d_solver->getBooleanSort()).getExpr());
 424
 425     addSepOperators();
 426     break;
 427
 428   default:
 429     std::stringstream ss;
 430     ss << "internal error: unsupported theory " << theory;
 431     throw ParserException(ss.str());
 432   }
 433 }
 434
 435 void Smt2::addOperator(Kind kind, const std::string& name) {
 436   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 437                   << std::endl;
 438   Parser::addOperator(kind);
 439   operatorKindMap[name] = kind;
 440 }
 441
 442 void Smt2::addIndexedOperator(Kind tKind,
 443                               api::Kind opKind,
 444                               const std::string& name)
 445 {
 446   Parser::addOperator(tKind);
 447   d_indexedOpKindMap[name] = opKind;
 448 }
 449
 450 Kind Smt2::getOperatorKind(const std::string& name) const {
 451   // precondition: isOperatorEnabled(name)
 452   return operatorKindMap.find(name)->second;
 453 }
 454
 455 bool Smt2::isOperatorEnabled(const std::string& name) const {
 456   return operatorKindMap.find(name) != operatorKindMap.end();
 457 }
 458
 459 bool Smt2::isTheoryEnabled(Theory theory) const {
 460   switch(theory) {
 461   case THEORY_ARRAYS:
 462     return d_logic.isTheoryEnabled(theory::THEORY_ARRAYS);
 463   case THEORY_BITVECTORS:
 464     return d_logic.isTheoryEnabled(theory::THEORY_BV);
 465   case THEORY_CORE:
 466     return true;
 467   case THEORY_DATATYPES:
 468     return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
 469   case THEORY_INTS:
 470     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 471       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
 472   case THEORY_REALS:
 473     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 474       ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
 475   case THEORY_REALS_INTS:
 476     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 477       d_logic.areIntegersUsed() && d_logic.areRealsUsed();
 478   case THEORY_QUANTIFIERS:
 479     return d_logic.isQuantified();
 480   case THEORY_SETS:
 481     return d_logic.isTheoryEnabled(theory::THEORY_SETS);
 482   case THEORY_STRINGS:
 483     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
 484   case THEORY_UF:
 485     return d_logic.isTheoryEnabled(theory::THEORY_UF);
 486   case THEORY_FP:
 487     return d_logic.isTheoryEnabled(theory::THEORY_FP);
 488   case THEORY_SEP:
 489     return d_logic.isTheoryEnabled(theory::THEORY_SEP);
 490   default:
 491     std::stringstream ss;
 492     ss << "internal error: unsupported theory " << theory;
 493     throw ParserException(ss.str());
 494   }
 495 }
 496
 497 bool Smt2::logicIsSet() {
 498   return d_logicSet;
 499 }
 500
 501 Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
 502   if (isAbstractValue(name))
 503   {
 504     return mkAbstractValue(name);
 505   }
 506   return Parser::getExpressionForNameAndType(name, t);
 507 }
 508
 509 api::Term Smt2::mkIndexedConstant(const std::string& name,
 510                                   const std::vector<uint64_t>& numerals)
 511 {
 512   if (isTheoryEnabled(THEORY_FP))
 513   {
 514     if (name == "+oo")
 515     {
 516       return d_solver->mkPosInf(numerals[0], numerals[1]);
 517     }
 518     else if (name == "-oo")
 519     {
 520       return d_solver->mkNegInf(numerals[0], numerals[1]);
 521     }
 522     else if (name == "NaN")
 523     {
 524       return d_solver->mkNaN(numerals[0], numerals[1]);
 525     }
 526     else if (name == "+zero")
 527     {
 528       return d_solver->mkPosZero(numerals[0], numerals[1]);
 529     }
 530     else if (name == "-zero")
 531     {
 532       return d_solver->mkNegZero(numerals[0], numerals[1]);
 533     }
 534   }
 535
 536   if (isTheoryEnabled(THEORY_BITVECTORS) && name.find("bv") == 0)
 537   {
 538     std::string bvStr = name.substr(2);
 539     return d_solver->mkBitVector(numerals[0], bvStr, 10);
 540   }
 541
 542   // NOTE: Theory parametric constants go here
 543
 544   parseError(std::string("Unknown indexed literal `") + name + "'");
 545   return api::Term();
 546 }
 547
 548 api::Op Smt2::mkIndexedOp(const std::string& name,
 549                           const std::vector<uint64_t>& numerals)
 550 {
 551   const auto& kIt = d_indexedOpKindMap.find(name);
 552   if (kIt != d_indexedOpKindMap.end())
 553   {
 554     api::Kind k = (*kIt).second;
 555     if (numerals.size() == 1)
 556     {
 557       return d_solver->mkOp(k, numerals[0]);
 558     }
 559     else if (numerals.size() == 2)
 560     {
 561       return d_solver->mkOp(k, numerals[0], numerals[1]);
 562     }
 563   }
 564
 565   parseError(std::string("Unknown indexed function `") + name + "'");
 566   return api::Op();
 567 }
 568
 569 Expr Smt2::mkDefineFunRec(
 570     const std::string& fname,
 571     const std::vector<std::pair<std::string, Type> >& sortedVarNames,
 572     Type t,
 573     std::vector<Expr>& flattenVars)
 574 {
 575   std::vector<Type> sorts;
 576   for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
 577   {
 578     sorts.push_back(svn.second);
 579   }
 580
 581   // make the flattened function type, add bound variables
 582   // to flattenVars if the defined function was given a function return type.
 583   Type ft = mkFlatFunctionType(sorts, t, flattenVars);
 584
 585   // allow overloading
 586   return mkVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
 587 }
 588
 589 void Smt2::pushDefineFunRecScope(
 590     const std::vector<std::pair<std::string, Type> >& sortedVarNames,
 591     Expr func,
 592     const std::vector<Expr>& flattenVars,
 593     std::vector<Expr>& bvs,
 594     bool bindingLevel)
 595 {
 596   pushScope(bindingLevel);
 597
 598   // bound variables are those that are explicitly named in the preamble
 599   // of the define-fun(s)-rec command, we define them here
 600   for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
 601   {
 602     Expr v = mkBoundVar(svn.first, svn.second);
 603     bvs.push_back(v);
 604   }
 605
 606   bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end());
 607 }
 608
 609 void Smt2::reset() {
 610   d_logicSet = false;
 611   d_seenSetLogic = false;
 612   d_logic = LogicInfo();
 613   operatorKindMap.clear();
 614   d_lastNamedTerm = std::pair<Expr, std::string>();
 615   this->Parser::reset();
 616
 617   if( !strictModeEnabled() ) {
 618     addTheory(Smt2::THEORY_CORE);
 619   }
 620 }
 621
 622 void Smt2::resetAssertions() {
 623   // Remove all declarations except the ones at level 0.
 624   while (this->scopeLevel() > 0) {
 625     this->popScope();
 626   }
 627 }
 628
 629 std::unique_ptr<Command> Smt2::assertRewriteRule(
 630     Kind kind,
 631     Expr bvl,
 632     const std::vector<Expr>& triggers,
 633     const std::vector<Expr>& guards,
 634     const std::vector<Expr>& heads,
 635     Expr body)
 636 {
 637   assert(kind == kind::RR_REWRITE || kind == kind::RR_REDUCTION
 638          || kind == kind::RR_DEDUCTION);
 639
 640   ExprManager* em = getExprManager();
 641
 642   std::vector<Expr> args;
 643   args.push_back(mkAnd(heads));
 644   args.push_back(body);
 645
 646   if (!triggers.empty())
 647   {
 648     args.push_back(em->mkExpr(kind::INST_PATTERN_LIST, triggers));
 649   }
 650
 651   Expr rhs = em->mkExpr(kind, args);
 652   Expr rule = em->mkExpr(kind::REWRITE_RULE, bvl, mkAnd(guards), rhs);
 653   return std::unique_ptr<Command>(new AssertCommand(rule, false));
 654 }
 655
 656 Smt2::SynthFunFactory::SynthFunFactory(
 657     Smt2* smt2,
 658     const std::string& fun,
 659     bool isInv,
 660     Type range,
 661     std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames)
 662     : d_smt2(smt2), d_fun(fun), d_isInv(isInv)
 663 {
 664   if (range.isNull())
 665   {
 666     smt2->parseError("Must supply return type for synth-fun.");
 667   }
 668   if (range.isFunction())
 669   {
 670     smt2->parseError("Cannot use synth-fun with function return type.");
 671   }
 672   std::vector<Type> varSorts;
 673   for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
 674   {
 675     varSorts.push_back(p.second);
 676   }
 677   Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
 678   Type synthFunType =
 679       varSorts.size() > 0
 680           ? d_smt2->getExprManager()->mkFunctionType(varSorts, range)
 681           : range;
 682
 683   // we do not allow overloading for synth fun
 684   d_synthFun = d_smt2->mkBoundVar(fun, synthFunType);
 685   // set the sygus type to be range by default, which is overwritten below
 686   // if a grammar is provided
 687   d_sygusType = range;
 688
 689   d_smt2->pushScope(true);
 690   d_sygusVars = d_smt2->mkBoundVars(sortedVarNames);
 691 }
 692
 693 Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); }
 694
 695 std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(Type grammar)
 696 {
 697   Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl;
 698   return std::unique_ptr<Command>(
 699       new SynthFunCommand(d_fun,
 700                           d_synthFun,
 701                           grammar.isNull() ? d_sygusType : grammar,
 702                           d_isInv,
 703                           d_sygusVars));
 704 }
 705
 706 std::unique_ptr<Command> Smt2::invConstraint(
 707     const std::vector<std::string>& names)
 708 {
 709   checkThatLogicIsSet();
 710   Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
 711   Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
 712
 713   if (names.size() != 4)
 714   {
 715     parseError(
 716         "Bad syntax for inv-constraint: expected 4 "
 717         "arguments.");
 718   }
 719
 720   std::vector<Expr> terms;
 721   for (const std::string& name : names)
 722   {
 723     if (!isDeclared(name))
 724     {
 725       std::stringstream ss;
 726       ss << "Function " << name << " in inv-constraint is not defined.";
 727       parseError(ss.str());
 728     }
 729
 730     terms.push_back(getVariable(name));
 731   }
 732
 733   return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms));
 734 }
 735
 736 Command* Smt2::setLogic(std::string name, bool fromCommand)
 737 {
 738   if (fromCommand)
 739   {
 740     if (d_seenSetLogic)
 741     {
 742       parseError("Only one set-logic is allowed.");
 743     }
 744     d_seenSetLogic = true;
 745
 746     if (logicIsForced())
 747     {
 748       // If the logic is forced, we ignore all set-logic requests from commands.
 749       return new EmptyCommand();
 750     }
 751   }
 752
 753   if (sygus_v1())
 754   {
 755     // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2)
 756     if(name == "Arrays") {
 757       name = "A";
 758     }else if(name == "Reals") {
 759       name = "LRA";
 760     }
 761   }
 762
 763   d_logicSet = true;
 764   d_logic = name;
 765
 766   // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
 767   // higher-order
 768   if(sygus()) {
 769     if (!d_logic.isQuantified())
 770     {
 771       warning("Logics in sygus are assumed to contain quantifiers.");
 772       warning("Omit QF_ from the logic to avoid this warning.");
 773     }
 774     // get unlocked copy, modify, copy and relock
 775     LogicInfo log(d_logic.getUnlockedCopy());
 776     // enable everything needed for sygus
 777     log.enableSygus();
 778     d_logic = log;
 779     d_logic.lock();
 780   }
 781
 782   // Core theory belongs to every logic
 783   addTheory(THEORY_CORE);
 784
 785   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 786     addTheory(THEORY_UF);
 787   }
 788
 789   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 790     if(d_logic.areIntegersUsed()) {
 791       if(d_logic.areRealsUsed()) {
 792         addTheory(THEORY_REALS_INTS);
 793       } else {
 794         addTheory(THEORY_INTS);
 795       }
 796     } else if(d_logic.areRealsUsed()) {
 797       addTheory(THEORY_REALS);
 798     }
 799
 800     if (d_logic.areTranscendentalsUsed())
 801     {
 802       addTheory(THEORY_TRANSCENDENTALS);
 803     }
 804   }
 805
 806   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
 807     addTheory(THEORY_ARRAYS);
 808   }
 809
 810   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 811     addTheory(THEORY_BITVECTORS);
 812   }
 813
 814   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
 815     addTheory(THEORY_DATATYPES);
 816   }
 817
 818   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 819     addTheory(THEORY_SETS);
 820   }
 821
 822   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 823     addTheory(THEORY_STRINGS);
 824   }
 825
 826   if(d_logic.isQuantified()) {
 827     addTheory(THEORY_QUANTIFIERS);
 828   }
 829
 830   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
 831     addTheory(THEORY_FP);
 832   }
 833
 834   if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
 835     addTheory(THEORY_SEP);
 836   }
 837
 838   Command* cmd =
 839       new SetBenchmarkLogicCommand(sygus() ? d_logic.getLogicString() : name);
 840   cmd->setMuted(!fromCommand);
 841   return cmd;
 842 } /* Smt2::setLogic() */
 843
 844 bool Smt2::sygus() const
 845 {
 846   InputLanguage ilang = getLanguage();
 847   return ilang == language::input::LANG_SYGUS
 848          || ilang == language::input::LANG_SYGUS_V2;
 849 }
 850 bool Smt2::sygus_v1() const
 851 {
 852   return getLanguage() == language::input::LANG_SYGUS;
 853 }
 854
 855 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 856   // TODO: ???
 857 }
 858
 859 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 860   // TODO: ???
 861 }
 862
 863 void Smt2::checkThatLogicIsSet()
 864 {
 865   if (!logicIsSet())
 866   {
 867     if (strictModeEnabled())
 868     {
 869       parseError("set-logic must appear before this point.");
 870     }
 871     else
 872     {
 873       Command* cmd = nullptr;
 874       if (logicIsForced())
 875       {
 876         cmd = setLogic(getForcedLogic(), false);
 877       }
 878       else
 879       {
 880         warning("No set-logic command was given before this point.");
 881         warning("CVC4 will make all theories available.");
 882         warning(
 883             "Consider setting a stricter logic for (likely) better "
 884             "performance.");
 885         warning("To suppress this warning in the future use (set-logic ALL).");
 886
 887         cmd = setLogic("ALL", false);
 888       }
 889       preemptCommand(cmd);
 890     }
 891   }
 892 }
 893
 894 /* The include are managed in the lexer but called in the parser */
 895 // Inspired by http://www.antlr3.org/api/C/interop.html
 896
 897 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 898   Debug("parser") << "Including " << filename << std::endl;
 899   // Create a new input stream and take advantage of built in stream stacking
 900   // in C target runtime.
 901   //
 902   pANTLR3_INPUT_STREAM    in;
 903 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 904   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 905 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 906   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 907 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 908   if( in == NULL ) {
 909     Debug("parser") << "Can't open " << filename << std::endl;
 910     return false;
 911   }
 912   // Same thing as the predefined PUSHSTREAM(in);
 913   lexer->pushCharStream(lexer, in);
 914   // restart it
 915   //lexer->rec->state->tokenStartCharIndex      = -10;
 916   //lexer->emit(lexer);
 917
 918   // Note that the input stream is not closed when it EOFs, I don't bother
 919   // to do it here, but it is up to you to track streams created like this
 920   // and destroy them when the whole parse session is complete. Remember that you
 921   // don't want to do this until all tokens have been manipulated all the way through
 922   // your tree parsers etc as the token does not store the text it just refers
 923   // back to the input stream and trying to get the text for it will abort if you
 924   // close the input stream too early.
 925
 926   //TODO what said before
 927   return true;
 928 }
 929
 930 void Smt2::includeFile(const std::string& filename) {
 931   // security for online version
 932   if(!canIncludeFile()) {
 933     parseError("include-file feature was disabled for this run.");
 934   }
 935
 936   // Get the lexer
 937   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 938   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 939   // get the name of the current stream "Does it work inside an include?"
 940   const std::string inputName = ai->getInputStreamName();
 941
 942   // Find the directory of the current input file
 943   std::string path;
 944   size_t pos = inputName.rfind('/');
 945   if(pos != std::string::npos) {
 946     path = std::string(inputName, 0, pos + 1);
 947   }
 948   path.append(filename);
 949   if(!newInputStream(path, lexer)) {
 950     parseError("Couldn't open include file `" + path + "'");
 951   }
 952 }
 953
 954 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
 955   if( type.isInteger() ){
 956     ops.push_back(getExprManager()->mkConst(Rational(0)));
 957     ops.push_back(getExprManager()->mkConst(Rational(1)));
 958   }else if( type.isBitVector() ){
 959     unsigned sz = ((BitVectorType)type).getSize();
 960     BitVector bval0(sz, (unsigned int)0);
 961     ops.push_back( getExprManager()->mkConst(bval0) );
 962     BitVector bval1(sz, (unsigned int)1);
 963     ops.push_back( getExprManager()->mkConst(bval1) );
 964   }else if( type.isBoolean() ){
 965     ops.push_back(getExprManager()->mkConst(true));
 966     ops.push_back(getExprManager()->mkConst(false));
 967   }
 968   //TODO : others?
 969 }
 970
 971 //  This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
 972 //  This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
 973 void Smt2::processSygusGTerm(
 974     CVC4::SygusGTerm& sgt,
 975     int index,
 976     std::vector<CVC4::Datatype>& datatypes,
 977     std::vector<CVC4::Type>& sorts,
 978     std::vector<std::vector<ParseOp>>& ops,
 979     std::vector<std::vector<std::string>>& cnames,
 980     std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
 981     std::vector<bool>& allow_const,
 982     std::vector<std::vector<std::string>>& unresolved_gterm_sym,
 983     const std::vector<CVC4::Expr>& sygus_vars,
 984     std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
 985     std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
 986     CVC4::Type& ret,
 987     bool isNested)
 988 {
 989   if (sgt.d_gterm_type == SygusGTerm::gterm_op)
 990   {
 991     Debug("parser-sygus") << "Add " << sgt.d_op << " to datatype "
 992                           << index << std::endl;
 993     Kind oldKind;
 994     Kind newKind = kind::UNDEFINED_KIND;
 995     //convert to UMINUS if one child of MINUS
 996     if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == kind::MINUS)
 997     {
 998       oldKind = kind::MINUS;
 999       newKind = kind::UMINUS;
1000     }
1001     if( newKind!=kind::UNDEFINED_KIND ){
1002       Debug("parser-sygus")
1003           << "Replace " << sgt.d_op.d_kind << " with " << newKind << std::endl;
1004       sgt.d_op.d_kind = newKind;
1005       std::string oldName = kind::kindToString(oldKind);
1006       std::string newName = kind::kindToString(newKind);
1007       size_t pos = 0;
1008       if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){
1009         sgt.d_name.replace(pos, oldName.length(), newName);
1010       }
1011     }
1012     ops[index].push_back(sgt.d_op);
1013     cnames[index].push_back( sgt.d_name );
1014     cargs[index].push_back( std::vector< CVC4::Type >() );
1015     for( unsigned i=0; i<sgt.d_children.size(); i++ ){
1016       std::stringstream ss;
1017       ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
1018       std::string sub_dname = ss.str();
1019       //add datatype for child
1020       Type null_type;
1021       pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
1022       int sub_dt_index = datatypes.size()-1;
1023       //process child
1024       Type sub_ret;
1025       processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
1026                          sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
1027       //process the nested gterm (either pop the last datatype, or flatten the argument)
1028       Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
1029                                          sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
1030       cargs[index].back().push_back(tt);
1031     }
1032   }
1033   else if (sgt.d_gterm_type == SygusGTerm::gterm_constant)
1034   {
1035     if( sgt.getNumChildren()!=0 ){
1036       parseError("Bad syntax for Sygus Constant.");
1037     }
1038     std::vector< Expr > consts;
1039     mkSygusConstantsForType( sgt.d_type, consts );
1040     Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
1041     for( unsigned i=0; i<consts.size(); i++ ){
1042       std::stringstream ss;
1043       ss << consts[i];
1044       Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
1045       ParseOp constOp;
1046       constOp.d_expr = consts[i];
1047       ops[index].push_back(constOp);
1048       cnames[index].push_back( ss.str() );
1049       cargs[index].push_back( std::vector< CVC4::Type >() );
1050     }
1051     allow_const[index] = true;
1052   }
1053   else if (sgt.d_gterm_type == SygusGTerm::gterm_variable
1054            || sgt.d_gterm_type == SygusGTerm::gterm_input_variable)
1055   {
1056     if( sgt.getNumChildren()!=0 ){
1057       parseError("Bad syntax for Sygus Variable.");
1058     }
1059     Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
1060     for( unsigned i=0; i<sygus_vars.size(); i++ ){
1061       if( sygus_vars[i].getType()==sgt.d_type ){
1062         std::stringstream ss;
1063         ss << sygus_vars[i];
1064         Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
1065         ParseOp varOp;
1066         varOp.d_expr = sygus_vars[i];
1067         ops[index].push_back(varOp);
1068         cnames[index].push_back( ss.str() );
1069         cargs[index].push_back( std::vector< CVC4::Type >() );
1070       }
1071     }
1072   }
1073   else if (sgt.d_gterm_type == SygusGTerm::gterm_nested_sort)
1074   {
1075     ret = sgt.d_type;
1076   }
1077   else if (sgt.d_gterm_type == SygusGTerm::gterm_unresolved)
1078   {
1079     if( isNested ){
1080       if( isUnresolvedType(sgt.d_name) ){
1081         ret = getSort(sgt.d_name);
1082       }else{
1083         //nested, unresolved symbol...fail
1084         std::stringstream ss;
1085         ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl;
1086         parseError(ss.str());
1087       }
1088     }else{
1089       //will resolve when adding constructors
1090       unresolved_gterm_sym[index].push_back(sgt.d_name);
1091     }
1092   }
1093   else if (sgt.d_gterm_type == SygusGTerm::gterm_ignore)
1094   {
1095     // do nothing
1096   }
1097 }
1098
1099 bool Smt2::pushSygusDatatypeDef(
1100     Type t,
1101     std::string& dname,
1102     std::vector<CVC4::Datatype>& datatypes,
1103     std::vector<CVC4::Type>& sorts,
1104     std::vector<std::vector<ParseOp>>& ops,
1105     std::vector<std::vector<std::string>>& cnames,
1106     std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
1107     std::vector<bool>& allow_const,
1108     std::vector<std::vector<std::string>>& unresolved_gterm_sym)
1109 {
1110   sorts.push_back(t);
1111   datatypes.push_back(Datatype(getExprManager(), dname));
1112   ops.push_back(std::vector<ParseOp>());
1113   cnames.push_back(std::vector<std::string>());
1114   cargs.push_back(std::vector<std::vector<CVC4::Type> >());
1115   allow_const.push_back(false);
1116   unresolved_gterm_sym.push_back(std::vector< std::string >());
1117   return true;
1118 }
1119
1120 bool Smt2::popSygusDatatypeDef(
1121     std::vector<CVC4::Datatype>& datatypes,
1122     std::vector<CVC4::Type>& sorts,
1123     std::vector<std::vector<ParseOp>>& ops,
1124     std::vector<std::vector<std::string>>& cnames,
1125     std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
1126     std::vector<bool>& allow_const,
1127     std::vector<std::vector<std::string>>& unresolved_gterm_sym)
1128 {
1129   sorts.pop_back();
1130   datatypes.pop_back();
1131   ops.pop_back();
1132   cnames.pop_back();
1133   cargs.pop_back();
1134   allow_const.pop_back();
1135   unresolved_gterm_sym.pop_back();
1136   return true;
1137 }
1138
1139 Type Smt2::processSygusNestedGTerm(
1140     int sub_dt_index,
1141     std::string& sub_dname,
1142     std::vector<CVC4::Datatype>& datatypes,
1143     std::vector<CVC4::Type>& sorts,
1144     std::vector<std::vector<ParseOp>>& ops,
1145     std::vector<std::vector<std::string>>& cnames,
1146     std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
1147     std::vector<bool>& allow_const,
1148     std::vector<std::vector<std::string>>& unresolved_gterm_sym,
1149     std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
1150     std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
1151     Type sub_ret)
1152 {
1153   Type t = sub_ret;
1154   Debug("parser-sygus") << "Argument is ";
1155   if( t.isNull() ){
1156     //then, it is the datatype we constructed, which should have a single constructor
1157     t = mkUnresolvedType(sub_dname);
1158     Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t << std::endl;
1159     Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs[sub_dt_index].size() << std::endl;
1160     if( cargs[sub_dt_index].empty() ){
1161       parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
1162     }
1163     ParseOp op = ops[sub_dt_index][0];
1164     Type curr_t;
1165     if (!op.d_expr.isNull()
1166         && (op.d_expr.isConst() || cargs[sub_dt_index][0].empty()))
1167     {
1168       Expr sop = op.d_expr;
1169       curr_t = sop.getType();
1170       Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl;
1171       // only cache if it is a singleton datatype (has unique expr)
1172       if (ops[sub_dt_index].size() == 1)
1173       {
1174         sygus_to_builtin_expr[t] = sop;
1175         // store that term sop has dedicated sygus type t
1176         if (d_sygus_bound_var_type.find(sop) == d_sygus_bound_var_type.end())
1177         {
1178           d_sygus_bound_var_type[sop] = t;
1179         }
1180       }
1181     }
1182     else
1183     {
1184       std::vector< Expr > children;
1185       for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
1186         std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
1187         if( it==sygus_to_builtin_expr.end() ){
1188           if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){
1189             std::stringstream ss;
1190             ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl;
1191             ss << "Builtin types are currently : " << std::endl;
1192             for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){
1193               ss << "  " << itb->first << " -> " << itb->second << std::endl;
1194             }
1195             parseError(ss.str());
1196           }
1197           Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
1198           Debug("parser-sygus") << ":  child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
1199           std::stringstream ss;
1200           ss << t << "_x_" << i;
1201           Expr bv = mkBoundVar(ss.str(), bt);
1202           children.push_back( bv );
1203           d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i];
1204         }else{
1205           Debug("parser-sygus") << ":  child " << i << " existing sygus to builtin expr : " << it->second << std::endl;
1206           children.push_back( it->second );
1207         }
1208       }
1209       Expr e = applyParseOp(op, children);
1210       Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
1211       curr_t = e.getType();
1212       sygus_to_builtin_expr[t] = e;
1213     }
1214     sorts[sub_dt_index] = curr_t;
1215     sygus_to_builtin[t] = curr_t;
1216   }else{
1217     Debug("parser-sygus") << "simple argument " << t << std::endl;
1218     Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl;
1219     //otherwise, datatype was unecessary
1220     //pop argument datatype definition
1221     popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
1222   }
1223   return t;
1224 }
1225
1226 void Smt2::setSygusStartIndex(const std::string& fun,
1227                               int startIndex,
1228                               std::vector<CVC4::Datatype>& datatypes,
1229                               std::vector<CVC4::Type>& sorts,
1230                               std::vector<std::vector<ParseOp>>& ops)
1231 {
1232   if( startIndex>0 ){
1233     CVC4::Datatype tmp_dt = datatypes[0];
1234     Type tmp_sort = sorts[0];
1235     std::vector<ParseOp> tmp_ops;
1236     tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
1237     datatypes[0] = datatypes[startIndex];
1238     sorts[0] = sorts[startIndex];
1239     ops[0].clear();
1240     ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
1241     datatypes[startIndex] = tmp_dt;
1242     sorts[startIndex] = tmp_sort;
1243     ops[startIndex].clear();
1244     ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
1245   }else if( startIndex<0 ){
1246     std::stringstream ss;
1247     ss << "warning: no symbol named Start for synth-fun " << fun << std::endl;
1248     warning(ss.str());
1249   }
1250 }
1251
1252 void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
1253                            std::vector<ParseOp>& ops,
1254                            std::vector<std::string>& cnames,
1255                            std::vector<std::vector<CVC4::Type>>& cargs,
1256                            std::vector<std::string>& unresolved_gterm_sym,
1257                            std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin)
1258 {
1259   Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
1260   Debug("parser-sygus") << "  add constructors..." << std::endl;
1261
1262   Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl;
1263   Debug("parser-sygus") << "  add constructors..." << std::endl;
1264   // size of cnames changes, this loop must check size
1265   for (unsigned i = 0; i < cnames.size(); i++)
1266   {
1267     bool is_dup = false;
1268     bool is_dup_op = false;
1269     for (unsigned j = 0; j < i; j++)
1270     {
1271       if( ops[i]==ops[j] ){
1272         is_dup_op = true;
1273         if( cargs[i].size()==cargs[j].size() ){
1274           is_dup = true;
1275           for( unsigned k=0; k<cargs[i].size(); k++ ){
1276             if( cargs[i][k]!=cargs[j][k] ){
1277               is_dup = false;
1278               break;
1279             }
1280           }
1281         }
1282         if( is_dup ){
1283           break;
1284         }
1285       }
1286     }
1287     Debug("parser-sygus") << "SYGUS CONS " << i << " : ";
1288     if( is_dup ){
1289       Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl;
1290       ops.erase( ops.begin() + i, ops.begin() + i + 1 );
1291       cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 );
1292       cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 );
1293       i--;
1294     }
1295     else
1296     {
1297       std::shared_ptr<SygusPrintCallback> spc;
1298       if (is_dup_op)
1299       {
1300         Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i]
1301                               << std::endl;
1302         // make into define-fun
1303         std::vector<Type> ltypes;
1304         for (unsigned j = 0, size = cargs[i].size(); j < size; j++)
1305         {
1306           ltypes.push_back(sygus_to_builtin[cargs[i][j]]);
1307         }
1308         std::vector<Expr> largs;
1309         Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
1310
1311         // make the let_body
1312         Expr body = applyParseOp(ops[i], largs);
1313         // replace by lambda
1314         ParseOp pLam;
1315         pLam.d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
1316         ops[i] = pLam;
1317         Debug("parser-sygus") << "  ...replace op : " << ops[i] << std::endl;
1318         // callback prints as the expression
1319         spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs);
1320       }
1321       else
1322       {
1323         Expr sop = ops[i].d_expr;
1324         if (!sop.isNull() && sop.getType().isBitVector() && sop.isConst())
1325         {
1326           Debug("parser-sygus") << "--> Bit-vector constant " << sop << " ("
1327                                 << cnames[i] << ")" << std::endl;
1328           // Since there are multiple output formats for bit-vectors and
1329           // we are required by sygus standards to print in the exact input
1330           // format given by the user, we use a print callback to custom print
1331           // the given name.
1332           spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
1333         }
1334         else if (!sop.isNull() && sop.getKind() == kind::VARIABLE)
1335         {
1336           Debug("parser-sygus") << "--> Defined function " << ops[i]
1337                                 << std::endl;
1338           // turn f into (lammbda (x) (f x))
1339           // in a degenerate case, ops[i] may be a defined constant,
1340           // in which case we do not replace by a lambda.
1341           if (sop.getType().isFunction())
1342           {
1343             std::vector<Type> ftypes =
1344                 static_cast<FunctionType>(sop.getType()).getArgTypes();
1345             std::vector<Expr> largs;
1346             Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
1347             largs.insert(largs.begin(), sop);
1348             Expr body = getExprManager()->mkExpr(kind::APPLY_UF, largs);
1349             ops[i].d_expr = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
1350             Debug("parser-sygus") << "  ...replace op : " << ops[i]
1351                                   << std::endl;
1352           }
1353           else
1354           {
1355             Debug("parser-sygus") << "  ...replace op : " << ops[i]
1356                                   << std::endl;
1357           }
1358           // keep a callback to say it should be printed with the defined name
1359           spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
1360         }
1361         else
1362         {
1363           Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl;
1364         }
1365       }
1366       // must rename to avoid duplication
1367       std::stringstream ss;
1368       ss << dt.getName() << "_" << i << "_" << cnames[i];
1369       cnames[i] = ss.str();
1370       Debug("parser-sygus") << "  construct the datatype " << cnames[i] << "..."
1371                             << std::endl;
1372       // Add the sygus constructor, either using the expression operator of
1373       // ops[i], or the kind.
1374       if (!ops[i].d_expr.isNull())
1375       {
1376         dt.addSygusConstructor(ops[i].d_expr, cnames[i], cargs[i], spc);
1377       }
1378       else if (ops[i].d_kind != kind::NULL_EXPR)
1379       {
1380         dt.addSygusConstructor(ops[i].d_kind, cnames[i], cargs[i], spc);
1381       }
1382       else
1383       {
1384         std::stringstream ss;
1385         ss << "unexpected parse operator for sygus constructor" << ops[i];
1386         parseError(ss.str());
1387       }
1388       Debug("parser-sygus") << "  finished constructing the datatype"
1389                             << std::endl;
1390     }
1391   }
1392
1393   Debug("parser-sygus") << "  add constructors for unresolved symbols..." << std::endl;
1394   if( !unresolved_gterm_sym.empty() ){
1395     std::vector< Type > types;
1396     Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl;
1397     for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){
1398       Debug("parser-sygus") << "  resolve : " << unresolved_gterm_sym[i] << std::endl;
1399       if( isUnresolvedType(unresolved_gterm_sym[i]) ){
1400         Debug("parser-sygus") << "    it is an unresolved type." << std::endl;
1401         Type t = getSort(unresolved_gterm_sym[i]);
1402         if( std::find( types.begin(), types.end(), t )==types.end() ){
1403           types.push_back( t );
1404           //identity element
1405           Type bt = dt.getSygusType();
1406           Debug("parser-sygus") << ":  make identity function for " << bt << ", argument type " << t << std::endl;
1407
1408           std::stringstream ss;
1409           ss << t << "_x";
1410           Expr var = mkBoundVar(ss.str(), bt);
1411           std::vector<Expr> lchildren;
1412           lchildren.push_back(
1413               getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var));
1414           lchildren.push_back(var);
1415           Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren);
1416
1417           // empty sygus callback (should not be printed)
1418           std::shared_ptr<SygusPrintCallback> sepc =
1419               std::make_shared<printer::SygusEmptyPrintCallback>();
1420
1421           //make the sygus argument list
1422           std::vector< Type > id_carg;
1423           id_carg.push_back( t );
1424           dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc);
1425
1426           //add to operators
1427           ParseOp idOp;
1428           idOp.d_expr = id_op;
1429           ops.push_back(idOp);
1430         }
1431       }else{
1432         std::stringstream ss;
1433         ss << "Unhandled sygus constructor " << unresolved_gterm_sym[i];
1434         throw ParserException(ss.str());
1435       }
1436     }
1437   }
1438 }
1439
1440 Expr Smt2::makeSygusBoundVarList(Datatype& dt,
1441                                  unsigned i,
1442                                  const std::vector<Type>& ltypes,
1443                                  std::vector<Expr>& lvars)
1444 {
1445   for (unsigned j = 0, size = ltypes.size(); j < size; j++)
1446   {
1447     std::stringstream ss;
1448     ss << dt.getName() << "_x_" << i << "_" << j;
1449     Expr v = mkBoundVar(ss.str(), ltypes[j]);
1450     lvars.push_back(v);
1451   }
1452   return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
1453 }
1454
1455 void Smt2::addSygusConstructorTerm(Datatype& dt,
1456                                    Expr term,
1457                                    std::map<Expr, Type>& ntsToUnres) const
1458 {
1459   Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl;
1460   // Ensure that we do type checking here to catch sygus constructors with
1461   // malformed builtin operators. The argument "true" to getType here forces
1462   // a recursive well-typedness check.
1463   term.getType(true);
1464   // purify each occurrence of a non-terminal symbol in term, replace by
1465   // free variables. These become arguments to constructors. Notice we must do
1466   // a tree traversal in this function, since unique paths to the same term
1467   // should be treated as distinct terms.
1468   // Notice that let expressions are forbidden in the input syntax of term, so
1469   // this does not lead to exponential behavior with respect to input size.
1470   std::vector<Expr> args;
1471   std::vector<Type> cargs;
1472   Expr op = purifySygusGTerm(term, ntsToUnres, args, cargs);
1473   Trace("parser-sygus2") << "Purified operator " << op
1474                          << ", #args/cargs=" << args.size() << "/"
1475                          << cargs.size() << std::endl;
1476   std::shared_ptr<SygusPrintCallback> spc;
1477   // callback prints as the expression
1478   spc = std::make_shared<printer::SygusExprPrintCallback>(op, args);
1479   if (!args.empty())
1480   {
1481     bool pureVar = false;
1482     if (op.getNumChildren() == args.size())
1483     {
1484       pureVar = true;
1485       for (unsigned i = 0, nchild = op.getNumChildren(); i < nchild; i++)
1486       {
1487         if (op[i] != args[i])
1488         {
1489           pureVar = false;
1490           break;
1491         }
1492       }
1493     }
1494     Trace("parser-sygus2") << "Pure var is " << pureVar
1495                            << ", hasOp=" << op.hasOperator() << std::endl;
1496     if (pureVar && op.hasOperator())
1497     {
1498       // optimization: use just the operator if it an application to only vars
1499       op = op.getOperator();
1500     }
1501     else
1502     {
1503       Expr lbvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, args);
1504       // its operator is a lambda
1505       op = getExprManager()->mkExpr(kind::LAMBDA, lbvl, op);
1506     }
1507   }
1508   Trace("parser-sygus2") << "Generated operator " << op << std::endl;
1509   std::stringstream ss;
1510   ss << op.getKind();
1511   dt.addSygusConstructor(op, ss.str(), cargs, spc);
1512 }
1513
1514 Expr Smt2::purifySygusGTerm(Expr term,
1515                             std::map<Expr, Type>& ntsToUnres,
1516                             std::vector<Expr>& args,
1517                             std::vector<Type>& cargs) const
1518 {
1519   Trace("parser-sygus2-debug")
1520       << "purifySygusGTerm: " << term << " #nchild=" << term.getNumChildren()
1521       << std::endl;
1522   std::map<Expr, Type>::iterator itn = ntsToUnres.find(term);
1523   if (itn != ntsToUnres.end())
1524   {
1525     Expr ret = getExprManager()->mkBoundVar(term.getType());
1526     Trace("parser-sygus2-debug")
1527         << "...unresolved non-terminal, intro " << ret << std::endl;
1528     args.push_back(ret);
1529     cargs.push_back(itn->second);
1530     return ret;
1531   }
1532   std::vector<Expr> pchildren;
1533   // To test whether the operator should be passed to mkExpr below, we check
1534   // whether this term is parameterized. This includes APPLY_UF terms and BV
1535   // extraction terms, but excludes applications of most interpreted symbols
1536   // like PLUS.
1537   if (term.isParameterized())
1538   {
1539     pchildren.push_back(term.getOperator());
1540   }
1541   bool childChanged = false;
1542   for (unsigned i = 0, nchild = term.getNumChildren(); i < nchild; i++)
1543   {
1544     Trace("parser-sygus2-debug")
1545         << "......purify child " << i << " : " << term[i] << std::endl;
1546     Expr ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs);
1547     pchildren.push_back(ptermc);
1548     childChanged = childChanged || ptermc != term[i];
1549   }
1550   if (!childChanged)
1551   {
1552     Trace("parser-sygus2-debug") << "...no child changed" << std::endl;
1553     return term;
1554   }
1555   Expr nret = getExprManager()->mkExpr(term.getKind(), pchildren);
1556   Trace("parser-sygus2-debug")
1557       << "...child changed, return " << nret << std::endl;
1558   return nret;
1559 }
1560
1561 void Smt2::addSygusConstructorVariables(Datatype& dt,
1562                                         const std::vector<Expr>& sygusVars,
1563                                         Type type) const
1564 {
1565   // each variable of appropriate type becomes a sygus constructor in dt.
1566   for (unsigned i = 0, size = sygusVars.size(); i < size; i++)
1567   {
1568     Expr v = sygusVars[i];
1569     if (v.getType() == type)
1570     {
1571       std::stringstream ss;
1572       ss << v;
1573       std::vector<CVC4::Type> cargs;
1574       dt.addSygusConstructor(v, ss.str(), cargs);
1575     }
1576   }
1577 }
1578
1579 InputLanguage Smt2::getLanguage() const
1580 {
1581   ExprManager* em = getExprManager();
1582   return em->getOptions().getInputLanguage();
1583 }
1584
1585 void Smt2::applyTypeAscription(ParseOp& p, Type type)
1586 {
1587   // (as const (Array T1 T2))
1588   if (p.d_kind == kind::STORE_ALL)
1589   {
1590     if (!type.isArray())
1591     {
1592       std::stringstream ss;
1593       ss << "expected array constant term, but cast is not of array type"
1594          << std::endl
1595          << "cast type: " << type;
1596       parseError(ss.str());
1597     }
1598     p.d_type = type;
1599     return;
1600   }
1601   if (p.d_expr.isNull())
1602   {
1603     Trace("parser-overloading")
1604         << "Getting variable expression with name " << p.d_name << " and type "
1605         << type << std::endl;
1606     // get the variable expression for the type
1607     if (isDeclared(p.d_name, SYM_VARIABLE))
1608     {
1609       p.d_expr = getExpressionForNameAndType(p.d_name, type);
1610     }
1611     if (p.d_expr.isNull())
1612     {
1613       std::stringstream ss;
1614       ss << "Could not resolve expression with name " << p.d_name
1615          << " and type " << type << std::endl;
1616       parseError(ss.str());
1617     }
1618   }
1619   ExprManager* em = getExprManager();
1620   Type etype = p.d_expr.getType();
1621   Kind ekind = p.d_expr.getKind();
1622   Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr;
1623   Trace("parser-qid") << " " << ekind << " " << etype;
1624   Trace("parser-qid") << std::endl;
1625   if (ekind == kind::APPLY_CONSTRUCTOR && type.isDatatype())
1626   {
1627     // nullary constructors with a type ascription
1628     // could be a parametric constructor or just an overloaded constructor
1629     DatatypeType dtype = static_cast<DatatypeType>(type);
1630     if (dtype.isParametric())
1631     {
1632       std::vector<Expr> v;
1633       Expr e = p.d_expr.getOperator();
1634       const DatatypeConstructor& dtc =
1635           Datatype::datatypeOf(e)[Datatype::indexOf(e)];
1636       v.push_back(em->mkExpr(
1637           kind::APPLY_TYPE_ASCRIPTION,
1638           em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))),
1639           p.d_expr.getOperator()));
1640       v.insert(v.end(), p.d_expr.begin(), p.d_expr.end());
1641       p.d_expr = em->mkExpr(kind::APPLY_CONSTRUCTOR, v);
1642     }
1643   }
1644   else if (etype.isConstructor())
1645   {
1646     // a non-nullary constructor with a type ascription
1647     DatatypeType dtype = static_cast<DatatypeType>(type);
1648     if (dtype.isParametric())
1649     {
1650       const DatatypeConstructor& dtc =
1651           Datatype::datatypeOf(p.d_expr)[Datatype::indexOf(p.d_expr)];
1652       p.d_expr = em->mkExpr(
1653           kind::APPLY_TYPE_ASCRIPTION,
1654           em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))),
1655           p.d_expr);
1656     }
1657   }
1658   else if (ekind == kind::EMPTYSET)
1659   {
1660     Debug("parser") << "Empty set encountered: " << p.d_expr << " " << type
1661                     << std::endl;
1662     p.d_expr = em->mkConst(EmptySet(type));
1663   }
1664   else if (ekind == kind::UNIVERSE_SET)
1665   {
1666     p.d_expr = em->mkNullaryOperator(type, kind::UNIVERSE_SET);
1667   }
1668   else if (ekind == kind::SEP_NIL)
1669   {
1670     // We don't want the nil reference to be a constant: for instance, it
1671     // could be of type Int but is not a const rational. However, the
1672     // expression has 0 children. So we convert to a SEP_NIL variable.
1673     p.d_expr = em->mkNullaryOperator(type, kind::SEP_NIL);
1674   }
1675   else if (etype != type)
1676   {
1677     parseError("Type ascription not satisfied.");
1678   }
1679 }
1680
1681 Expr Smt2::parseOpToExpr(ParseOp& p)
1682 {
1683   Expr expr;
1684   if (p.d_kind != kind::NULL_EXPR || !p.d_type.isNull())
1685   {
1686     parseError(
1687         "Bad syntax for qualified identifier operator in term position.");
1688   }
1689   else if (!p.d_expr.isNull())
1690   {
1691     expr = p.d_expr;
1692   }
1693   else if (!isDeclared(p.d_name, SYM_VARIABLE))
1694   {
1695     if (sygus_v1() && p.d_name[0] == '-'
1696         && p.d_name.find_first_not_of("0123456789", 1) == std::string::npos)
1697     {
1698       // allow unary minus in sygus version 1
1699       expr = getExprManager()->mkConst(Rational(p.d_name));
1700     }
1701     else
1702     {
1703       std::stringstream ss;
1704       ss << "Symbol " << p.d_name << " is not declared.";
1705       parseError(ss.str());
1706     }
1707   }
1708   else
1709   {
1710     expr = getExpressionForName(p.d_name);
1711   }
1712   assert(!expr.isNull());
1713   return expr;
1714 }
1715
1716 Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
1717 {
1718   bool isBuiltinOperator = false;
1719   // the builtin kind of the overall return expression
1720   Kind kind = kind::NULL_EXPR;
1721   // First phase: process the operator
1722   if (Debug.isOn("parser"))
1723   {
1724     Debug("parser") << "Apply parse op to:" << std::endl;
1725     Debug("parser") << "args has size " << args.size() << std::endl;
1726     for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
1727     {
1728       Debug("parser") << "++ " << *i << std::endl;
1729     }
1730   }
1731   if (p.d_kind != kind::NULL_EXPR)
1732   {
1733     // It is a special case, e.g. tupSel or array constant specification.
1734     // We have to wait until the arguments are parsed to resolve it.
1735   }
1736   else if (!p.d_expr.isNull())
1737   {
1738     // An explicit operator, e.g. an indexed symbol.
1739     args.insert(args.begin(), p.d_expr);
1740     Kind fkind = getKindForFunction(p.d_expr);
1741     if (fkind != kind::UNDEFINED_KIND)
1742     {
1743       // Some operators may require a specific kind.
1744       // Testers are handled differently than other indexed operators,
1745       // since they require a kind.
1746       kind = fkind;
1747     }
1748   }
1749   else
1750   {
1751     isBuiltinOperator = isOperatorEnabled(p.d_name);
1752     if (isBuiltinOperator)
1753     {
1754       // a builtin operator, convert to kind
1755       kind = getOperatorKind(p.d_name);
1756     }
1757     else
1758     {
1759       // A non-built-in function application, get the expression
1760       checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE);
1761       Expr v = getVariable(p.d_name);
1762       if (!v.isNull())
1763       {
1764         checkFunctionLike(v);
1765         kind = getKindForFunction(v);
1766         args.insert(args.begin(), v);
1767       }
1768       else
1769       {
1770         // Overloaded symbol?
1771         // Could not find the expression. It may be an overloaded symbol,
1772         // in which case we may find it after knowing the types of its
1773         // arguments.
1774         std::vector<Type> argTypes;
1775         for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
1776         {
1777           argTypes.push_back((*i).getType());
1778         }
1779         Expr op = getOverloadedFunctionForTypes(p.d_name, argTypes);
1780         if (!op.isNull())
1781         {
1782           checkFunctionLike(op);
1783           kind = getKindForFunction(op);
1784           args.insert(args.begin(), op);
1785         }
1786         else
1787         {
1788           parseError(
1789               "Cannot find unambiguous overloaded function for argument "
1790               "types.");
1791         }
1792       }
1793     }
1794   }
1795   // Second phase: apply the arguments to the parse op
1796   ExprManager* em = getExprManager();
1797   // handle special cases
1798   if (p.d_kind == kind::STORE_ALL && !p.d_type.isNull())
1799   {
1800     if (args.size() != 1)
1801     {
1802       parseError("Too many arguments to array constant.");
1803     }
1804     Expr constVal = args[0];
1805     if (!constVal.isConst())
1806     {
1807       // To parse array constants taking reals whose values are specified by
1808       // rationals, e.g. ((as const (Array Int Real)) (/ 1 3)), we must handle
1809       // the fact that (/ 1 3) is the division of constants 1 and 3, and not
1810       // the resulting constant rational value. Thus, we must construct the
1811       // resulting rational here. This also is applied for integral real values
1812       // like 5.0 which are converted to (/ 5 1) to distinguish them from
1813       // integer constants. We must ensure numerator and denominator are
1814       // constant and the denominator is non-zero.
1815       if (constVal.getKind() == kind::DIVISION && constVal[0].isConst()
1816           && constVal[1].isConst()
1817           && !constVal[1].getConst<Rational>().isZero())
1818       {
1819         constVal = em->mkConst(constVal[0].getConst<Rational>()
1820                                / constVal[1].getConst<Rational>());
1821       }
1822       if (!constVal.isConst())
1823       {
1824         std::stringstream ss;
1825         ss << "expected constant term inside array constant, but found "
1826            << "nonconstant term:" << std::endl
1827            << "the term: " << constVal;
1828         parseError(ss.str());
1829       }
1830     }
1831     ArrayType aqtype = static_cast<ArrayType>(p.d_type);
1832     if (!aqtype.getConstituentType().isComparableTo(constVal.getType()))
1833     {
1834       std::stringstream ss;
1835       ss << "type mismatch inside array constant term:" << std::endl
1836          << "array type:          " << p.d_type << std::endl
1837          << "expected const type: " << aqtype.getConstituentType() << std::endl
1838          << "computed const type: " << constVal.getType();
1839       parseError(ss.str());
1840     }
1841     return em->mkConst(ArrayStoreAll(p.d_type, constVal));
1842   }
1843   else if (p.d_kind == kind::APPLY_SELECTOR && !p.d_expr.isNull())
1844   {
1845     // tuple selector case
1846     Integer x = p.d_expr.getConst<Rational>().getNumerator();
1847     if (!x.fitsUnsignedInt())
1848     {
1849       parseError("index of tupSel is larger than size of unsigned int");
1850     }
1851     unsigned int n = x.toUnsignedInt();
1852     if (args.size() > 1)
1853     {
1854       parseError("tupSel applied to more than one tuple argument");
1855     }
1856     Type t = args[0].getType();
1857     if (!t.isTuple())
1858     {
1859       parseError("tupSel applied to non-tuple");
1860     }
1861     size_t length = ((DatatypeType)t).getTupleLength();
1862     if (n >= length)
1863     {
1864       std::stringstream ss;
1865       ss << "tuple is of length " << length << "; cannot access index " << n;
1866       parseError(ss.str());
1867     }
1868     const Datatype& dt = ((DatatypeType)t).getDatatype();
1869     return em->mkExpr(kind::APPLY_SELECTOR, dt[0][n].getSelector(), args);
1870   }
1871   else if (p.d_kind != kind::NULL_EXPR)
1872   {
1873     // it should not have an expression or type specified at this point
1874     if (!p.d_expr.isNull() || !p.d_type.isNull())
1875     {
1876       std::stringstream ss;
1877       ss << "Could not process parsed qualified identifier kind " << p.d_kind;
1878       parseError(ss.str());
1879     }
1880     // otherwise it is a simple application
1881     kind = p.d_kind;
1882   }
1883   else if (isBuiltinOperator)
1884   {
1885     if (!em->getOptions().getUfHo()
1886         && (kind == kind::EQUAL || kind == kind::DISTINCT))
1887     {
1888       // need --uf-ho if these operators are applied over function args
1889       for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
1890       {
1891         if ((*i).getType().isFunction())
1892         {
1893           parseError(
1894               "Cannot apply equalty to functions unless --uf-ho is set.");
1895         }
1896       }
1897     }
1898     if (args.size() > 2)
1899     {
1900       if (kind == kind::INTS_DIVISION || kind == kind::XOR
1901           || kind == kind::MINUS || kind == kind::DIVISION
1902           || (kind == kind::BITVECTOR_XNOR && v2_6()))
1903       {
1904         // Builtin operators that are not tokenized, are left associative,
1905         // but not internally variadic must set this.
1906         return em->mkLeftAssociative(kind, args);
1907       }
1908       else if (kind == kind::IMPLIES)
1909       {
1910         /* right-associative, but CVC4 internally only supports 2 args */
1911         return em->mkRightAssociative(kind, args);
1912       }
1913       else if (kind == kind::EQUAL || kind == kind::LT || kind == kind::GT
1914                || kind == kind::LEQ || kind == kind::GEQ)
1915       {
1916         /* "chainable", but CVC4 internally only supports 2 args */
1917         return em->mkExpr(em->mkConst(Chain(kind)), args);
1918       }
1919     }
1920
1921     if (kind::isAssociative(kind) && args.size() > em->maxArity(kind))
1922     {
1923       /* Special treatment for associative operators with lots of children
1924        */
1925       return em->mkAssociative(kind, args);
1926     }
1927     else if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR)
1928              && args.size() == 1)
1929     {
1930       // Unary AND/OR can be replaced with the argument.
1931       return args[0];
1932     }
1933     else if (kind == kind::MINUS && args.size() == 1)
1934     {
1935       return em->mkExpr(kind::UMINUS, args[0]);
1936     }
1937     else
1938     {
1939       checkOperator(kind, args.size());
1940       return em->mkExpr(kind, args);
1941     }
1942   }
1943
1944   if (args.size() >= 2)
1945   {
1946     // may be partially applied function, in this case we use HO_APPLY
1947     Type argt = args[0].getType();
1948     if (argt.isFunction())
1949     {
1950       unsigned arity = static_cast<FunctionType>(argt).getArity();
1951       if (args.size() - 1 < arity)
1952       {
1953         Debug("parser") << "Partial application of " << args[0];
1954         Debug("parser") << " : #argTypes = " << arity;
1955         Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
1956         // must curry the partial application
1957         return em->mkLeftAssociative(kind::HO_APPLY, args);
1958       }
1959     }
1960   }
1961   if (kind == kind::NULL_EXPR)
1962   {
1963     std::vector<Expr> eargs(args.begin() + 1, args.end());
1964     return em->mkExpr(args[0], eargs);
1965   }
1966   return em->mkExpr(kind, args);
1967 }
1968
1969 Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr)
1970 {
1971   if (!sexpr.isKeyword())
1972   {
1973     parseError("improperly formed :named annotation");
1974   }
1975   std::string name = sexpr.getValue();
1976   checkUserSymbol(name);
1977   // ensure expr is a closed subterm
1978   if (expr.hasFreeVariable())
1979   {
1980     std::stringstream ss;
1981     ss << ":named annotations can only name terms that are closed";
1982     parseError(ss.str());
1983   }
1984   // check that sexpr is a fresh function symbol, and reserve it
1985   reserveSymbolAtAssertionLevel(name);
1986   // define it
1987   Expr func = mkVar(name, expr.getType(), ExprManager::VAR_FLAG_DEFINED);
1988   // remember the last term to have been given a :named attribute
1989   setLastNamedTerm(expr, name);
1990   return func;
1991 }
1992
1993 Expr Smt2::mkAnd(const std::vector<Expr>& es)
1994 {
1995   ExprManager* em = getExprManager();
1996
1997   if (es.size() == 0)
1998   {
1999     return em->mkConst(true);
2000   }
2001   else if (es.size() == 1)
2002   {
2003     return es[0];
2004   }
2005   else
2006   {
2007     return em->mkExpr(kind::AND, es);
2008   }
2009 }
2010
2011 }  // namespace parser
2012 }/* CVC4 namespace */