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