src/parser/smt2/smt2.cpp

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