src/parser/smt2/smt2.cpp

   1 /*********************                                                        */
   2 /*! \file smt2.cpp
   3  ** \verbatim
   4  ** Original author: Christopher L. Conway
   5  ** Major contributors: Kshitij Bansal, Morgan Deters
   6  ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett, Tianyi Liang
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Definitions of SMT2 constants.
  13  **
  14  ** Definitions of SMT2 constants.
  15  **/
  16
  17 #include "expr/type.h"
  18 #include "expr/command.h"
  19 #include "parser/parser.h"
  20 #include "parser/smt1/smt1.h"
  21 #include "parser/smt2/smt2.h"
  22 #include "parser/antlr_input.h"
  23
  24 #include "util/bitvector.h"
  25
  26 // ANTLR defines these, which is really bad!
  27 #undef true
  28 #undef false
  29
  30 namespace CVC4 {
  31 namespace parser {
  32
  33 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
  34   Parser(exprManager,input,strictMode,parseOnly),
  35   d_logicSet(false),
  36   d_nextSygusFun(0) {
  37   d_unsatCoreNames.push(std::map<Expr, std::string>());
  38   if( !strictModeEnabled() ) {
  39     addTheory(Smt2::THEORY_CORE);
  40   }
  41 }
  42
  43 void Smt2::addArithmeticOperators() {
  44   Parser::addOperator(kind::PLUS);
  45   Parser::addOperator(kind::MINUS);
  46   Parser::addOperator(kind::UMINUS);
  47   Parser::addOperator(kind::MULT);
  48   Parser::addOperator(kind::LT);
  49   Parser::addOperator(kind::LEQ);
  50   Parser::addOperator(kind::GT);
  51   Parser::addOperator(kind::GEQ);
  52 }
  53
  54 void Smt2::addBitvectorOperators() {
  55   addOperator(kind::BITVECTOR_CONCAT, "concat");
  56   addOperator(kind::BITVECTOR_NOT, "bvnot");
  57   addOperator(kind::BITVECTOR_AND, "bvand");
  58   addOperator(kind::BITVECTOR_OR, "bvor");
  59   addOperator(kind::BITVECTOR_NEG, "bvneg");
  60   addOperator(kind::BITVECTOR_PLUS, "bvadd");
  61   addOperator(kind::BITVECTOR_MULT, "bvmul");
  62   addOperator(kind::BITVECTOR_UDIV, "bvudiv");
  63   addOperator(kind::BITVECTOR_UREM, "bvurem");
  64   addOperator(kind::BITVECTOR_SHL, "bvshl");
  65   addOperator(kind::BITVECTOR_LSHR, "bvlshr");
  66   addOperator(kind::BITVECTOR_ULT, "bvult");
  67   addOperator(kind::BITVECTOR_NAND, "bvnand");
  68   addOperator(kind::BITVECTOR_NOR, "bvnor");
  69   addOperator(kind::BITVECTOR_XOR, "bvxor");
  70   addOperator(kind::BITVECTOR_XNOR, "bvxnor");
  71   addOperator(kind::BITVECTOR_COMP, "bvcomp");
  72   addOperator(kind::BITVECTOR_SUB, "bvsub");
  73   addOperator(kind::BITVECTOR_SDIV, "bvsdiv");
  74   addOperator(kind::BITVECTOR_SREM, "bvsrem");
  75   addOperator(kind::BITVECTOR_SMOD, "bvsmod");
  76   addOperator(kind::BITVECTOR_ASHR, "bvashr");
  77   addOperator(kind::BITVECTOR_ULE, "bvule");
  78   addOperator(kind::BITVECTOR_UGT, "bvugt");
  79   addOperator(kind::BITVECTOR_UGE, "bvuge");
  80   addOperator(kind::BITVECTOR_SLT, "bvslt");
  81   addOperator(kind::BITVECTOR_SLE, "bvsle");
  82   addOperator(kind::BITVECTOR_SGT, "bvsgt");
  83   addOperator(kind::BITVECTOR_SGE, "bvsge");
  84   addOperator(kind::BITVECTOR_REDOR, "bvredor");
  85   addOperator(kind::BITVECTOR_REDAND, "bvredand");
  86
  87   Parser::addOperator(kind::BITVECTOR_BITOF);
  88   Parser::addOperator(kind::BITVECTOR_EXTRACT);
  89   Parser::addOperator(kind::BITVECTOR_REPEAT);
  90   Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND);
  91   Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND);
  92   Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT);
  93   Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT);
  94
  95   Parser::addOperator(kind::INT_TO_BITVECTOR);
  96   Parser::addOperator(kind::BITVECTOR_TO_NAT);
  97 }
  98
  99 void Smt2::addStringOperators() {
 100   addOperator(kind::STRING_CONCAT, "str.++");
 101   addOperator(kind::STRING_LENGTH, "str.len");
 102   addOperator(kind::STRING_SUBSTR, "str.substr" );
 103   addOperator(kind::STRING_STRCTN, "str.contains" );
 104   addOperator(kind::STRING_CHARAT, "str.at" );
 105   addOperator(kind::STRING_STRIDOF, "str.indexof" );
 106   addOperator(kind::STRING_STRREPL, "str.replace" );
 107   addOperator(kind::STRING_PREFIX, "str.prefixof" );
 108   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
 109   addOperator(kind::STRING_ITOS, "int.to.str" );
 110   addOperator(kind::STRING_STOI, "str.to.int" );
 111   addOperator(kind::STRING_U16TOS, "u16.to.str" );
 112   addOperator(kind::STRING_STOU16, "str.to.u16" );
 113   addOperator(kind::STRING_U32TOS, "u32.to.str" );
 114   addOperator(kind::STRING_STOU32, "str.to.u32" );
 115   addOperator(kind::STRING_IN_REGEXP, "str.in.re");
 116   addOperator(kind::STRING_TO_REGEXP, "str.to.re");
 117   addOperator(kind::REGEXP_CONCAT, "re.++");
 118   addOperator(kind::REGEXP_UNION, "re.union");
 119   addOperator(kind::REGEXP_INTER, "re.inter");
 120   addOperator(kind::REGEXP_STAR, "re.*");
 121   addOperator(kind::REGEXP_PLUS, "re.+");
 122   addOperator(kind::REGEXP_OPT, "re.opt");
 123   addOperator(kind::REGEXP_RANGE, "re.range");
 124   addOperator(kind::REGEXP_LOOP, "re.loop");
 125 }
 126
 127 void Smt2::addFloatingPointOperators() {
 128   addOperator(kind::FLOATINGPOINT_FP, "fp");
 129   addOperator(kind::FLOATINGPOINT_EQ, "fp.eq");
 130   addOperator(kind::FLOATINGPOINT_ABS, "fp.abs");
 131   addOperator(kind::FLOATINGPOINT_NEG, "fp.neg");
 132   addOperator(kind::FLOATINGPOINT_PLUS, "fp.add");
 133   addOperator(kind::FLOATINGPOINT_SUB, "fp.sub");
 134   addOperator(kind::FLOATINGPOINT_MULT, "fp.mul");
 135   addOperator(kind::FLOATINGPOINT_DIV, "fp.div");
 136   addOperator(kind::FLOATINGPOINT_FMA, "fp.fma");
 137   addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt");
 138   addOperator(kind::FLOATINGPOINT_REM, "fp.rem");
 139   addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral");
 140   addOperator(kind::FLOATINGPOINT_MIN, "fp.min");
 141   addOperator(kind::FLOATINGPOINT_MAX, "fp.max");
 142   addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq");
 143   addOperator(kind::FLOATINGPOINT_LT, "fp.lt");
 144   addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq");
 145   addOperator(kind::FLOATINGPOINT_GT, "fp.gt");
 146   addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal");
 147   addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal");
 148   addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero");
 149   addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite");
 150   addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN");
 151   addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative");
 152   addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
 153   addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
 154
 155   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
 156   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
 157   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL);
 158   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
 159   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
 160   Parser::addOperator(kind::FLOATINGPOINT_TO_UBV);
 161   Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
 162 }
 163
 164
 165 void Smt2::addTheory(Theory theory) {
 166   switch(theory) {
 167   case THEORY_ARRAYS:
 168     addOperator(kind::SELECT, "select");
 169     addOperator(kind::STORE, "store");
 170     break;
 171
 172   case THEORY_BITVECTORS:
 173     addBitvectorOperators();
 174     break;
 175
 176   case THEORY_CORE:
 177     defineType("Bool", getExprManager()->booleanType());
 178     defineVar("true", getExprManager()->mkConst(true));
 179     defineVar("false", getExprManager()->mkConst(false));
 180     Parser::addOperator(kind::AND);
 181     Parser::addOperator(kind::DISTINCT);
 182     Parser::addOperator(kind::EQUAL);
 183     Parser::addOperator(kind::IFF);
 184     Parser::addOperator(kind::IMPLIES);
 185     Parser::addOperator(kind::ITE);
 186     Parser::addOperator(kind::NOT);
 187     Parser::addOperator(kind::OR);
 188     Parser::addOperator(kind::XOR);
 189     break;
 190
 191   case THEORY_REALS_INTS:
 192     defineType("Real", getExprManager()->realType());
 193     Parser::addOperator(kind::DIVISION);
 194     addOperator(kind::TO_INTEGER, "to_int");
 195     addOperator(kind::IS_INTEGER, "is_int");
 196     addOperator(kind::TO_REAL, "to_real");
 197     // falling through on purpose, to add Ints part of Reals_Ints
 198   case THEORY_INTS:
 199     defineType("Int", getExprManager()->integerType());
 200     addArithmeticOperators();
 201     addOperator(kind::INTS_DIVISION, "div");
 202     addOperator(kind::INTS_MODULUS, "mod");
 203     addOperator(kind::ABS, "abs");
 204     Parser::addOperator(kind::DIVISIBLE);
 205     break;
 206
 207   case THEORY_REALS:
 208     defineType("Real", getExprManager()->realType());
 209     addArithmeticOperators();
 210     Parser::addOperator(kind::DIVISION);
 211     break;
 212
 213   case THEORY_QUANTIFIERS:
 214     break;
 215
 216   case THEORY_SETS:
 217     addOperator(kind::UNION, "union");
 218     addOperator(kind::INTERSECTION, "intersection");
 219     addOperator(kind::SETMINUS, "setminus");
 220     addOperator(kind::SUBSET, "subset");
 221     addOperator(kind::MEMBER, "member");
 222     addOperator(kind::SINGLETON, "singleton");
 223     addOperator(kind::INSERT, "insert");
 224     break;
 225
 226   case THEORY_DATATYPES:
 227     Parser::addOperator(kind::APPLY_CONSTRUCTOR);
 228     Parser::addOperator(kind::APPLY_TESTER);
 229     Parser::addOperator(kind::APPLY_SELECTOR);
 230     Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
 231     break;
 232
 233   case THEORY_STRINGS:
 234     defineType("String", getExprManager()->stringType());
 235     defineType("Int", getExprManager()->integerType());
 236     addStringOperators();
 237     break;
 238
 239   case THEORY_UF:
 240     Parser::addOperator(kind::APPLY_UF);
 241     break;
 242
 243   case THEORY_FP:
 244     defineType("RoundingMode", getExprManager()->roundingModeType());
 245     defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
 246     defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
 247     defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
 248     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
 249     addFloatingPointOperators();
 250     break;
 251
 252   default:
 253     std::stringstream ss;
 254     ss << "internal error: unsupported theory " << theory;
 255     throw ParserException(ss.str());
 256   }
 257 }
 258
 259 void Smt2::addOperator(Kind kind, const std::string& name) {
 260   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 261                   << std::endl;
 262   Parser::addOperator(kind);
 263   operatorKindMap[name] = kind;
 264 }
 265
 266 Kind Smt2::getOperatorKind(const std::string& name) const {
 267   // precondition: isOperatorEnabled(name)
 268   return operatorKindMap.find(name)->second;
 269 }
 270
 271 bool Smt2::isOperatorEnabled(const std::string& name) const {
 272   return operatorKindMap.find(name) != operatorKindMap.end();
 273 }
 274
 275 bool Smt2::isTheoryEnabled(Theory theory) const {
 276   switch(theory) {
 277   case THEORY_ARRAYS:
 278     return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
 279   case THEORY_BITVECTORS:
 280     return d_logic.isTheoryEnabled(theory::THEORY_BV);
 281   case THEORY_CORE:
 282     return true;
 283   case THEORY_DATATYPES:
 284     return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
 285   case THEORY_INTS:
 286     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 287       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
 288   case THEORY_REALS:
 289     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 290       ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
 291   case THEORY_REALS_INTS:
 292     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 293       d_logic.areIntegersUsed() && d_logic.areRealsUsed();
 294   case THEORY_QUANTIFIERS:
 295     return d_logic.isQuantified();
 296   case THEORY_SETS:
 297     return d_logic.isTheoryEnabled(theory::THEORY_SETS);
 298   case THEORY_STRINGS:
 299     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
 300   case THEORY_UF:
 301     return d_logic.isTheoryEnabled(theory::THEORY_UF);
 302   case THEORY_FP:
 303     return d_logic.isTheoryEnabled(theory::THEORY_FP);
 304   default:
 305     std::stringstream ss;
 306     ss << "internal error: unsupported theory " << theory;
 307     throw ParserException(ss.str());
 308   }
 309 }
 310
 311 bool Smt2::logicIsSet() {
 312   return d_logicSet;
 313 }
 314
 315 void Smt2::reset() {
 316   d_logicSet = false;
 317   d_logic = LogicInfo();
 318   operatorKindMap.clear();
 319   d_lastNamedTerm = std::pair<Expr, std::string>();
 320   d_unsatCoreNames = std::stack< std::map<Expr, std::string> >();
 321   this->Parser::reset();
 322
 323   d_unsatCoreNames.push(std::map<Expr, std::string>());
 324   if( !strictModeEnabled() ) {
 325     addTheory(Smt2::THEORY_CORE);
 326   }
 327 }
 328
 329 void Smt2::resetAssertions() {
 330   this->Parser::reset();
 331 }
 332
 333 void Smt2::setLogic(std::string name) {
 334   if(sygus()) {
 335     if(name == "Arrays") {
 336       name = "AUF";
 337     } else if(name == "Reals") {
 338       name = "UFLRA";
 339     } else if(name == "LIA") {
 340       name = "UFLIA";
 341     } else if(name == "LRA") {
 342       name = "UFLRA";
 343     } else if(name == "LIRA") {
 344       name = "UFLIRA";
 345     } else if(name == "BV") {
 346       name = "UFBV";
 347     } else {
 348       std::stringstream ss;
 349       ss << "Unknown SyGuS background logic `" << name << "'";
 350       parseError(ss.str());
 351     }
 352   }
 353
 354   d_logicSet = true;
 355   if(logicIsForced()) {
 356     d_logic = getForcedLogic();
 357   } else {
 358     d_logic = name;
 359   }
 360
 361   // Core theory belongs to every logic
 362   addTheory(THEORY_CORE);
 363
 364   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 365     addTheory(THEORY_UF);
 366   }
 367
 368   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 369     if(d_logic.areIntegersUsed()) {
 370       if(d_logic.areRealsUsed()) {
 371         addTheory(THEORY_REALS_INTS);
 372       } else {
 373         addTheory(THEORY_INTS);
 374       }
 375     } else if(d_logic.areRealsUsed()) {
 376       addTheory(THEORY_REALS);
 377     }
 378   }
 379
 380   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
 381     addTheory(THEORY_ARRAYS);
 382   }
 383
 384   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 385     addTheory(THEORY_BITVECTORS);
 386   }
 387
 388   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
 389     addTheory(THEORY_DATATYPES);
 390   }
 391
 392   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 393     addTheory(THEORY_SETS);
 394   }
 395
 396   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 397     addTheory(THEORY_STRINGS);
 398   }
 399
 400   if(d_logic.isQuantified()) {
 401     addTheory(THEORY_QUANTIFIERS);
 402   }
 403
 404   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
 405     addTheory(THEORY_FP);
 406   }
 407
 408 }/* Smt2::setLogic() */
 409
 410 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 411   // TODO: ???
 412 }
 413
 414 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 415   // TODO: ???
 416 }
 417
 418 void Smt2::checkThatLogicIsSet() {
 419   if( ! logicIsSet() ) {
 420     if(strictModeEnabled()) {
 421       parseError("set-logic must appear before this point.");
 422     } else {
 423       if(sygus()) {
 424         setLogic("LIA");
 425       } else {
 426         warning("No set-logic command was given before this point.");
 427         warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
 428         warning("Consider setting a stricter logic for (likely) better performance.");
 429         warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 430
 431         setLogic("ALL_SUPPORTED");
 432       }
 433
 434       Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
 435       c->setMuted(true);
 436       preemptCommand(c);
 437     }
 438   }
 439 }
 440
 441 /* The include are managed in the lexer but called in the parser */
 442 // Inspired by http://www.antlr3.org/api/C/interop.html
 443
 444 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 445   Debug("parser") << "Including " << filename << std::endl;
 446   // Create a new input stream and take advantage of built in stream stacking
 447   // in C target runtime.
 448   //
 449   pANTLR3_INPUT_STREAM    in;
 450 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 451   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 452 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 453   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 454 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 455   if( in == NULL ) {
 456     Debug("parser") << "Can't open " << filename << std::endl;
 457     return false;
 458   }
 459   // Same thing as the predefined PUSHSTREAM(in);
 460   lexer->pushCharStream(lexer, in);
 461   // restart it
 462   //lexer->rec->state->tokenStartCharIndex      = -10;
 463   //lexer->emit(lexer);
 464
 465   // Note that the input stream is not closed when it EOFs, I don't bother
 466   // to do it here, but it is up to you to track streams created like this
 467   // and destroy them when the whole parse session is complete. Remember that you
 468   // don't want to do this until all tokens have been manipulated all the way through
 469   // your tree parsers etc as the token does not store the text it just refers
 470   // back to the input stream and trying to get the text for it will abort if you
 471   // close the input stream too early.
 472
 473   //TODO what said before
 474   return true;
 475 }
 476
 477 void Smt2::includeFile(const std::string& filename) {
 478   // security for online version
 479   if(!canIncludeFile()) {
 480     parseError("include-file feature was disabled for this run.");
 481   }
 482
 483   // Get the lexer
 484   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 485   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 486   // get the name of the current stream "Does it work inside an include?"
 487   const std::string inputName = ai->getInputStreamName();
 488
 489   // Find the directory of the current input file
 490   std::string path;
 491   size_t pos = inputName.rfind('/');
 492   if(pos != std::string::npos) {
 493     path = std::string(inputName, 0, pos + 1);
 494   }
 495   path.append(filename);
 496   if(!newInputStream(path, lexer)) {
 497     parseError("Couldn't open include file `" + path + "'");
 498   }
 499 }
 500
 501 Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) {
 502   Expr e = mkBoundVar(name, type);
 503   d_sygusVars.push_back(e);
 504   d_sygusVarPrimed[e] = false;
 505   if( isPrimed ){
 506     std::stringstream ss;
 507     ss << name << "'";
 508     Expr ep = mkBoundVar(ss.str(), type);
 509     d_sygusVars.push_back(ep);
 510     d_sygusVarPrimed[ep] = true;
 511   }
 512   return e;
 513 }
 514
 515 void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
 516                                   std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ) {
 517   startIndex = -1;
 518   Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl;
 519   std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
 520
 521   std::vector< Type > types;
 522   for( unsigned i=0; i<sygus_vars.size(); i++ ){
 523     Type t = sygus_vars[i].getType();
 524     if( !t.isBoolean() && std::find( types.begin(), types.end(), t )==types.end() ){
 525       types.push_back( t );
 526     }
 527   }
 528
 529   //name of boolean sort
 530   std::stringstream ssb;
 531   ssb << fun << "_Bool";
 532   std::string dbname = ssb.str();
 533   Type unres_bt = mkUnresolvedType(ssb.str());
 534
 535   std::vector< Type > unres_types;
 536   for( unsigned i=0; i<types.size(); i++ ){
 537     std::stringstream ss;
 538     ss << fun << "_" << types[i];
 539     std::string dname = ss.str();
 540     datatypes.push_back(Datatype(dname));
 541     ops.push_back(std::vector<Expr>());
 542     std::vector<std::string> cnames;
 543     std::vector<std::vector<CVC4::Type> > cargs;
 544     std::vector<std::string> unresolved_gterm_sym;
 545     //make unresolved type
 546     Type unres_t = mkUnresolvedType(dname);
 547     unres_types.push_back(unres_t);
 548     //add variables
 549     for( unsigned j=0; j<sygus_vars.size(); j++ ){
 550       if( sygus_vars[j].getType()==types[i] ){
 551         std::stringstream ss;
 552         ss << sygus_vars[j];
 553         Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
 554         ops.back().push_back( sygus_vars[j] );
 555         cnames.push_back( ss.str() );
 556         cargs.push_back( std::vector< CVC4::Type >() );
 557       }
 558     }
 559     //add constants
 560     std::vector< Expr > consts;
 561     mkSygusConstantsForType( types[i], consts );
 562     for( unsigned j=0; j<consts.size(); j++ ){
 563       std::stringstream ss;
 564       ss << consts[j];
 565       Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
 566       ops.back().push_back( consts[j] );
 567       cnames.push_back( ss.str() );
 568       cargs.push_back( std::vector< CVC4::Type >() );
 569     }
 570     //ITE
 571     CVC4::Kind k = kind::ITE;
 572     Debug("parser-sygus") << "...add for " << k << std::endl;
 573     ops.back().push_back(getExprManager()->operatorOf(k));
 574     cnames.push_back( kind::kindToString(k) );
 575     cargs.push_back( std::vector< CVC4::Type >() );
 576     cargs.back().push_back(unres_bt);
 577     cargs.back().push_back(unres_t);
 578     cargs.back().push_back(unres_t);
 579
 580     if( types[i].isInteger() ){
 581       for( unsigned j=0; j<2; j++ ){
 582         CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS;
 583         Debug("parser-sygus") << "...add for " << k << std::endl;
 584         ops.back().push_back(getExprManager()->operatorOf(k));
 585         cnames.push_back(kind::kindToString(k));
 586         cargs.push_back( std::vector< CVC4::Type >() );
 587         cargs.back().push_back(unres_t);
 588         cargs.back().push_back(unres_t);
 589       }
 590     }else{
 591       std::stringstream sserr;
 592       sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
 593       warning(sserr.str());
 594     }
 595     Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
 596     datatypes.back().setSygus( types[i], bvl, true, true );
 597     mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
 598     sorts.push_back( types[i] );
 599     //set start index if applicable
 600     if( types[i]==range ){
 601       startIndex = i;
 602     }
 603   }
 604
 605   //make Boolean type
 606   Type btype = getExprManager()->booleanType();
 607   datatypes.push_back(Datatype(dbname));
 608   ops.push_back(std::vector<Expr>());
 609   std::vector<std::string> cnames;
 610   std::vector<std::vector<CVC4::Type> > cargs;
 611   std::vector<std::string> unresolved_gterm_sym;
 612   //add variables
 613   for( unsigned i=0; i<sygus_vars.size(); i++ ){
 614     if( sygus_vars[i].getType().isBoolean() ){
 615       std::stringstream ss;
 616       ss << sygus_vars[i];
 617       Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
 618       ops.back().push_back( sygus_vars[i] );
 619       cnames.push_back( ss.str() );
 620       cargs.push_back( std::vector< CVC4::Type >() );
 621     }
 622   }
 623   //add constants if no variables and no connected types
 624   if( ops.back().empty() && types.empty() ){
 625     std::vector< Expr > consts;
 626     mkSygusConstantsForType( btype, consts );
 627     for( unsigned j=0; j<consts.size(); j++ ){
 628       std::stringstream ss;
 629       ss << consts[j];
 630       Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
 631       ops.back().push_back( consts[j] );
 632       cnames.push_back( ss.str() );
 633       cargs.push_back( std::vector< CVC4::Type >() );
 634     }
 635   }
 636   //add operators
 637   for( unsigned i=0; i<3; i++ ){
 638     CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : kind::OR );
 639     Debug("parser-sygus") << "...add for " << k << std::endl;
 640     ops.back().push_back(getExprManager()->operatorOf(k));
 641     cnames.push_back(kind::kindToString(k));
 642     cargs.push_back( std::vector< CVC4::Type >() );
 643     if( k==kind::NOT ){
 644       cargs.back().push_back(unres_bt);
 645     }else if( k==kind::AND || k==kind::OR ){
 646       cargs.back().push_back(unres_bt);
 647       cargs.back().push_back(unres_bt);
 648     }
 649   }
 650   //add predicates for types
 651   for( unsigned i=0; i<types.size(); i++ ){
 652     //add equality per type
 653     CVC4::Kind k = kind::EQUAL;
 654     Debug("parser-sygus") << "...add for " << k << std::endl;
 655     ops.back().push_back(getExprManager()->operatorOf(k));
 656     std::stringstream ss;
 657     ss << kind::kindToString(k) << "_" << types[i];
 658     cnames.push_back(ss.str());
 659     cargs.push_back( std::vector< CVC4::Type >() );
 660     cargs.back().push_back(unres_types[i]);
 661     cargs.back().push_back(unres_types[i]);
 662     //type specific predicates
 663     if( types[i].isInteger() ){
 664       CVC4::Kind k = kind::LEQ;
 665       Debug("parser-sygus") << "...add for " << k << std::endl;
 666       ops.back().push_back(getExprManager()->operatorOf(k));
 667       cnames.push_back(kind::kindToString(k));
 668       cargs.push_back( std::vector< CVC4::Type >() );
 669       cargs.back().push_back(unres_types[i]);
 670       cargs.back().push_back(unres_types[i]);
 671     }
 672   }
 673   if( range==btype ){
 674     startIndex = sorts.size();
 675   }
 676   Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
 677   datatypes.back().setSygus( btype, bvl, true, true );
 678   mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
 679   sorts.push_back( btype );
 680
 681   Debug("parser-sygus") << "...finished make default grammar for " << fun << " " << range << std::endl;
 682 }
 683
 684 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
 685   if( type.isInteger() ){
 686     ops.push_back(getExprManager()->mkConst(Rational(0)));
 687     ops.push_back(getExprManager()->mkConst(Rational(1)));
 688   }else if( type.isBitVector() ){
 689     unsigned sz = ((BitVectorType)type).getSize();
 690     BitVector bval0(sz, (unsigned int)0);
 691     ops.push_back( getExprManager()->mkConst(bval0) );
 692     BitVector bval1(sz, (unsigned int)1);
 693     ops.push_back( getExprManager()->mkConst(bval1) );
 694   }else if( type.isBoolean() ){
 695     ops.push_back(getExprManager()->mkConst(true));
 696     ops.push_back(getExprManager()->mkConst(false));
 697   }
 698   //TODO : others?
 699 }
 700
 701 //  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)
 702 //  This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
 703 void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
 704                               std::vector< CVC4::Datatype >& datatypes,
 705                               std::vector< CVC4::Type>& sorts,
 706                               std::vector< std::vector<CVC4::Expr> >& ops,
 707                               std::vector< std::vector<std::string> >& cnames,
 708                               std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 709                               std::vector< bool >& allow_const,
 710                               std::vector< std::vector< std::string > >& unresolved_gterm_sym,
 711                               std::vector<CVC4::Expr>& sygus_vars,
 712                               std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
 713                               CVC4::Type& ret, bool isNested ){
 714   if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){
 715     Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index << std::endl;
 716     //convert to UMINUS if one child of -
 717     if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){
 718       sgt.d_expr = getExprManager()->operatorOf(kind::UMINUS);
 719     }
 720     ops[index].push_back( sgt.d_expr );
 721     cnames[index].push_back( sgt.d_name );
 722     cargs[index].push_back( std::vector< CVC4::Type >() );
 723     for( unsigned i=0; i<sgt.d_children.size(); i++ ){
 724       std::stringstream ss;
 725       ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
 726       std::string sub_dname = ss.str();
 727       //add datatype for child
 728       Type null_type;
 729       pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
 730       int sub_dt_index = datatypes.size()-1;
 731       //process child
 732       Type sub_ret;
 733       processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
 734                          sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
 735       //process the nested gterm (either pop the last datatype, or flatten the argument)
 736       Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
 737                                          sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
 738       cargs[index].back().push_back(tt);
 739     }
 740     //if let, must create operator
 741     if( sgt.d_gterm_type==SygusGTerm::gterm_let ){
 742       processSygusLetConstructor( sgt.d_let_vars, index, datatypes, sorts, ops, cnames, cargs,
 743                                   sygus_vars, sygus_to_builtin, sygus_to_builtin_expr );
 744     }
 745   }else if( sgt.d_gterm_type==SygusGTerm::gterm_constant ){
 746     if( sgt.getNumChildren()!=0 ){
 747       parseError("Bad syntax for Sygus Constant.");
 748     }
 749     std::vector< Expr > consts;
 750     mkSygusConstantsForType( sgt.d_type, consts );
 751     Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
 752     for( unsigned i=0; i<consts.size(); i++ ){
 753       std::stringstream ss;
 754       ss << consts[i];
 755       Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
 756       ops[index].push_back( consts[i] );
 757       cnames[index].push_back( ss.str() );
 758       cargs[index].push_back( std::vector< CVC4::Type >() );
 759     }
 760     allow_const[index] = true;
 761   }else if( sgt.d_gterm_type==SygusGTerm::gterm_variable || sgt.d_gterm_type==SygusGTerm::gterm_input_variable ){
 762     if( sgt.getNumChildren()!=0 ){
 763       parseError("Bad syntax for Sygus Variable.");
 764     }
 765     Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl;
 766     for( unsigned i=0; i<sygus_vars.size(); i++ ){
 767       if( sygus_vars[i].getType()==sgt.d_type ){
 768         std::stringstream ss;
 769         ss << sygus_vars[i];
 770         Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
 771         ops[index].push_back( sygus_vars[i] );
 772         cnames[index].push_back( ss.str() );
 773         cargs[index].push_back( std::vector< CVC4::Type >() );
 774       }
 775     }
 776   }else if( sgt.d_gterm_type==SygusGTerm::gterm_nested_sort ){
 777     ret = sgt.d_type;
 778   }else if( sgt.d_gterm_type==SygusGTerm::gterm_unresolved ){
 779     if( isNested ){
 780       if( isUnresolvedType(sgt.d_name) ){
 781         ret = getSort(sgt.d_name);
 782       }else{
 783         //nested, unresolved symbol...fail
 784         std::stringstream ss;
 785         ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl;
 786         parseError(ss.str());
 787       }
 788     }else{
 789       //will resolve when adding constructors
 790       unresolved_gterm_sym[index].push_back(sgt.d_name);
 791     }
 792   }else if( sgt.d_gterm_type==SygusGTerm::gterm_ignore ){
 793
 794   }
 795 }
 796
 797 bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
 798                                   std::vector< CVC4::Datatype >& datatypes,
 799                                   std::vector< CVC4::Type>& sorts,
 800                                   std::vector< std::vector<CVC4::Expr> >& ops,
 801                                   std::vector< std::vector<std::string> >& cnames,
 802                                   std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 803                                   std::vector< bool >& allow_const,
 804                                   std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
 805   sorts.push_back(t);
 806   datatypes.push_back(Datatype(dname));
 807   ops.push_back(std::vector<Expr>());
 808   cnames.push_back(std::vector<std::string>());
 809   cargs.push_back(std::vector<std::vector<CVC4::Type> >());
 810   allow_const.push_back(false);
 811   unresolved_gterm_sym.push_back(std::vector< std::string >());
 812   return true;
 813 }
 814
 815 bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
 816                                  std::vector< CVC4::Type>& sorts,
 817                                  std::vector< std::vector<CVC4::Expr> >& ops,
 818                                  std::vector< std::vector<std::string> >& cnames,
 819                                  std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 820                                  std::vector< bool >& allow_const,
 821                                  std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
 822   sorts.pop_back();
 823   datatypes.pop_back();
 824   ops.pop_back();
 825   cnames.pop_back();
 826   cargs.pop_back();
 827   allow_const.pop_back();
 828   unresolved_gterm_sym.pop_back();
 829   return true;
 830 }
 831
 832 Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
 833                                     std::vector< CVC4::Type>& sorts,
 834                                     std::vector< std::vector<CVC4::Expr> >& ops,
 835                                     std::vector< std::vector<std::string> >& cnames,
 836                                     std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 837                                     std::vector< bool >& allow_const,
 838                                     std::vector< std::vector< std::string > >& unresolved_gterm_sym,
 839                                     std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
 840                                     std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) {
 841   Type t = sub_ret;
 842   Debug("parser-sygus") << "Argument is ";
 843   if( t.isNull() ){
 844     //then, it is the datatype we constructed, which should have a single constructor
 845     t = mkUnresolvedType(sub_dname);
 846     Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t << std::endl;
 847     Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs[sub_dt_index].size() << std::endl;
 848     if( cargs[sub_dt_index].empty() ){
 849       parseError(std::string("Internal error : datatype for nested gterm does not have a constructor."));
 850     }
 851     Expr sop = ops[sub_dt_index][0];
 852     Type curr_t;
 853     if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){
 854       curr_t = sop.getType();
 855       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;
 856       sygus_to_builtin_expr[t] = sop;
 857       //store that term sop has dedicated sygus type t
 858       if( d_sygus_bound_var_type.find( sop )==d_sygus_bound_var_type.end() ){
 859         d_sygus_bound_var_type[sop] = t;
 860       }
 861     }else{
 862       std::vector< Expr > children;
 863       if( sop.getKind() != kind::BUILTIN ){
 864         children.push_back( sop );
 865       }
 866       for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
 867         std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
 868         if( it==sygus_to_builtin_expr.end() ){
 869           if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){
 870             std::stringstream ss;
 871             ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl;
 872             ss << "Builtin types are currently : " << std::endl;
 873             for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){
 874               ss << "  " << itb->first << " -> " << itb->second << std::endl;
 875             }
 876             parseError(ss.str());
 877           }
 878           Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
 879           Debug("parser-sygus") << ":  child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
 880           std::stringstream ss;
 881           ss << t << "_x_" << i;
 882           Expr bv = mkBoundVar(ss.str(), bt);
 883           children.push_back( bv );
 884           d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i];
 885         }else{
 886           Debug("parser-sygus") << ":  child " << i << " existing sygus to builtin expr : " << it->second << std::endl;
 887           children.push_back( it->second );
 888         }
 889       }
 890       Kind sk = sop.getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(sop);
 891       Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl;
 892       Expr e = getExprManager()->mkExpr( sk, children );
 893       Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
 894       curr_t = e.getType();
 895       sygus_to_builtin_expr[t] = e;
 896     }
 897     sorts[sub_dt_index] = curr_t;
 898     sygus_to_builtin[t] = curr_t;
 899   }else{
 900     Debug("parser-sygus") << "simple argument " << t << std::endl;
 901     Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl;
 902     //otherwise, datatype was unecessary
 903     //pop argument datatype definition
 904     popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
 905   }
 906   return t;
 907 }
 908
 909 void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
 910                                        int index,
 911                                        std::vector< CVC4::Datatype >& datatypes,
 912                                        std::vector< CVC4::Type>& sorts,
 913                                        std::vector< std::vector<CVC4::Expr> >& ops,
 914                                        std::vector< std::vector<std::string> >& cnames,
 915                                        std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
 916                                        std::vector<CVC4::Expr>& sygus_vars,
 917                                        std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
 918                                        std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ) {
 919   std::vector< CVC4::Expr > let_define_args;
 920   Expr let_body;
 921   int dindex = cargs[index].size()-1;
 922   Debug("parser-sygus") << "Process let constructor for datatype " << datatypes[index].getName() << ", #subtypes = " << cargs[index][dindex].size() << std::endl;
 923   for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
 924     Debug("parser-sygus") << "  " << i << " : " << cargs[index][dindex][i] << std::endl;
 925     if( i+1==cargs[index][dindex].size() ){
 926       std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[index][dindex][i] );
 927       if( it!=sygus_to_builtin_expr.end() ){
 928         let_body = it->second;
 929       }else{
 930         std::stringstream ss;
 931         ss << datatypes[index].getName() << "_body";
 932         let_body = mkBoundVar(ss.str(), sygus_to_builtin[cargs[index][dindex][i]]);
 933         d_sygus_bound_var_type[let_body] = cargs[index][dindex][i];
 934       }
 935     }
 936   }
 937   Debug("parser-sygus") << std::endl;
 938   Debug("parser-sygus") << "Body is " << let_body << std::endl;
 939   Debug("parser-sygus") << "# let vars = " << let_vars.size() << std::endl;
 940   for( unsigned i=0; i<let_vars.size(); i++ ){
 941     Debug("parser-sygus") << "  let var " << i << " : " << let_vars[i] << " " << let_vars[i].getType() << std::endl;
 942     let_define_args.push_back( let_vars[i] );
 943   }
 944   /*
 945   Debug("parser-sygus") << "index = " << index << ", start index = " << start_index << ", #Current datatypes = " << datatypes.size() << std::endl;
 946   for( unsigned i=start_index; i<datatypes.size(); i++ ){
 947     Debug("parser-sygus") << "  datatype " << i << " : " << datatypes[i].getName() << ", #cons = " << cargs[i].size() << std::endl;
 948     if( !cargs[i].empty() ){
 949       Debug("parser-sygus") << "  operator 0 is " << ops[i][0] << std::endl;
 950       Debug("parser-sygus") << "  cons 0 has " << cargs[i][0].size() << " sub fields." << std::endl;
 951       for( unsigned j=0; j<cargs[i][0].size(); j++ ){
 952         Type bt = sygus_to_builtin[cargs[i][0][j]];
 953         Debug("parser-sygus") << "    cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl;
 954       }
 955     }
 956   }
 957   */
 958   //last argument is the return, pop
 959   cargs[index][dindex].pop_back();
 960   collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );
 961
 962   Debug("parser-sygus") << "Make define-fun with " << cargs[index][dindex].size() << " arguments..." << std::endl;
 963   std::vector<CVC4::Type> fsorts;
 964   for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
 965     Debug("parser-sygus") << "  " << i << " : " << let_define_args[i] << " " << let_define_args[i].getType() << " " << cargs[index][dindex][i] << std::endl;
 966     fsorts.push_back(let_define_args[i].getType());
 967   }
 968
 969   Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
 970   std::stringstream ss;
 971   ss << datatypes[index].getName() << "_let";
 972   Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
 973   preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) );
 974
 975   ops[index].pop_back();
 976   ops[index].push_back( let_func );
 977   cnames[index].pop_back();
 978   cnames[index].push_back(ss.str());
 979
 980   //mark function as let constructor
 981   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() );
 982   d_sygus_let_func_to_body[let_func] = let_body;
 983   d_sygus_let_func_to_num_input_vars[let_func] = let_vars.size();
 984 }
 985
 986
 987 void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ) {
 988   if( e.getKind()==kind::BOUND_VARIABLE ){
 989     if( std::find( builtinArgs.begin(), builtinArgs.end(), e )==builtinArgs.end() ){
 990       builtinArgs.push_back( e );
 991       sygusArgs.push_back( d_sygus_bound_var_type[e] );
 992       if( d_sygus_bound_var_type[e].isNull() ){
 993         std::stringstream ss;
 994         ss << "While constructing body of let gterm, can't map " << e << " to sygus type." << std::endl;
 995         parseError(ss.str());
 996       }
 997     }
 998   }else{
 999     for( unsigned i=0; i<e.getNumChildren(); i++ ){
1000       collectSygusLetArgs( e[i], sygusArgs, builtinArgs );
1001     }
1002   }
1003 }
1004
1005 void Smt2::setSygusStartIndex( std::string& fun, int startIndex,
1006                                std::vector< CVC4::Datatype >& datatypes,
1007                                std::vector< CVC4::Type>& sorts,
1008                                std::vector< std::vector<CVC4::Expr> >& ops ) {
1009   if( startIndex>0 ){
1010     CVC4::Datatype tmp_dt = datatypes[0];
1011     Type tmp_sort = sorts[0];
1012     std::vector< Expr > tmp_ops;
1013     tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
1014     datatypes[0] = datatypes[startIndex];
1015     sorts[0] = sorts[startIndex];
1016     ops[0].clear();
1017     ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
1018     datatypes[startIndex] = tmp_dt;
1019     sorts[startIndex] = tmp_sort;
1020     ops[startIndex].clear();
1021     ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
1022   }else if( startIndex<0 ){
1023     std::stringstream ss;
1024     ss << "warning: no symbol named Start for synth-fun " << fun << std::endl;
1025     warning(ss.str());
1026   }
1027 }
1028
1029 void Smt2::defineSygusFuns() {
1030   // only define each one once
1031   while(d_nextSygusFun < d_sygusFuns.size()) {
1032     std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun];
1033     std::string fun = p.first;
1034     Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl;
1035     Expr eval = p.second;
1036     FunctionType evalType = eval.getType();
1037     std::vector<Type> argTypes = evalType.getArgTypes();
1038     Type rangeType = evalType.getRangeType();
1039     Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl;
1040
1041     // first make the function type
1042     std::vector<Expr> sygusVars;
1043     std::vector<Type> funType;
1044     for(size_t j = 1; j < argTypes.size(); ++j) {
1045       funType.push_back(argTypes[j]);
1046       std::stringstream ss;
1047       ss << fun << "_v_" << j;
1048       sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), argTypes[j]));
1049     }
1050     Type funt;
1051     if( !funType.empty() ){
1052       funt = getExprManager()->mkFunctionType(funType, rangeType);
1053       Debug("parser-sygus") << "...eval function type : " << funt << std::endl;
1054
1055       // copy the bound vars
1056       /*
1057       std::vector<Expr> sygusVars;
1058       //std::vector<Type> types;
1059       for(size_t i = 0; i < d_sygusVars.size(); ++i) {
1060         std::stringstream ss;
1061         ss << d_sygusVars[i];
1062         Type type = d_sygusVars[i].getType();
1063         sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
1064         //types.push_back(type);
1065       }
1066       Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
1067       */
1068
1069       //Type t = getExprManager()->mkFunctionType(types, rangeType);
1070       //Debug("parser-sygus") << "...function type : " << t << std::endl;
1071     }else{
1072       funt = rangeType;
1073     }
1074     Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED);
1075     Debug("parser-sygus") << "...made function : " << lambda << std::endl;
1076     std::vector<Expr> applyv;
1077     Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]);
1078     d_sygusFunSymbols.push_back(funbv);
1079     applyv.push_back(eval);
1080     applyv.push_back(funbv);
1081     for(size_t i = 0; i < sygusVars.size(); ++i) {
1082       applyv.push_back(sygusVars[i]);
1083     }
1084     Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv);
1085     Debug("parser-sygus") << "...made apply " << apply << std::endl;
1086     Debug("parser-sygus") << "--> Define " << fun << " as " << lambda << " " << apply << std::endl;
1087     Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply);
1088     preemptCommand(cmd);
1089
1090     ++d_nextSygusFun;
1091   }
1092 }
1093
1094 void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
1095                             std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
1096                             std::vector<std::string>& unresolved_gterm_sym,
1097                             std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
1098   Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
1099   Debug("parser-sygus") << "  add constructors..." << std::endl;
1100   for( int i=0; i<(int)cnames.size(); i++ ){
1101     bool is_dup = false;
1102     bool is_dup_op = false;
1103     Expr let_body;
1104     std::vector< Expr > let_args;
1105     unsigned let_num_input_args = 0;
1106     for( int j=0; j<i; j++ ){
1107       if( ops[i]==ops[j] ){
1108         is_dup_op = true;
1109         if( cargs[i].size()==cargs[j].size() ){
1110           is_dup = true;
1111           for( unsigned k=0; k<cargs[i].size(); k++ ){
1112             if( cargs[i][k]!=cargs[j][k] ){
1113               is_dup = false;
1114               break;
1115             }
1116           }
1117         }
1118         if( is_dup ){
1119           break;
1120         }
1121       }
1122     }
1123     if( is_dup ){
1124       Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << " at " << i << std::endl;
1125       ops.erase( ops.begin() + i, ops.begin() + i + 1 );
1126       cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 );
1127       cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 );
1128       i--;
1129     }else if( is_dup_op ){
1130       Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] << " at " << i << std::endl;
1131       //make into define-fun
1132       std::vector<CVC4::Type> fsorts;
1133       for( unsigned j=0; j<cargs[i].size(); j++ ){
1134         Type bt = sygus_to_builtin[cargs[i][j]];
1135         std::stringstream ss;
1136         ss << dt.getName() << "_x_" << i << "_" << j;
1137         Expr v = mkBoundVar(ss.str(), bt);
1138         let_args.push_back( v );
1139         fsorts.push_back( bt );
1140         Debug("parser-sygus") << ": var " << i << " " << v << " with type " << bt << " from " << cargs[i][j] << std::endl;
1141       }
1142       //make the let_body
1143       std::vector< Expr > children;
1144       if( ops[i].getKind() != kind::BUILTIN ){
1145         children.push_back( ops[i] );
1146       }
1147       children.insert( children.end(), let_args.begin(), let_args.end() );
1148       Kind sk = ops[i].getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(ops[i]);
1149       Debug("parser-sygus") << ": replace " << ops[i] << " " << ops[i].getKind() << " " << sk << std::endl;
1150       let_body = getExprManager()->mkExpr( sk, children );
1151       Debug("parser-sygus") << ": new body of function is " << let_body << std::endl;
1152
1153       Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
1154       Debug("parser-sygus") << ": function type is " << ft << std::endl;
1155       std::stringstream ss;
1156       ss << dt.getName() << "_df_" << i;
1157       //replace operator and name
1158       ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
1159       cnames[i] = ss.str();
1160       preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) );
1161       addSygusDatatypeConstructor( dt, ops[i], cnames[i], cargs[i], let_body, let_args, 0 );
1162     }else{
1163       std::map< CVC4::Expr, CVC4::Expr >::iterator it = d_sygus_let_func_to_body.find( ops[i] );
1164       if( it!=d_sygus_let_func_to_body.end() ){
1165         let_body = it->second;
1166         let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() );
1167         let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]];
1168       }
1169       addSygusDatatypeConstructor( dt, ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args );
1170     }
1171   }
1172   Debug("parser-sygus") << "  add constructors for unresolved symbols..." << std::endl;
1173   if( !unresolved_gterm_sym.empty() ){
1174     std::vector< Type > types;
1175     Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl;
1176     for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){
1177       Debug("parser-sygus") << "  resolve : " << unresolved_gterm_sym[i] << std::endl;
1178       if( isUnresolvedType(unresolved_gterm_sym[i]) ){
1179         Debug("parser-sygus") << "    it is an unresolved type." << std::endl;
1180         Type t = getSort(unresolved_gterm_sym[i]);
1181         if( std::find( types.begin(), types.end(), t )==types.end() ){
1182           types.push_back( t );
1183           //identity element
1184           Type bt = dt.getSygusType();
1185           Debug("parser-sygus") << ":  make identity function for " << bt << ", argument type " << t << std::endl;
1186           std::stringstream ss;
1187           ss << t << "_x_id";
1188           Expr let_body = mkBoundVar(ss.str(), bt);
1189           std::vector< Expr > let_args;
1190           let_args.push_back( let_body );
1191           //make the identity function
1192           Type ft = getExprManager()->mkFunctionType(bt, bt);
1193           std::stringstream ssid;
1194           ssid << unresolved_gterm_sym[i] << "_id";
1195           Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
1196           preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) );
1197           //make the sygus argument list
1198           std::vector< Type > id_carg;
1199           id_carg.push_back( t );
1200           addSygusDatatypeConstructor( dt, id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 );
1201           //add to operators
1202           ops.push_back( id_op );
1203         }
1204       }else{
1205         Debug("parser-sygus") << "    ignore. (likely a free let variable)" << std::endl;
1206       }
1207     }
1208   }
1209
1210 }
1211
1212 void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
1213                                         CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) {
1214   Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt.getName() << std::endl;
1215   if( !let_body.isNull() ){
1216     Debug("parser-sygus") << "    let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl;
1217     //TODO : remove arguments not occurring in body
1218     //if this is a self identity function, ignore
1219     if( let_args.size()==0 && let_args[0]==let_body ){
1220       Debug("parser-sygus") << "    identity function " << cargs[0] << " to " << dt.getName() << std::endl;
1221       //TODO
1222     }
1223   }
1224   std::string name = dt.getName() + "_" + cname;
1225   std::string testerId("is-");
1226   testerId.append(name);
1227   checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
1228   checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
1229   CVC4::DatatypeConstructor c(name, testerId );
1230   c.setSygus( op, let_body, let_args, let_num_input_args );
1231   for( unsigned j=0; j<cargs.size(); j++ ){
1232     std::stringstream sname;
1233     sname << name << "_" << j;
1234     c.addArg(sname.str(), cargs[j]);
1235   }
1236   dt.addConstructor(c);
1237 }
1238
1239
1240 // i is index in datatypes/ops
1241 // j is index is datatype
1242 Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
1243                               std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
1244                               Expr eval, const Datatype& dt, size_t i, size_t j ) {
1245   const DatatypeConstructor& ctor = dt[j];
1246   Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl;
1247   std::vector<Expr> bvs, extraArgs;
1248   for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
1249     std::string vname = "v_" + ctor[k].getName();
1250     Expr bv = getExprManager()->mkBoundVar(vname, SelectorType(ctor[k].getType()).getRangeType());
1251     bvs.push_back(bv);
1252     extraArgs.push_back(bv);
1253   }
1254   if( !terms[0].isNull() ){
1255     bvs.insert(bvs.end(), terms[0].begin(), terms[0].end());
1256   }
1257   Expr bvl;
1258   if( !bvs.empty() ){
1259     bvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, bvs);
1260   }
1261   Debug("parser-sygus") << "...made bv list " << bvl << std::endl;
1262   std::vector<Expr> patv;
1263   patv.push_back(eval);
1264   std::vector<Expr> applyv;
1265   applyv.push_back(ctor.getConstructor());
1266   applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end());
1267   for(size_t k = 0; k < applyv.size(); ++k) {
1268   }
1269   Expr cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
1270   Debug("parser-sygus") << "...made eval ctor apply " << cpatv << std::endl;
1271   patv.push_back(cpatv);
1272   if( !terms[0].isNull() ){
1273     patv.insert(patv.end(), terms[0].begin(), terms[0].end());
1274   }
1275   Expr evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
1276   Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl;
1277   std::vector<Expr> builtApply;
1278   for(size_t k = 0; k < extraArgs.size(); ++k) {
1279     std::vector<Expr> patvb;
1280     patvb.push_back(evals[DatatypeType(extraArgs[k].getType())]);
1281     patvb.push_back(extraArgs[k]);
1282     if( !terms[0].isNull() ){
1283       patvb.insert(patvb.end(), terms[0].begin(), terms[0].end());
1284     }
1285     builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb));
1286   }
1287   for(size_t k = 0; k < builtApply.size(); ++k) {
1288   }
1289   Expr builtTerm;
1290   //if( ops[i][j].getKind() == kind::BUILTIN ){
1291   if( !builtApply.empty() ){
1292     if( ops[i][j].getKind() != kind::BUILTIN ){
1293       builtTerm = getExprManager()->mkExpr(kind::APPLY, ops[i][j], builtApply);
1294     }else{
1295       builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
1296     }
1297   }else{
1298     builtTerm = ops[i][j];
1299   }
1300   Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
1301   Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
1302   if( !bvl.isNull() ){
1303     Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
1304     pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
1305     assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern);
1306   }
1307   Debug("parser-sygus") << "...made assertion " << assertion << std::endl;
1308
1309   //linearize multiplication if possible
1310   if( builtTerm.getKind()==kind::MULT ){
1311     for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
1312       Type at = SelectorType(ctor[k].getType()).getRangeType();
1313       if( at.isDatatype() ){
1314         DatatypeType atd = (DatatypeType)SelectorType(ctor[k].getType()).getRangeType();
1315         Debug("parser-sygus") << "Argument " << k << " " << atd << std::endl;
1316         std::vector<DatatypeType>::iterator itd = std::find( datatypeTypes.begin(), datatypeTypes.end(), atd );
1317         if( itd!=datatypeTypes.end() ){
1318           Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl;
1319           unsigned index = itd-datatypeTypes.begin();
1320           Debug("parser-sygus2") << "index = " << index << std::endl;
1321           bool isConst = true;
1322           for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
1323             Debug("parser-sygus2") << "ops[" << cc << "]=" << ops[index][cc] << std::endl;
1324             if( ops[index][cc].getKind() != kind::CONST_RATIONAL ){
1325               isConst = false;
1326               break;
1327             }
1328           }
1329           if( isConst ){
1330             Debug("parser-sygus") << "Linearize multiplication " << ctor << " based on argument " << k << std::endl;
1331             const Datatype & atdd = atd.getDatatype();
1332             std::vector<Expr> assertions;
1333             std::vector<Expr> nbvs;
1334             for( unsigned a=0; a<bvl.getNumChildren(); a++ ){
1335               if( a!=k ){
1336                 nbvs.push_back( bvl[a] );
1337               }
1338             }
1339             Expr nbvl = getExprManager()->mkExpr( kind::BOUND_VAR_LIST, nbvs );
1340             for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
1341               //Make new assertion based on partially instantiating existing
1342               applyv[k+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, atdd[cc].getConstructor());
1343               Debug("parser-sygus") << "applyv " << applyv[k+1] << std::endl;
1344               cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
1345               Debug("parser-sygus") << "cpatv " << cpatv << std::endl;
1346               patv[1] = cpatv;
1347               evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
1348               Debug("parser-sygus") << "evalApply " << evalApply << std::endl;
1349               builtApply[k] = ops[index][cc];
1350               Debug("parser-sygus") << "builtApply " << builtApply[k] << std::endl;
1351               builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
1352               Debug("parser-sygus") << "builtTerm " << builtTerm << std::endl;
1353               Expr eassertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
1354               Expr epattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
1355               epattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, epattern);
1356               eassertion = getExprManager()->mkExpr(kind::FORALL, nbvl, eassertion, epattern);
1357               assertions.push_back( eassertion );
1358             }
1359             assertion = assertions.size()==1 ? assertions[0] : getExprManager()->mkExpr( kind::AND, assertions );
1360             Debug("parser-sygus") << "...(linearized) assertion is: " << assertion << std::endl;
1361           }
1362         }
1363       }
1364     }
1365   }
1366   return assertion;
1367 }
1368
1369 const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
1370   for( unsigned i=0; i<d_sygusVars.size(); i++ ){
1371     Expr v = d_sygusVars[i];
1372     std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v );
1373     if( it!=d_sygusVarPrimed.end() ){
1374       if( it->second==isPrimed ){
1375         vars.push_back( v );
1376       }
1377     }else{
1378       //should never happen
1379     }
1380   }
1381 }
1382
1383 }/* CVC4::parser namespace */
1384 }/* CVC4 namespace */