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