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