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-2017 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
  19 #include "expr/type.h"
  20 #include "parser/antlr_input.h"
  21 #include "parser/parser.h"
  22 #include "parser/smt1/smt1.h"
  23 #include "parser/smt2/smt2_input.h"
  24 #include "printer/sygus_print_callback.h"
  25 #include "smt/command.h"
  26 #include "util/bitvector.h"
  27
  28 #include <algorithm>
  29
  30 // ANTLR defines these, which is really bad!
  31 #undef true
  32 #undef false
  33
  34 namespace CVC4 {
  35 namespace parser {
  36
  37 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
  38   Parser(exprManager,input,strictMode,parseOnly),
  39   d_logicSet(false) {
  40   if( !strictModeEnabled() ) {
  41     addTheory(Smt2::THEORY_CORE);
  42   }
  43 }
  44
  45 void Smt2::setLanguage(InputLanguage lang) {
  46   ((Smt2Input*) getInput())->setLanguage(lang);
  47 }
  48
  49 void Smt2::addArithmeticOperators() {
  50   Parser::addOperator(kind::PLUS);
  51   Parser::addOperator(kind::MINUS);
  52   Parser::addOperator(kind::UMINUS);
  53   Parser::addOperator(kind::MULT);
  54   Parser::addOperator(kind::LT);
  55   Parser::addOperator(kind::LEQ);
  56   Parser::addOperator(kind::GT);
  57   Parser::addOperator(kind::GEQ);
  58
  59   addOperator(kind::POW, "^");
  60   addOperator(kind::EXPONENTIAL, "exp");
  61   addOperator(kind::SINE, "sin");
  62   addOperator(kind::COSINE, "cos");
  63   addOperator(kind::TANGENT, "tan");
  64 }
  65
  66 void Smt2::addBitvectorOperators() {
  67   addOperator(kind::BITVECTOR_CONCAT, "concat");
  68   addOperator(kind::BITVECTOR_NOT, "bvnot");
  69   addOperator(kind::BITVECTOR_AND, "bvand");
  70   addOperator(kind::BITVECTOR_OR, "bvor");
  71   addOperator(kind::BITVECTOR_NEG, "bvneg");
  72   addOperator(kind::BITVECTOR_PLUS, "bvadd");
  73   addOperator(kind::BITVECTOR_MULT, "bvmul");
  74   addOperator(kind::BITVECTOR_UDIV, "bvudiv");
  75   addOperator(kind::BITVECTOR_UREM, "bvurem");
  76   addOperator(kind::BITVECTOR_SHL, "bvshl");
  77   addOperator(kind::BITVECTOR_LSHR, "bvlshr");
  78   addOperator(kind::BITVECTOR_ULT, "bvult");
  79   addOperator(kind::BITVECTOR_NAND, "bvnand");
  80   addOperator(kind::BITVECTOR_NOR, "bvnor");
  81   addOperator(kind::BITVECTOR_XOR, "bvxor");
  82   addOperator(kind::BITVECTOR_XNOR, "bvxnor");
  83   addOperator(kind::BITVECTOR_COMP, "bvcomp");
  84   addOperator(kind::BITVECTOR_SUB, "bvsub");
  85   addOperator(kind::BITVECTOR_SDIV, "bvsdiv");
  86   addOperator(kind::BITVECTOR_SREM, "bvsrem");
  87   addOperator(kind::BITVECTOR_SMOD, "bvsmod");
  88   addOperator(kind::BITVECTOR_ASHR, "bvashr");
  89   addOperator(kind::BITVECTOR_ULE, "bvule");
  90   addOperator(kind::BITVECTOR_UGT, "bvugt");
  91   addOperator(kind::BITVECTOR_UGE, "bvuge");
  92   addOperator(kind::BITVECTOR_SLT, "bvslt");
  93   addOperator(kind::BITVECTOR_SLE, "bvsle");
  94   addOperator(kind::BITVECTOR_SGT, "bvsgt");
  95   addOperator(kind::BITVECTOR_SGE, "bvsge");
  96   addOperator(kind::BITVECTOR_REDOR, "bvredor");
  97   addOperator(kind::BITVECTOR_REDAND, "bvredand");
  98
  99   Parser::addOperator(kind::BITVECTOR_BITOF);
 100   Parser::addOperator(kind::BITVECTOR_EXTRACT);
 101   Parser::addOperator(kind::BITVECTOR_REPEAT);
 102   Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND);
 103   Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND);
 104   Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT);
 105   Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT);
 106
 107   Parser::addOperator(kind::INT_TO_BITVECTOR);
 108   Parser::addOperator(kind::BITVECTOR_TO_NAT);
 109 }
 110
 111 void Smt2::addStringOperators() {
 112   addOperator(kind::STRING_CONCAT, "str.++");
 113   addOperator(kind::STRING_LENGTH, "str.len");
 114   addOperator(kind::STRING_SUBSTR, "str.substr" );
 115   addOperator(kind::STRING_STRCTN, "str.contains" );
 116   addOperator(kind::STRING_CHARAT, "str.at" );
 117   addOperator(kind::STRING_STRIDOF, "str.indexof" );
 118   addOperator(kind::STRING_STRREPL, "str.replace" );
 119   addOperator(kind::STRING_PREFIX, "str.prefixof" );
 120   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
 121   addOperator(kind::STRING_ITOS, "int.to.str" );
 122   addOperator(kind::STRING_STOI, "str.to.int" );
 123   addOperator(kind::STRING_IN_REGEXP, "str.in.re");
 124   addOperator(kind::STRING_TO_REGEXP, "str.to.re");
 125   addOperator(kind::REGEXP_CONCAT, "re.++");
 126   addOperator(kind::REGEXP_UNION, "re.union");
 127   addOperator(kind::REGEXP_INTER, "re.inter");
 128   addOperator(kind::REGEXP_STAR, "re.*");
 129   addOperator(kind::REGEXP_PLUS, "re.+");
 130   addOperator(kind::REGEXP_OPT, "re.opt");
 131   addOperator(kind::REGEXP_RANGE, "re.range");
 132   addOperator(kind::REGEXP_LOOP, "re.loop");
 133 }
 134
 135 void Smt2::addFloatingPointOperators() {
 136   addOperator(kind::FLOATINGPOINT_FP, "fp");
 137   addOperator(kind::FLOATINGPOINT_EQ, "fp.eq");
 138   addOperator(kind::FLOATINGPOINT_ABS, "fp.abs");
 139   addOperator(kind::FLOATINGPOINT_NEG, "fp.neg");
 140   addOperator(kind::FLOATINGPOINT_PLUS, "fp.add");
 141   addOperator(kind::FLOATINGPOINT_SUB, "fp.sub");
 142   addOperator(kind::FLOATINGPOINT_MULT, "fp.mul");
 143   addOperator(kind::FLOATINGPOINT_DIV, "fp.div");
 144   addOperator(kind::FLOATINGPOINT_FMA, "fp.fma");
 145   addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt");
 146   addOperator(kind::FLOATINGPOINT_REM, "fp.rem");
 147   addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral");
 148   addOperator(kind::FLOATINGPOINT_MIN, "fp.min");
 149   addOperator(kind::FLOATINGPOINT_MAX, "fp.max");
 150   addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq");
 151   addOperator(kind::FLOATINGPOINT_LT, "fp.lt");
 152   addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq");
 153   addOperator(kind::FLOATINGPOINT_GT, "fp.gt");
 154   addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal");
 155   addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal");
 156   addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero");
 157   addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite");
 158   addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN");
 159   addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative");
 160   addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
 161   addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
 162
 163   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
 164   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
 165   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL);
 166   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
 167   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
 168   Parser::addOperator(kind::FLOATINGPOINT_TO_UBV);
 169   Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
 170 }
 171
 172 void Smt2::addSepOperators() {
 173   addOperator(kind::SEP_STAR, "sep");
 174   addOperator(kind::SEP_PTO, "pto");
 175   addOperator(kind::SEP_WAND, "wand");
 176   addOperator(kind::SEP_EMP, "emp");
 177   Parser::addOperator(kind::SEP_STAR);
 178   Parser::addOperator(kind::SEP_PTO);
 179   Parser::addOperator(kind::SEP_WAND);
 180   Parser::addOperator(kind::SEP_EMP);
 181 }
 182
 183 void Smt2::addTheory(Theory theory) {
 184   switch(theory) {
 185   case THEORY_ARRAYS:
 186     addOperator(kind::SELECT, "select");
 187     addOperator(kind::STORE, "store");
 188     break;
 189
 190   case THEORY_BITVECTORS:
 191     addBitvectorOperators();
 192     break;
 193
 194   case THEORY_CORE:
 195     defineType("Bool", getExprManager()->booleanType());
 196     defineVar("true", getExprManager()->mkConst(true));
 197     defineVar("false", getExprManager()->mkConst(false));
 198     Parser::addOperator(kind::AND);
 199     Parser::addOperator(kind::DISTINCT);
 200     Parser::addOperator(kind::EQUAL);
 201     Parser::addOperator(kind::IMPLIES);
 202     Parser::addOperator(kind::ITE);
 203     Parser::addOperator(kind::NOT);
 204     Parser::addOperator(kind::OR);
 205     Parser::addOperator(kind::XOR);
 206     break;
 207
 208   case THEORY_REALS_INTS:
 209     defineType("Real", getExprManager()->realType());
 210     Parser::addOperator(kind::DIVISION);
 211     addOperator(kind::TO_INTEGER, "to_int");
 212     addOperator(kind::IS_INTEGER, "is_int");
 213     addOperator(kind::TO_REAL, "to_real");
 214     // falling through on purpose, to add Ints part of Reals_Ints
 215   case THEORY_INTS:
 216     defineType("Int", getExprManager()->integerType());
 217     addArithmeticOperators();
 218     addOperator(kind::INTS_DIVISION, "div");
 219     addOperator(kind::INTS_MODULUS, "mod");
 220     addOperator(kind::ABS, "abs");
 221     Parser::addOperator(kind::DIVISIBLE);
 222     break;
 223
 224   case THEORY_REALS:
 225     defineType("Real", getExprManager()->realType());
 226     addArithmeticOperators();
 227     Parser::addOperator(kind::DIVISION);
 228     break;
 229
 230   case THEORY_QUANTIFIERS:
 231     break;
 232
 233   case THEORY_SETS:
 234     addOperator(kind::UNION, "union");
 235     addOperator(kind::INTERSECTION, "intersection");
 236     addOperator(kind::SETMINUS, "setminus");
 237     addOperator(kind::SUBSET, "subset");
 238     addOperator(kind::MEMBER, "member");
 239     addOperator(kind::SINGLETON, "singleton");
 240     addOperator(kind::INSERT, "insert");
 241     addOperator(kind::CARD, "card");
 242     addOperator(kind::COMPLEMENT, "complement");
 243     break;
 244
 245   case THEORY_DATATYPES:
 246     Parser::addOperator(kind::APPLY_CONSTRUCTOR);
 247     Parser::addOperator(kind::APPLY_TESTER);
 248     Parser::addOperator(kind::APPLY_SELECTOR);
 249     Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
 250     break;
 251
 252   case THEORY_STRINGS:
 253     defineType("String", getExprManager()->stringType());
 254     defineType("Int", getExprManager()->integerType());
 255     addStringOperators();
 256     break;
 257
 258   case THEORY_UF:
 259     Parser::addOperator(kind::APPLY_UF);
 260     break;
 261
 262   case THEORY_FP:
 263     defineType("RoundingMode", getExprManager()->roundingModeType());
 264     defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
 265     defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
 266     defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
 267     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
 268     addFloatingPointOperators();
 269     break;
 270
 271   case THEORY_SEP:
 272     addSepOperators();
 273     break;
 274
 275   default:
 276     std::stringstream ss;
 277     ss << "internal error: unsupported theory " << theory;
 278     throw ParserException(ss.str());
 279   }
 280 }
 281
 282 void Smt2::addOperator(Kind kind, const std::string& name) {
 283   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 284                   << std::endl;
 285   Parser::addOperator(kind);
 286   operatorKindMap[name] = kind;
 287 }
 288
 289 Kind Smt2::getOperatorKind(const std::string& name) const {
 290   // precondition: isOperatorEnabled(name)
 291   return operatorKindMap.find(name)->second;
 292 }
 293
 294 bool Smt2::isOperatorEnabled(const std::string& name) const {
 295   return operatorKindMap.find(name) != operatorKindMap.end();
 296 }
 297
 298 bool Smt2::isTheoryEnabled(Theory theory) const {
 299   switch(theory) {
 300   case THEORY_ARRAYS:
 301     return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
 302   case THEORY_BITVECTORS:
 303     return d_logic.isTheoryEnabled(theory::THEORY_BV);
 304   case THEORY_CORE:
 305     return true;
 306   case THEORY_DATATYPES:
 307     return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
 308   case THEORY_INTS:
 309     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 310       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
 311   case THEORY_REALS:
 312     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 313       ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
 314   case THEORY_REALS_INTS:
 315     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 316       d_logic.areIntegersUsed() && d_logic.areRealsUsed();
 317   case THEORY_QUANTIFIERS:
 318     return d_logic.isQuantified();
 319   case THEORY_SETS:
 320     return d_logic.isTheoryEnabled(theory::THEORY_SETS);
 321   case THEORY_STRINGS:
 322     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
 323   case THEORY_UF:
 324     return d_logic.isTheoryEnabled(theory::THEORY_UF);
 325   case THEORY_FP:
 326     return d_logic.isTheoryEnabled(theory::THEORY_FP);
 327   case THEORY_SEP:
 328     return d_logic.isTheoryEnabled(theory::THEORY_SEP);
 329   default:
 330     std::stringstream ss;
 331     ss << "internal error: unsupported theory " << theory;
 332     throw ParserException(ss.str());
 333   }
 334 }
 335
 336 bool Smt2::logicIsSet() {
 337   return d_logicSet;
 338 }
 339
 340 Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
 341   if(sygus() && name[0]=='-' &&
 342     name.find_first_not_of("0123456789", 1) == std::string::npos) {
 343     //allow unary minus in sygus
 344     return getExprManager()->mkConst(Rational(name));
 345   }else if(isAbstractValue(name)) {
 346     return mkAbstractValue(name);
 347   }else{
 348     return Parser::getExpressionForNameAndType(name, t);
 349   }
 350 }
 351
 352 Expr Smt2::mkDefineFunRec(
 353     const std::string& fname,
 354     const std::vector<std::pair<std::string, Type> >& sortedVarNames,
 355     Type t,
 356     std::vector<Expr>& flattenVars)
 357 {
 358   std::vector<Type> sorts;
 359   for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
 360   {
 361     sorts.push_back(svn.second);
 362   }
 363
 364   // make the flattened function type, add bound variables
 365   // to flattenVars if the defined function was given a function return type.
 366   Type ft = mkFlatFunctionType(sorts, t, flattenVars);
 367
 368   // allow overloading
 369   return mkVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
 370 }
 371
 372 void Smt2::pushDefineFunRecScope(
 373     const std::vector<std::pair<std::string, Type> >& sortedVarNames,
 374     Expr func,
 375     const std::vector<Expr>& flattenVars,
 376     Expr& func_app,
 377     std::vector<Expr>& bvs,
 378     bool bindingLevel)
 379 {
 380   pushScope(bindingLevel);
 381
 382   std::vector<Expr> f_app;
 383   f_app.push_back(func);
 384   // bound variables are those that are explicitly named in the preamble
 385   // of the define-fun(s)-rec command, we define them here
 386   for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
 387   {
 388     Expr v = mkBoundVar(svn.first, svn.second);
 389     bvs.push_back(v);
 390     f_app.push_back(v);
 391   }
 392
 393   bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end());
 394
 395   // make the function application
 396   if (bvs.empty())
 397   {
 398     // it has no arguments
 399     func_app = func;
 400   }
 401   else
 402   {
 403     func_app = getExprManager()->mkExpr(kind::APPLY_UF, f_app);
 404   }
 405 }
 406
 407 void Smt2::reset() {
 408   d_logicSet = false;
 409   d_logic = LogicInfo();
 410   operatorKindMap.clear();
 411   d_lastNamedTerm = std::pair<Expr, std::string>();
 412   this->Parser::reset();
 413
 414   if( !strictModeEnabled() ) {
 415     addTheory(Smt2::THEORY_CORE);
 416   }
 417 }
 418
 419 void Smt2::resetAssertions() {
 420   this->Parser::reset();
 421 }
 422
 423 void Smt2::setLogic(std::string name) {
 424
 425   if(sygus()) {
 426     // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2)
 427     if(name == "Arrays") {
 428       name = "A";
 429     }else if(name == "Reals") {
 430       name = "LRA";
 431     }
 432   }
 433
 434   d_logicSet = true;
 435   if(logicIsForced()) {
 436     d_logic = getForcedLogic();
 437   } else {
 438     d_logic = name;
 439   }
 440
 441   // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
 442   // higher-order
 443   if(sygus()) {
 444     // get unlocked copy, modify, copy and relock
 445     LogicInfo log(d_logic.getUnlockedCopy());
 446     log.enableTheory(theory::THEORY_UF);
 447     log.enableTheory(theory::THEORY_DATATYPES);
 448     log.enableIntegers();
 449     log.enableHigherOrder();
 450     d_logic = log;
 451     d_logic.lock();
 452   }
 453
 454   // Core theory belongs to every logic
 455   addTheory(THEORY_CORE);
 456
 457   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 458     addTheory(THEORY_UF);
 459   }
 460
 461   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 462     if(d_logic.areIntegersUsed()) {
 463       if(d_logic.areRealsUsed()) {
 464         addTheory(THEORY_REALS_INTS);
 465       } else {
 466         addTheory(THEORY_INTS);
 467       }
 468     } else if(d_logic.areRealsUsed()) {
 469       addTheory(THEORY_REALS);
 470     }
 471   }
 472
 473   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
 474     addTheory(THEORY_ARRAYS);
 475   }
 476
 477   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 478     addTheory(THEORY_BITVECTORS);
 479   }
 480
 481   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
 482     addTheory(THEORY_DATATYPES);
 483   }
 484
 485   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 486     addTheory(THEORY_SETS);
 487   }
 488
 489   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 490     addTheory(THEORY_STRINGS);
 491   }
 492
 493   if(d_logic.isQuantified()) {
 494     addTheory(THEORY_QUANTIFIERS);
 495   }
 496
 497   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
 498     addTheory(THEORY_FP);
 499   }
 500
 501   if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
 502     addTheory(THEORY_SEP);
 503   }
 504
 505 }/* Smt2::setLogic() */
 506
 507 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 508   // TODO: ???
 509 }
 510
 511 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 512   // TODO: ???
 513 }
 514
 515 void Smt2::checkThatLogicIsSet() {
 516   if( ! logicIsSet() ) {
 517     if(strictModeEnabled()) {
 518       parseError("set-logic must appear before this point.");
 519     } else {
 520       warning("No set-logic command was given before this point.");
 521       warning("CVC4 will make all theories available.");
 522       warning("Consider setting a stricter logic for (likely) better performance.");
 523       warning("To suppress this warning in the future use (set-logic ALL).");
 524
 525       setLogic("ALL");
 526
 527       Command* c = new SetBenchmarkLogicCommand("ALL");
 528       c->setMuted(true);
 529       preemptCommand(c);
 530     }
 531   }
 532 }
 533
 534 /* The include are managed in the lexer but called in the parser */
 535 // Inspired by http://www.antlr3.org/api/C/interop.html
 536
 537 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 538   Debug("parser") << "Including " << filename << std::endl;
 539   // Create a new input stream and take advantage of built in stream stacking
 540   // in C target runtime.
 541   //
 542   pANTLR3_INPUT_STREAM    in;
 543 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 544   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 545 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 546   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 547 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 548   if( in == NULL ) {
 549     Debug("parser") << "Can't open " << filename << std::endl;
 550     return false;
 551   }
 552   // Same thing as the predefined PUSHSTREAM(in);
 553   lexer->pushCharStream(lexer, in);
 554   // restart it
 555   //lexer->rec->state->tokenStartCharIndex      = -10;
 556   //lexer->emit(lexer);
 557
 558   // Note that the input stream is not closed when it EOFs, I don't bother
 559   // to do it here, but it is up to you to track streams created like this
 560   // and destroy them when the whole parse session is complete. Remember that you
 561   // don't want to do this until all tokens have been manipulated all the way through
 562   // your tree parsers etc as the token does not store the text it just refers
 563   // back to the input stream and trying to get the text for it will abort if you
 564   // close the input stream too early.
 565
 566   //TODO what said before
 567   return true;
 568 }
 569
 570 void Smt2::includeFile(const std::string& filename) {
 571   // security for online version
 572   if(!canIncludeFile()) {
 573     parseError("include-file feature was disabled for this run.");
 574   }
 575
 576   // Get the lexer
 577   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 578   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 579   // get the name of the current stream "Does it work inside an include?"
 580   const std::string inputName = ai->getInputStreamName();
 581
 582   // Find the directory of the current input file
 583   std::string path;
 584   size_t pos = inputName.rfind('/');
 585   if(pos != std::string::npos) {
 586     path = std::string(inputName, 0, pos + 1);
 587   }
 588   path.append(filename);
 589   if(!newInputStream(path, lexer)) {
 590     parseError("Couldn't open include file `" + path + "'");
 591   }
 592 }
 593
 594 Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) {
 595   Expr e = mkBoundVar(name, type);
 596   d_sygusVars.push_back(e);
 597   d_sygusVarPrimed[e] = false;
 598   if( isPrimed ){
 599     std::stringstream ss;
 600     ss << name << "'";
 601     Expr ep = mkBoundVar(ss.str(), type);
 602     d_sygusVars.push_back(ep);
 603     d_sygusVarPrimed[ep] = true;
 604   }
 605   return e;
 606 }
 607
 608 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
 609   if( type.isInteger() ){
 610     ops.push_back(getExprManager()->mkConst(Rational(0)));
 611     ops.push_back(getExprManager()->mkConst(Rational(1)));
 612   }else if( type.isBitVector() ){
 613     unsigned sz = ((BitVectorType)type).getSize();
 614     BitVector bval0(sz, (unsigned int)0);
 615     ops.push_back( getExprManager()->mkConst(bval0) );
 616     BitVector bval1(sz, (unsigned int)1);
 617     ops.push_back( getExprManager()->mkConst(bval1) );
 618   }else if( type.isBoolean() ){
 619     ops.push_back(getExprManager()->mkConst(true));
 620     ops.push_back(getExprManager()->mkConst(false));
 621   }
 622   //TODO : others?
 623 }
 624
 625 //  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)
 626 //  This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
 627 void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
 628                               std::vector< CVC4::Datatype >& datatypes,
 629                               std::vector< CVC4::Type>& sorts,
 630                               std::vector< std::vector<CVC4::Expr> >& ops,
 631                               std::vector< std::vector<std::string> >& cnames,
 632                               std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 633                               std::vector< bool >& allow_const,
 634                               std::vector< std::vector< std::string > >& unresolved_gterm_sym,
 635                               std::vector<CVC4::Expr>& sygus_vars,
 636                               std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
 637                               CVC4::Type& ret, bool isNested ){
 638   if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){
 639     Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index << std::endl;
 640     Kind oldKind;
 641     Kind newKind = kind::UNDEFINED_KIND;
 642     //convert to UMINUS if one child of MINUS
 643     if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){
 644       oldKind = kind::MINUS;
 645       newKind = kind::UMINUS;
 646     }
 647     /*
 648     //convert to IFF if boolean EQUAL
 649     if( sgt.d_expr==getExprManager()->operatorOf(kind::EQUAL) ){
 650       Type ctn = sgt.d_children[0].d_type;
 651       std::map< CVC4::Type, CVC4::Type >::iterator it = sygus_to_builtin.find( ctn );
 652       if( it != sygus_to_builtin.end() && it->second.isBoolean() ){
 653         oldKind = kind::EQUAL;
 654         newKind = kind::IFF;
 655       }
 656     }
 657     */
 658     if( newKind!=kind::UNDEFINED_KIND ){
 659       Expr newExpr = getExprManager()->operatorOf(newKind);
 660       Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl;
 661       sgt.d_expr = newExpr;
 662       std::string oldName = kind::kindToString(oldKind);
 663       std::string newName = kind::kindToString(newKind);
 664       size_t pos = 0;
 665       if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){
 666         sgt.d_name.replace(pos, oldName.length(), newName);
 667       }
 668     }
 669     ops[index].push_back( sgt.d_expr );
 670     cnames[index].push_back( sgt.d_name );
 671     cargs[index].push_back( std::vector< CVC4::Type >() );
 672     for( unsigned i=0; i<sgt.d_children.size(); i++ ){
 673       std::stringstream ss;
 674       ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
 675       std::string sub_dname = ss.str();
 676       //add datatype for child
 677       Type null_type;
 678       pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
 679       int sub_dt_index = datatypes.size()-1;
 680       //process child
 681       Type sub_ret;
 682       processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
 683                          sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
 684       //process the nested gterm (either pop the last datatype, or flatten the argument)
 685       Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
 686                                          sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
 687       cargs[index].back().push_back(tt);
 688     }
 689     //if let, must create operator
 690     if( sgt.d_gterm_type==SygusGTerm::gterm_let ){
 691       processSygusLetConstructor( sgt.d_let_vars, index, datatypes, sorts, ops, cnames, cargs,
 692                                   sygus_vars, sygus_to_builtin, sygus_to_builtin_expr );
 693     }
 694   }else if( sgt.d_gterm_type==SygusGTerm::gterm_constant ){
 695     if( sgt.getNumChildren()!=0 ){
 696       parseError("Bad syntax for Sygus Constant.");
 697     }
 698     std::vector< Expr > consts;
 699     mkSygusConstantsForType( sgt.d_type, consts );
 700     Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
 701     for( unsigned i=0; i<consts.size(); i++ ){
 702       std::stringstream ss;
 703       ss << consts[i];
 704       Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
 705       ops[index].push_back( consts[i] );
 706       cnames[index].push_back( ss.str() );
 707       cargs[index].push_back( std::vector< CVC4::Type >() );
 708     }
 709     allow_const[index] = true;
 710   }else if( sgt.d_gterm_type==SygusGTerm::gterm_variable || sgt.d_gterm_type==SygusGTerm::gterm_input_variable ){
 711     if( sgt.getNumChildren()!=0 ){
 712       parseError("Bad syntax for Sygus Variable.");
 713     }
 714     Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
 715     for( unsigned i=0; i<sygus_vars.size(); i++ ){
 716       if( sygus_vars[i].getType()==sgt.d_type ){
 717         std::stringstream ss;
 718         ss << sygus_vars[i];
 719         Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
 720         ops[index].push_back( sygus_vars[i] );
 721         cnames[index].push_back( ss.str() );
 722         cargs[index].push_back( std::vector< CVC4::Type >() );
 723       }
 724     }
 725   }else if( sgt.d_gterm_type==SygusGTerm::gterm_nested_sort ){
 726     ret = sgt.d_type;
 727   }else if( sgt.d_gterm_type==SygusGTerm::gterm_unresolved ){
 728     if( isNested ){
 729       if( isUnresolvedType(sgt.d_name) ){
 730         ret = getSort(sgt.d_name);
 731       }else{
 732         //nested, unresolved symbol...fail
 733         std::stringstream ss;
 734         ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl;
 735         parseError(ss.str());
 736       }
 737     }else{
 738       //will resolve when adding constructors
 739       unresolved_gterm_sym[index].push_back(sgt.d_name);
 740     }
 741   }else if( sgt.d_gterm_type==SygusGTerm::gterm_ignore ){
 742
 743   }
 744 }
 745
 746 bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
 747                                   std::vector< CVC4::Datatype >& datatypes,
 748                                   std::vector< CVC4::Type>& sorts,
 749                                   std::vector< std::vector<CVC4::Expr> >& ops,
 750                                   std::vector< std::vector<std::string> >& cnames,
 751                                   std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 752                                   std::vector< bool >& allow_const,
 753                                   std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
 754   sorts.push_back(t);
 755   datatypes.push_back(Datatype(dname));
 756   ops.push_back(std::vector<Expr>());
 757   cnames.push_back(std::vector<std::string>());
 758   cargs.push_back(std::vector<std::vector<CVC4::Type> >());
 759   allow_const.push_back(false);
 760   unresolved_gterm_sym.push_back(std::vector< std::string >());
 761   return true;
 762 }
 763
 764 bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
 765                                  std::vector< CVC4::Type>& sorts,
 766                                  std::vector< std::vector<CVC4::Expr> >& ops,
 767                                  std::vector< std::vector<std::string> >& cnames,
 768                                  std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 769                                  std::vector< bool >& allow_const,
 770                                  std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
 771   sorts.pop_back();
 772   datatypes.pop_back();
 773   ops.pop_back();
 774   cnames.pop_back();
 775   cargs.pop_back();
 776   allow_const.pop_back();
 777   unresolved_gterm_sym.pop_back();
 778   return true;
 779 }
 780
 781 Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
 782                                     std::vector< CVC4::Type>& sorts,
 783                                     std::vector< std::vector<CVC4::Expr> >& ops,
 784                                     std::vector< std::vector<std::string> >& cnames,
 785                                     std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 786                                     std::vector< bool >& allow_const,
 787                                     std::vector< std::vector< std::string > >& unresolved_gterm_sym,
 788                                     std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
 789                                     std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) {
 790   Type t = sub_ret;
 791   Debug("parser-sygus") << "Argument is ";
 792   if( t.isNull() ){
 793     //then, it is the datatype we constructed, which should have a single constructor
 794     t = mkUnresolvedType(sub_dname);
 795     Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t << std::endl;
 796     Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs[sub_dt_index].size() << std::endl;
 797     if( cargs[sub_dt_index].empty() ){
 798       parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
 799     }
 800     Expr sop = ops[sub_dt_index][0];
 801     Type curr_t;
 802     if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){
 803       curr_t = sop.getType();
 804       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;
 805       sygus_to_builtin_expr[t] = sop;
 806       //store that term sop has dedicated sygus type t
 807       if( d_sygus_bound_var_type.find( sop )==d_sygus_bound_var_type.end() ){
 808         d_sygus_bound_var_type[sop] = t;
 809       }
 810     }else{
 811       std::vector< Expr > children;
 812       if( sop.getKind() != kind::BUILTIN ){
 813         children.push_back( sop );
 814       }
 815       for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
 816         std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
 817         if( it==sygus_to_builtin_expr.end() ){
 818           if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){
 819             std::stringstream ss;
 820             ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl;
 821             ss << "Builtin types are currently : " << std::endl;
 822             for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){
 823               ss << "  " << itb->first << " -> " << itb->second << std::endl;
 824             }
 825             parseError(ss.str());
 826           }
 827           Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
 828           Debug("parser-sygus") << ":  child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
 829           std::stringstream ss;
 830           ss << t << "_x_" << i;
 831           Expr bv = mkBoundVar(ss.str(), bt);
 832           children.push_back( bv );
 833           d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i];
 834         }else{
 835           Debug("parser-sygus") << ":  child " << i << " existing sygus to builtin expr : " << it->second << std::endl;
 836           children.push_back( it->second );
 837         }
 838       }
 839       Kind sk = sop.getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(sop);
 840       Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl;
 841       Expr e = getExprManager()->mkExpr( sk, children );
 842       Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
 843       curr_t = e.getType();
 844       sygus_to_builtin_expr[t] = e;
 845     }
 846     sorts[sub_dt_index] = curr_t;
 847     sygus_to_builtin[t] = curr_t;
 848   }else{
 849     Debug("parser-sygus") << "simple argument " << t << std::endl;
 850     Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl;
 851     //otherwise, datatype was unecessary
 852     //pop argument datatype definition
 853     popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
 854   }
 855   return t;
 856 }
 857
 858 void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
 859                                        int index,
 860                                        std::vector< CVC4::Datatype >& datatypes,
 861                                        std::vector< CVC4::Type>& sorts,
 862                                        std::vector< std::vector<CVC4::Expr> >& ops,
 863                                        std::vector< std::vector<std::string> >& cnames,
 864                                        std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 865                                        std::vector<CVC4::Expr>& sygus_vars,
 866                                        std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
 867                                        std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ) {
 868   std::vector< CVC4::Expr > let_define_args;
 869   Expr let_body;
 870   int dindex = cargs[index].size()-1;
 871   Debug("parser-sygus") << "Process let constructor for datatype " << datatypes[index].getName() << ", #subtypes = " << cargs[index][dindex].size() << std::endl;
 872   for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
 873     Debug("parser-sygus") << "  " << i << " : " << cargs[index][dindex][i] << std::endl;
 874     if( i+1==cargs[index][dindex].size() ){
 875       std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[index][dindex][i] );
 876       if( it!=sygus_to_builtin_expr.end() ){
 877         let_body = it->second;
 878       }else{
 879         std::stringstream ss;
 880         ss << datatypes[index].getName() << "_body";
 881         let_body = mkBoundVar(ss.str(), sygus_to_builtin[cargs[index][dindex][i]]);
 882         d_sygus_bound_var_type[let_body] = cargs[index][dindex][i];
 883       }
 884     }
 885   }
 886   Debug("parser-sygus") << std::endl;
 887   Debug("parser-sygus") << "Body is " << let_body << std::endl;
 888   Debug("parser-sygus") << "# let vars = " << let_vars.size() << std::endl;
 889   for( unsigned i=0; i<let_vars.size(); i++ ){
 890     Debug("parser-sygus") << "  let var " << i << " : " << let_vars[i] << " " << let_vars[i].getType() << std::endl;
 891     let_define_args.push_back( let_vars[i] );
 892   }
 893   /*
 894   Debug("parser-sygus") << "index = " << index << ", start index = " << start_index << ", #Current datatypes = " << datatypes.size() << std::endl;
 895   for( unsigned i=start_index; i<datatypes.size(); i++ ){
 896     Debug("parser-sygus") << "  datatype " << i << " : " << datatypes[i].getName() << ", #cons = " << cargs[i].size() << std::endl;
 897     if( !cargs[i].empty() ){
 898       Debug("parser-sygus") << "  operator 0 is " << ops[i][0] << std::endl;
 899       Debug("parser-sygus") << "  cons 0 has " << cargs[i][0].size() << " sub fields." << std::endl;
 900       for( unsigned j=0; j<cargs[i][0].size(); j++ ){
 901         Type bt = sygus_to_builtin[cargs[i][0][j]];
 902         Debug("parser-sygus") << "    cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl;
 903       }
 904     }
 905   }
 906   */
 907   //last argument is the return, pop
 908   cargs[index][dindex].pop_back();
 909   collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );
 910
 911   Debug("parser-sygus") << "Make define-fun with " << cargs[index][dindex].size() << " arguments..." << std::endl;
 912   std::vector<CVC4::Type> fsorts;
 913   for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
 914     Debug("parser-sygus") << "  " << i << " : " << let_define_args[i] << " " << let_define_args[i].getType() << " " << cargs[index][dindex][i] << std::endl;
 915     fsorts.push_back(let_define_args[i].getType());
 916   }
 917
 918   Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
 919   std::stringstream ss;
 920   ss << datatypes[index].getName() << "_let";
 921   Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
 922   d_sygus_defined_funs.push_back( let_func );
 923   preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) );
 924
 925   ops[index].pop_back();
 926   ops[index].push_back( let_func );
 927   cnames[index].pop_back();
 928   cnames[index].push_back(ss.str());
 929
 930   //mark function as let constructor
 931   d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_define_args.begin(), let_define_args.end() );
 932   d_sygus_let_func_to_body[let_func] = let_body;
 933   d_sygus_let_func_to_num_input_vars[let_func] = let_vars.size();
 934 }
 935
 936
 937 void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ) {
 938   if( e.getKind()==kind::BOUND_VARIABLE ){
 939     if( std::find( builtinArgs.begin(), builtinArgs.end(), e )==builtinArgs.end() ){
 940       builtinArgs.push_back( e );
 941       sygusArgs.push_back( d_sygus_bound_var_type[e] );
 942       if( d_sygus_bound_var_type[e].isNull() ){
 943         std::stringstream ss;
 944         ss << "While constructing body of let gterm, can't map " << e << " to sygus type." << std::endl;
 945         parseError(ss.str());
 946       }
 947     }
 948   }else{
 949     for( unsigned i=0; i<e.getNumChildren(); i++ ){
 950       collectSygusLetArgs( e[i], sygusArgs, builtinArgs );
 951     }
 952   }
 953 }
 954
 955 void Smt2::setSygusStartIndex( std::string& fun, int startIndex,
 956                                std::vector< CVC4::Datatype >& datatypes,
 957                                std::vector< CVC4::Type>& sorts,
 958                                std::vector< std::vector<CVC4::Expr> >& ops ) {
 959   if( startIndex>0 ){
 960     CVC4::Datatype tmp_dt = datatypes[0];
 961     Type tmp_sort = sorts[0];
 962     std::vector< Expr > tmp_ops;
 963     tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
 964     datatypes[0] = datatypes[startIndex];
 965     sorts[0] = sorts[startIndex];
 966     ops[0].clear();
 967     ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
 968     datatypes[startIndex] = tmp_dt;
 969     sorts[startIndex] = tmp_sort;
 970     ops[startIndex].clear();
 971     ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
 972   }else if( startIndex<0 ){
 973     std::stringstream ss;
 974     ss << "warning: no symbol named Start for synth-fun " << fun << std::endl;
 975     warning(ss.str());
 976   }
 977 }
 978
 979 void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
 980                             std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
 981                             std::vector<std::string>& unresolved_gterm_sym,
 982                             std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
 983   Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
 984   Debug("parser-sygus") << "  add constructors..." << std::endl;
 985
 986   Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl;
 987   Debug("parser-sygus") << "  add constructors..." << std::endl;
 988   for (unsigned i = 0, size = cnames.size(); i < size; i++)
 989   {
 990     bool is_dup = false;
 991     bool is_dup_op = false;
 992     for (unsigned j = 0; j < i; j++)
 993     {
 994       if( ops[i]==ops[j] ){
 995         is_dup_op = true;
 996         if( cargs[i].size()==cargs[j].size() ){
 997           is_dup = true;
 998           for( unsigned k=0; k<cargs[i].size(); k++ ){
 999             if( cargs[i][k]!=cargs[j][k] ){
1000               is_dup = false;
1001               break;
1002             }
1003           }
1004         }
1005         if( is_dup ){
1006           break;
1007         }
1008       }
1009     }
1010     Debug("parser-sygus") << "SYGUS CONS " << i << " : ";
1011     if( is_dup ){
1012       Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl;
1013       ops.erase( ops.begin() + i, ops.begin() + i + 1 );
1014       cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 );
1015       cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 );
1016       i--;
1017     }
1018     else
1019     {
1020       std::shared_ptr<SygusPrintCallback> spc;
1021       if (is_dup_op)
1022       {
1023         Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i]
1024                               << std::endl;
1025         // make into define-fun
1026         std::vector<Type> ltypes;
1027         for (unsigned j = 0, size = cargs[i].size(); j < size; j++)
1028         {
1029           ltypes.push_back(sygus_to_builtin[cargs[i][j]]);
1030         }
1031         std::vector<Expr> largs;
1032         Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
1033
1034         // make the let_body
1035         std::vector<Expr> children;
1036         if (ops[i].getKind() != kind::BUILTIN)
1037         {
1038           children.push_back(ops[i]);
1039         }
1040         children.insert(children.end(), largs.begin(), largs.end());
1041         Kind sk = ops[i].getKind() != kind::BUILTIN
1042                       ? kind::APPLY
1043                       : getExprManager()->operatorToKind(ops[i]);
1044         Expr body = getExprManager()->mkExpr(sk, children);
1045         // replace by lambda
1046         ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
1047         Debug("parser-sygus") << "  ...replace op : " << ops[i] << std::endl;
1048         // callback prints as the expression
1049         spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs);
1050       }
1051       else
1052       {
1053         std::map<Expr, Expr>::iterator it =
1054             d_sygus_let_func_to_body.find(ops[i]);
1055         if (it != d_sygus_let_func_to_body.end())
1056         {
1057           Debug("parser-sygus") << "--> Let expression " << ops[i] << std::endl;
1058           Expr let_body = it->second;
1059           std::vector<Expr> let_args = d_sygus_let_func_to_vars[ops[i]];
1060           unsigned let_num_input_args =
1061               d_sygus_let_func_to_num_input_vars[ops[i]];
1062           // the operator is just the body for the arguments
1063           std::vector<Type> ltypes;
1064           for (unsigned j = 0, size = let_args.size(); j < size; j++)
1065           {
1066             ltypes.push_back(let_args[j].getType());
1067           }
1068           std::vector<Expr> largs;
1069           Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
1070           Expr sbody = let_body.substitute(let_args, largs);
1071           ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, sbody);
1072           Debug("parser-sygus") << "  ...replace op : " << ops[i] << std::endl;
1073           // callback prints as a let expression
1074           spc = std::make_shared<printer::SygusLetExprPrintCallback>(
1075               let_body, let_args, let_num_input_args);
1076         }
1077         else if (ops[i].getType().isBitVector() && ops[i].isConst())
1078         {
1079           Debug("parser-sygus") << "--> Bit-vector constant " << ops[i] << " ("
1080                                 << cnames[i] << ")" << std::endl;
1081           // Since there are multiple output formats for bit-vectors and
1082           // we are required by sygus standards to print in the exact input
1083           // format given by the user, we use a print callback to custom print
1084           // the given name.
1085           spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
1086         }
1087         else if (isDefinedFunction(ops[i]))
1088         {
1089           Debug("parser-sygus") << "--> Defined function " << ops[i]
1090                                 << std::endl;
1091           // turn f into (lammbda (x) (f x))
1092           // in a degenerate case, ops[i] may be a defined constant,
1093           // in which case we do not replace by a lambda.
1094           if (ops[i].getType().isFunction())
1095           {
1096             std::vector<Type> ftypes =
1097                 static_cast<FunctionType>(ops[i].getType()).getArgTypes();
1098             std::vector<Expr> largs;
1099             Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs);
1100             largs.insert(largs.begin(), ops[i]);
1101             Expr body = getExprManager()->mkExpr(kind::APPLY, largs);
1102             ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body);
1103             Debug("parser-sygus") << "  ...replace op : " << ops[i]
1104                                   << std::endl;
1105           }
1106           else
1107           {
1108             ops[i] = getExprManager()->mkExpr(kind::APPLY, ops[i]);
1109             Debug("parser-sygus") << "  ...replace op : " << ops[i]
1110                                   << std::endl;
1111           }
1112           // keep a callback to say it should be printed with the defined name
1113           spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
1114         }
1115         else
1116         {
1117           Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl;
1118         }
1119       }
1120       // must rename to avoid duplication
1121       std::stringstream ss;
1122       ss << dt.getName() << "_" << i << "_" << cnames[i];
1123       cnames[i] = ss.str();
1124       // add the sygus constructor
1125       dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc);
1126     }
1127   }
1128
1129   Debug("parser-sygus") << "  add constructors for unresolved symbols..." << std::endl;
1130   if( !unresolved_gterm_sym.empty() ){
1131     std::vector< Type > types;
1132     Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl;
1133     for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){
1134       Debug("parser-sygus") << "  resolve : " << unresolved_gterm_sym[i] << std::endl;
1135       if( isUnresolvedType(unresolved_gterm_sym[i]) ){
1136         Debug("parser-sygus") << "    it is an unresolved type." << std::endl;
1137         Type t = getSort(unresolved_gterm_sym[i]);
1138         if( std::find( types.begin(), types.end(), t )==types.end() ){
1139           types.push_back( t );
1140           //identity element
1141           Type bt = dt.getSygusType();
1142           Debug("parser-sygus") << ":  make identity function for " << bt << ", argument type " << t << std::endl;
1143
1144           std::stringstream ss;
1145           ss << t << "_x";
1146           Expr var = mkBoundVar(ss.str(), bt);
1147           std::vector<Expr> lchildren;
1148           lchildren.push_back(
1149               getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var));
1150           lchildren.push_back(var);
1151           Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren);
1152
1153           // empty sygus callback (should not be printed)
1154           std::shared_ptr<SygusPrintCallback> sepc =
1155               std::make_shared<printer::SygusEmptyPrintCallback>();
1156
1157           //make the sygus argument list
1158           std::vector< Type > id_carg;
1159           id_carg.push_back( t );
1160           dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc);
1161
1162           //add to operators
1163           ops.push_back( id_op );
1164         }
1165       }else{
1166         Debug("parser-sygus") << "    ignore. (likely a free let variable)" << std::endl;
1167       }
1168     }
1169   }
1170 }
1171
1172 Expr Smt2::makeSygusBoundVarList(Datatype& dt,
1173                                  unsigned i,
1174                                  const std::vector<Type>& ltypes,
1175                                  std::vector<Expr>& lvars)
1176 {
1177   for (unsigned j = 0, size = ltypes.size(); j < size; j++)
1178   {
1179     std::stringstream ss;
1180     ss << dt.getName() << "_x_" << i << "_" << j;
1181     Expr v = mkBoundVar(ss.str(), ltypes[j]);
1182     lvars.push_back(v);
1183   }
1184   return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars);
1185 }
1186
1187 const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
1188   for( unsigned i=0; i<d_sygusVars.size(); i++ ){
1189     Expr v = d_sygusVars[i];
1190     std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v );
1191     if( it!=d_sygusVarPrimed.end() ){
1192       if( it->second==isPrimed ){
1193         vars.push_back( v );
1194       }
1195     }else{
1196       //should never happen
1197     }
1198   }
1199 }
1200
1201 const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){
1202   // When constructing the synthesis conjecture, we quantify on the
1203   // (higher-order) bound variable synth_fun.
1204   d_sygusFunSymbols.push_back(synth_fun);
1205
1206   // Variable "sfproxy" carries the type, which may be a SyGuS datatype
1207   // that corresponds to syntactic restrictions.
1208   Expr sym = mkBoundVar("sfproxy", t);
1209   std::vector< Expr > attr_value;
1210   attr_value.push_back(sym);
1211   Command* cattr =
1212       new SetUserAttributeCommand("sygus-synth-grammar", synth_fun, attr_value);
1213   cattr->setMuted(true);
1214   preemptCommand(cattr);
1215 }
1216
1217 }/* CVC4::parser namespace */
1218 }/* CVC4 namespace */