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