src/parser/smt2/smt2.cpp

   1 /*********************                                                        */
   2 /*! \file smt2.cpp
   3  ** \verbatim
   4  ** Original author: Christopher L. Conway
   5  ** Major contributors: Kshitij Bansal, Morgan Deters
   6  ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett, Tianyi Liang
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Definitions of SMT2 constants.
  13  **
  14  ** Definitions of SMT2 constants.
  15  **/
  16
  17 #include "expr/type.h"
  18 #include "expr/command.h"
  19 #include "parser/parser.h"
  20 #include "parser/smt1/smt1.h"
  21 #include "parser/smt2/smt2.h"
  22 #include "parser/antlr_input.h"
  23
  24 // ANTLR defines these, which is really bad!
  25 #undef true
  26 #undef false
  27
  28 namespace CVC4 {
  29 namespace parser {
  30
  31 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
  32   Parser(exprManager,input,strictMode,parseOnly),
  33   d_logicSet(false),
  34   d_nextSygusFun(0) {
  35   d_unsatCoreNames.push(std::map<Expr, std::string>());
  36   if( !strictModeEnabled() ) {
  37     addTheory(Smt2::THEORY_CORE);
  38   }
  39 }
  40
  41 void Smt2::addArithmeticOperators() {
  42   Parser::addOperator(kind::PLUS);
  43   Parser::addOperator(kind::MINUS);
  44   Parser::addOperator(kind::UMINUS);
  45   Parser::addOperator(kind::MULT);
  46   Parser::addOperator(kind::LT);
  47   Parser::addOperator(kind::LEQ);
  48   Parser::addOperator(kind::GT);
  49   Parser::addOperator(kind::GEQ);
  50 }
  51
  52 void Smt2::addBitvectorOperators() {
  53   addOperator(kind::BITVECTOR_CONCAT, "concat");
  54   addOperator(kind::BITVECTOR_NOT, "bvnot");
  55   addOperator(kind::BITVECTOR_AND, "bvand");
  56   addOperator(kind::BITVECTOR_OR, "bvor");
  57   addOperator(kind::BITVECTOR_NEG, "bvneg");
  58   addOperator(kind::BITVECTOR_PLUS, "bvadd");
  59   addOperator(kind::BITVECTOR_MULT, "bvmul");
  60   addOperator(kind::BITVECTOR_UDIV, "bvudiv");
  61   addOperator(kind::BITVECTOR_UREM, "bvurem");
  62   addOperator(kind::BITVECTOR_SHL, "bvshl");
  63   addOperator(kind::BITVECTOR_LSHR, "bvlshr");
  64   addOperator(kind::BITVECTOR_ULT, "bvult");
  65   addOperator(kind::BITVECTOR_NAND, "bvnand");
  66   addOperator(kind::BITVECTOR_NOR, "bvnor");
  67   addOperator(kind::BITVECTOR_XOR, "bvxor");
  68   addOperator(kind::BITVECTOR_XNOR, "bvxnor");
  69   addOperator(kind::BITVECTOR_COMP, "bvcomp");
  70   addOperator(kind::BITVECTOR_SUB, "bvsub");
  71   addOperator(kind::BITVECTOR_SDIV, "bvsdiv");
  72   addOperator(kind::BITVECTOR_SREM, "bvsrem");
  73   addOperator(kind::BITVECTOR_SMOD, "bvsmod");
  74   addOperator(kind::BITVECTOR_ASHR, "bvashr");
  75   addOperator(kind::BITVECTOR_ULE, "bvule");
  76   addOperator(kind::BITVECTOR_UGT, "bvugt");
  77   addOperator(kind::BITVECTOR_UGE, "bvuge");
  78   addOperator(kind::BITVECTOR_SLT, "bvslt");
  79   addOperator(kind::BITVECTOR_SLE, "bvsle");
  80   addOperator(kind::BITVECTOR_SGT, "bvsgt");
  81   addOperator(kind::BITVECTOR_SGE, "bvsge");
  82
  83   Parser::addOperator(kind::BITVECTOR_BITOF);
  84   Parser::addOperator(kind::BITVECTOR_EXTRACT);
  85   Parser::addOperator(kind::BITVECTOR_REPEAT);
  86   Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND);
  87   Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND);
  88   Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT);
  89   Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT);
  90
  91   Parser::addOperator(kind::INT_TO_BITVECTOR);
  92   Parser::addOperator(kind::BITVECTOR_TO_NAT);
  93 }
  94
  95 void Smt2::addStringOperators() {
  96   addOperator(kind::STRING_CONCAT, "str.++");
  97   addOperator(kind::STRING_LENGTH, "str.len");
  98   addOperator(kind::STRING_SUBSTR, "str.substr" );
  99   addOperator(kind::STRING_STRCTN, "str.contains" );
 100   addOperator(kind::STRING_CHARAT, "str.at" );
 101   addOperator(kind::STRING_STRIDOF, "str.indexof" );
 102   addOperator(kind::STRING_STRREPL, "str.replace" );
 103   addOperator(kind::STRING_PREFIX, "str.prefixof" );
 104   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
 105   addOperator(kind::STRING_ITOS, "int.to.str" );
 106   addOperator(kind::STRING_STOI, "str.to.int" );
 107   addOperator(kind::STRING_U16TOS, "u16.to.str" );
 108   addOperator(kind::STRING_STOU16, "str.to.u16" );
 109   addOperator(kind::STRING_U32TOS, "u32.to.str" );
 110   addOperator(kind::STRING_STOU32, "str.to.u32" );
 111   addOperator(kind::STRING_IN_REGEXP, "str.in.re");
 112   addOperator(kind::STRING_TO_REGEXP, "str.to.re");
 113   addOperator(kind::REGEXP_CONCAT, "re.++");
 114   addOperator(kind::REGEXP_UNION, "re.union");
 115   addOperator(kind::REGEXP_INTER, "re.inter");
 116   addOperator(kind::REGEXP_STAR, "re.*");
 117   addOperator(kind::REGEXP_PLUS, "re.+");
 118   addOperator(kind::REGEXP_OPT, "re.opt");
 119   addOperator(kind::REGEXP_RANGE, "re.range");
 120   addOperator(kind::REGEXP_LOOP, "re.loop");
 121 }
 122
 123 void Smt2::addFloatingPointOperators() {
 124   addOperator(kind::FLOATINGPOINT_FP, "fp");
 125   addOperator(kind::FLOATINGPOINT_EQ, "fp.eq");
 126   addOperator(kind::FLOATINGPOINT_ABS, "fp.abs");
 127   addOperator(kind::FLOATINGPOINT_NEG, "fp.neg");
 128   addOperator(kind::FLOATINGPOINT_PLUS, "fp.add");
 129   addOperator(kind::FLOATINGPOINT_SUB, "fp.sub");
 130   addOperator(kind::FLOATINGPOINT_MULT, "fp.mul");
 131   addOperator(kind::FLOATINGPOINT_DIV, "fp.div");
 132   addOperator(kind::FLOATINGPOINT_FMA, "fp.fma");
 133   addOperator(kind::FLOATINGPOINT_SQRT, "fp.sqrt");
 134   addOperator(kind::FLOATINGPOINT_REM, "fp.rem");
 135   addOperator(kind::FLOATINGPOINT_RTI, "fp.roundToIntegral");
 136   addOperator(kind::FLOATINGPOINT_MIN, "fp.min");
 137   addOperator(kind::FLOATINGPOINT_MAX, "fp.max");
 138   addOperator(kind::FLOATINGPOINT_LEQ, "fp.leq");
 139   addOperator(kind::FLOATINGPOINT_LT, "fp.lt");
 140   addOperator(kind::FLOATINGPOINT_GEQ, "fp.geq");
 141   addOperator(kind::FLOATINGPOINT_GT, "fp.gt");
 142   addOperator(kind::FLOATINGPOINT_ISN, "fp.isNormal");
 143   addOperator(kind::FLOATINGPOINT_ISSN, "fp.isSubnormal");
 144   addOperator(kind::FLOATINGPOINT_ISZ, "fp.isZero");
 145   addOperator(kind::FLOATINGPOINT_ISINF, "fp.isInfinite");
 146   addOperator(kind::FLOATINGPOINT_ISNAN, "fp.isNaN");
 147   addOperator(kind::FLOATINGPOINT_ISNEG, "fp.isNegative");
 148   addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
 149   addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
 150
 151   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
 152   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
 153   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL);
 154   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
 155   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
 156   Parser::addOperator(kind::FLOATINGPOINT_TO_UBV);
 157   Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
 158 }
 159
 160
 161 void Smt2::addTheory(Theory theory) {
 162   switch(theory) {
 163   case THEORY_ARRAYS:
 164     addOperator(kind::SELECT, "select");
 165     addOperator(kind::STORE, "store");
 166     break;
 167
 168   case THEORY_BITVECTORS:
 169     addBitvectorOperators();
 170     break;
 171
 172   case THEORY_CORE:
 173     defineType("Bool", getExprManager()->booleanType());
 174     defineVar("true", getExprManager()->mkConst(true));
 175     defineVar("false", getExprManager()->mkConst(false));
 176     Parser::addOperator(kind::AND);
 177     Parser::addOperator(kind::DISTINCT);
 178     Parser::addOperator(kind::EQUAL);
 179     Parser::addOperator(kind::IFF);
 180     Parser::addOperator(kind::IMPLIES);
 181     Parser::addOperator(kind::ITE);
 182     Parser::addOperator(kind::NOT);
 183     Parser::addOperator(kind::OR);
 184     Parser::addOperator(kind::XOR);
 185     break;
 186
 187   case THEORY_REALS_INTS:
 188     defineType("Real", getExprManager()->realType());
 189     Parser::addOperator(kind::DIVISION);
 190     addOperator(kind::TO_INTEGER, "to_int");
 191     addOperator(kind::IS_INTEGER, "is_int");
 192     addOperator(kind::TO_REAL, "to_real");
 193     // falling through on purpose, to add Ints part of Reals_Ints
 194   case THEORY_INTS:
 195     defineType("Int", getExprManager()->integerType());
 196     addArithmeticOperators();
 197     addOperator(kind::INTS_DIVISION, "div");
 198     addOperator(kind::INTS_MODULUS, "mod");
 199     addOperator(kind::ABS, "abs");
 200     Parser::addOperator(kind::DIVISIBLE);
 201     break;
 202
 203   case THEORY_REALS:
 204     defineType("Real", getExprManager()->realType());
 205     addArithmeticOperators();
 206     Parser::addOperator(kind::DIVISION);
 207     break;
 208
 209   case THEORY_QUANTIFIERS:
 210     break;
 211
 212   case THEORY_SETS:
 213     addOperator(kind::UNION, "union");
 214     addOperator(kind::INTERSECTION, "intersection");
 215     addOperator(kind::SETMINUS, "setminus");
 216     addOperator(kind::SUBSET, "subset");
 217     addOperator(kind::MEMBER, "member");
 218     addOperator(kind::SINGLETON, "singleton");
 219     addOperator(kind::INSERT, "insert");
 220     break;
 221
 222   case THEORY_DATATYPES:
 223     Parser::addOperator(kind::APPLY_CONSTRUCTOR);
 224     Parser::addOperator(kind::APPLY_TESTER);
 225     Parser::addOperator(kind::APPLY_SELECTOR);
 226     Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
 227     break;
 228
 229   case THEORY_STRINGS:
 230     defineType("String", getExprManager()->stringType());
 231     defineType("Int", getExprManager()->integerType());
 232     addStringOperators();
 233     break;
 234
 235   case THEORY_UF:
 236     Parser::addOperator(kind::APPLY_UF);
 237     break;
 238
 239   case THEORY_FP:
 240     defineType("RoundingMode", getExprManager()->roundingModeType());
 241     defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
 242     defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
 243     defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
 244     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
 245     addFloatingPointOperators();
 246     break;
 247
 248   default:
 249     std::stringstream ss;
 250     ss << "internal error: unsupported theory " << theory;
 251     throw ParserException(ss.str());
 252   }
 253 }
 254
 255 void Smt2::addOperator(Kind kind, const std::string& name) {
 256   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 257                   << std::endl;
 258   Parser::addOperator(kind);
 259   operatorKindMap[name] = kind;
 260 }
 261
 262 Kind Smt2::getOperatorKind(const std::string& name) const {
 263   // precondition: isOperatorEnabled(name)
 264   return operatorKindMap.find(name)->second;
 265 }
 266
 267 bool Smt2::isOperatorEnabled(const std::string& name) const {
 268   return operatorKindMap.find(name) != operatorKindMap.end();
 269 }
 270
 271 bool Smt2::isTheoryEnabled(Theory theory) const {
 272   switch(theory) {
 273   case THEORY_ARRAYS:
 274     return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
 275   case THEORY_BITVECTORS:
 276     return d_logic.isTheoryEnabled(theory::THEORY_BV);
 277   case THEORY_CORE:
 278     return true;
 279   case THEORY_DATATYPES:
 280     return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
 281   case THEORY_INTS:
 282     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 283       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
 284   case THEORY_REALS:
 285     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 286       ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
 287   case THEORY_REALS_INTS:
 288     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 289       d_logic.areIntegersUsed() && d_logic.areRealsUsed();
 290   case THEORY_QUANTIFIERS:
 291     return d_logic.isQuantified();
 292   case THEORY_SETS:
 293     return d_logic.isTheoryEnabled(theory::THEORY_SETS);
 294   case THEORY_STRINGS:
 295     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
 296   case THEORY_UF:
 297     return d_logic.isTheoryEnabled(theory::THEORY_UF);
 298   case THEORY_FP:
 299     return d_logic.isTheoryEnabled(theory::THEORY_FP);
 300   default:
 301     std::stringstream ss;
 302     ss << "internal error: unsupported theory " << theory;
 303     throw ParserException(ss.str());
 304   }
 305 }
 306
 307 bool Smt2::logicIsSet() {
 308   return d_logicSet;
 309 }
 310
 311 void Smt2::reset() {
 312   d_logicSet = false;
 313   d_logic = LogicInfo();
 314   operatorKindMap.clear();
 315   d_lastNamedTerm = std::pair<Expr, std::string>();
 316   d_unsatCoreNames = std::stack< std::map<Expr, std::string> >();
 317   this->Parser::reset();
 318
 319   d_unsatCoreNames.push(std::map<Expr, std::string>());
 320   if( !strictModeEnabled() ) {
 321     addTheory(Smt2::THEORY_CORE);
 322   }
 323 }
 324
 325 void Smt2::resetAssertions() {
 326   this->Parser::reset();
 327 }
 328
 329 void Smt2::setLogic(std::string name) {
 330   if(sygus()) {
 331     if(name == "Arrays") {
 332       name = "AUF";
 333     } else if(name == "Reals") {
 334       name = "UFLRA";
 335     } else if(name == "LIA") {
 336       name = "UFLIA";
 337     } else if(name == "LRA") {
 338       name = "UFLRA";
 339     } else if(name == "LIRA") {
 340       name = "UFLIRA";
 341     } else if(name == "BV") {
 342       name = "UFBV";
 343     } else {
 344       std::stringstream ss;
 345       ss << "Unknown SyGuS background logic `" << name << "'";
 346       parseError(ss.str());
 347     }
 348   }
 349
 350   d_logicSet = true;
 351   if(logicIsForced()) {
 352     d_logic = getForcedLogic();
 353   } else {
 354     d_logic = name;
 355   }
 356
 357   // Core theory belongs to every logic
 358   addTheory(THEORY_CORE);
 359
 360   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 361     addTheory(THEORY_UF);
 362   }
 363
 364   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 365     if(d_logic.areIntegersUsed()) {
 366       if(d_logic.areRealsUsed()) {
 367         addTheory(THEORY_REALS_INTS);
 368       } else {
 369         addTheory(THEORY_INTS);
 370       }
 371     } else if(d_logic.areRealsUsed()) {
 372       addTheory(THEORY_REALS);
 373     }
 374   }
 375
 376   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
 377     addTheory(THEORY_ARRAYS);
 378   }
 379
 380   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 381     addTheory(THEORY_BITVECTORS);
 382   }
 383
 384   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
 385     addTheory(THEORY_DATATYPES);
 386   }
 387
 388   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 389     addTheory(THEORY_SETS);
 390   }
 391
 392   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 393     addTheory(THEORY_STRINGS);
 394   }
 395
 396   if(d_logic.isQuantified()) {
 397     addTheory(THEORY_QUANTIFIERS);
 398   }
 399
 400   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
 401     addTheory(THEORY_FP);
 402   }
 403
 404 }/* Smt2::setLogic() */
 405
 406 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 407   // TODO: ???
 408 }
 409
 410 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 411   // TODO: ???
 412 }
 413
 414 void Smt2::checkThatLogicIsSet() {
 415   if( ! logicIsSet() ) {
 416     if(strictModeEnabled()) {
 417       parseError("set-logic must appear before this point.");
 418     } else {
 419       if(sygus()) {
 420         setLogic("LIA");
 421       } else {
 422         warning("No set-logic command was given before this point.");
 423         warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
 424         warning("Consider setting a stricter logic for (likely) better performance.");
 425         warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 426
 427         setLogic("ALL_SUPPORTED");
 428       }
 429
 430       Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
 431       c->setMuted(true);
 432       preemptCommand(c);
 433     }
 434   }
 435 }
 436
 437 /* The include are managed in the lexer but called in the parser */
 438 // Inspired by http://www.antlr3.org/api/C/interop.html
 439
 440 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 441   Debug("parser") << "Including " << filename << std::endl;
 442   // Create a new input stream and take advantage of built in stream stacking
 443   // in C target runtime.
 444   //
 445   pANTLR3_INPUT_STREAM    in;
 446 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 447   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 448 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 449   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 450 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 451   if( in == NULL ) {
 452     Debug("parser") << "Can't open " << filename << std::endl;
 453     return false;
 454   }
 455   // Same thing as the predefined PUSHSTREAM(in);
 456   lexer->pushCharStream(lexer, in);
 457   // restart it
 458   //lexer->rec->state->tokenStartCharIndex      = -10;
 459   //lexer->emit(lexer);
 460
 461   // Note that the input stream is not closed when it EOFs, I don't bother
 462   // to do it here, but it is up to you to track streams created like this
 463   // and destroy them when the whole parse session is complete. Remember that you
 464   // don't want to do this until all tokens have been manipulated all the way through
 465   // your tree parsers etc as the token does not store the text it just refers
 466   // back to the input stream and trying to get the text for it will abort if you
 467   // close the input stream too early.
 468
 469   //TODO what said before
 470   return true;
 471 }
 472
 473 void Smt2::includeFile(const std::string& filename) {
 474   // security for online version
 475   if(!canIncludeFile()) {
 476     parseError("include-file feature was disabled for this run.");
 477   }
 478
 479   // Get the lexer
 480   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 481   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 482   // get the name of the current stream "Does it work inside an include?"
 483   const std::string inputName = ai->getInputStreamName();
 484
 485   // Find the directory of the current input file
 486   std::string path;
 487   size_t pos = inputName.rfind('/');
 488   if(pos != std::string::npos) {
 489     path = std::string(inputName, 0, pos + 1);
 490   }
 491   path.append(filename);
 492   if(!newInputStream(path, lexer)) {
 493     parseError("Couldn't open include file `" + path + "'");
 494   }
 495 }
 496
 497
 498
 499  void Smt2::defineSygusFuns() {
 500   // only define each one once
 501   while(d_nextSygusFun < d_sygusFuns.size()) {
 502     std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun];
 503     std::string fun = p.first;
 504     Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl;
 505     Expr eval = p.second;
 506     FunctionType evalType = eval.getType();
 507     std::vector<Type> argTypes = evalType.getArgTypes();
 508     Type rangeType = evalType.getRangeType();
 509     Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl;
 510
 511     // first make the function type
 512     std::vector<Expr> sygusVars;
 513     std::vector<Type> funType;
 514     for(size_t j = 1; j < argTypes.size(); ++j) {
 515       funType.push_back(argTypes[j]);
 516       std::stringstream ss;
 517       ss << fun << "_v_" << j;
 518       sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), argTypes[j]));
 519     }
 520     Type funt;
 521     if( !funType.empty() ){
 522       funt = getExprManager()->mkFunctionType(funType, rangeType);
 523       Debug("parser-sygus") << "...eval function type : " << funt << std::endl;
 524
 525       // copy the bound vars
 526       /*
 527       std::vector<Expr> sygusVars;
 528       //std::vector<Type> types;
 529       for(size_t i = 0; i < d_sygusVars.size(); ++i) {
 530         std::stringstream ss;
 531         ss << d_sygusVars[i];
 532         Type type = d_sygusVars[i].getType();
 533         sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
 534         //types.push_back(type);
 535       }
 536       Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
 537       */
 538
 539       //Type t = getExprManager()->mkFunctionType(types, rangeType);
 540       //Debug("parser-sygus") << "...function type : " << t << std::endl;
 541     }else{
 542       funt = rangeType;
 543     }
 544     Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED);
 545     Debug("parser-sygus") << "...made function : " << lambda << std::endl;
 546     std::vector<Expr> applyv;
 547     Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]);
 548     d_sygusFunSymbols.push_back(funbv);
 549     applyv.push_back(eval);
 550     applyv.push_back(funbv);
 551     for(size_t i = 0; i < sygusVars.size(); ++i) {
 552       applyv.push_back(sygusVars[i]);
 553     }
 554     Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv);
 555     Debug("parser-sygus") << "...made apply " << apply << std::endl;
 556     Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply);
 557     preemptCommand(cmd);
 558
 559     ++d_nextSygusFun;
 560   }
 561 }
 562
 563 void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
 564                             std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ) {
 565   for( unsigned i=0; i<cnames.size(); i++ ){
 566     std::string name = dt.getName() + "_" + cnames[i];
 567     std::string testerId("is-");
 568     testerId.append(name);
 569     checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
 570     checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
 571     CVC4::DatatypeConstructor c(name, testerId, ops[i] );
 572     for( unsigned j=0; j<cargs[i].size(); j++ ){
 573       std::stringstream sname;
 574       sname << name << "_" << j;
 575       c.addArg(sname.str(), cargs[i][j]);
 576     }
 577     dt.addConstructor(c);
 578   }
 579 }
 580
 581 // i is index in datatypes/ops
 582 // j is index is datatype
 583 Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
 584                               std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
 585                               Expr eval, const Datatype& dt, size_t i, size_t j ) {
 586   const DatatypeConstructor& ctor = dt[j];
 587   Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl;
 588   std::vector<Expr> bvs, extraArgs;
 589   for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
 590     std::string vname = "v_" + ctor[k].getName();
 591     Expr bv = getExprManager()->mkBoundVar(vname, SelectorType(ctor[k].getType()).getRangeType());
 592     bvs.push_back(bv);
 593     extraArgs.push_back(bv);
 594   }
 595   if( !terms[0].isNull() ){
 596     bvs.insert(bvs.end(), terms[0].begin(), terms[0].end());
 597   }
 598   Expr bvl;
 599   if( !bvs.empty() ){
 600     bvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, bvs);
 601   }
 602   Debug("parser-sygus") << "...made bv list " << bvl << std::endl;
 603   std::vector<Expr> patv;
 604   patv.push_back(eval);
 605   std::vector<Expr> applyv;
 606   applyv.push_back(ctor.getConstructor());
 607   applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end());
 608   for(size_t k = 0; k < applyv.size(); ++k) {
 609   }
 610   Expr cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
 611   Debug("parser-sygus") << "...made eval ctor apply " << cpatv << std::endl;
 612   patv.push_back(cpatv);
 613   if( !terms[0].isNull() ){
 614     patv.insert(patv.end(), terms[0].begin(), terms[0].end());
 615   }
 616   Expr evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
 617   Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl;
 618   std::vector<Expr> builtApply;
 619   for(size_t k = 0; k < extraArgs.size(); ++k) {
 620     std::vector<Expr> patvb;
 621     patvb.push_back(evals[DatatypeType(extraArgs[k].getType())]);
 622     patvb.push_back(extraArgs[k]);
 623     if( !terms[0].isNull() ){
 624       patvb.insert(patvb.end(), terms[0].begin(), terms[0].end());
 625     }
 626     builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb));
 627   }
 628   for(size_t k = 0; k < builtApply.size(); ++k) {
 629   }
 630   Expr builtTerm;
 631   //if( ops[i][j].getKind() == kind::BUILTIN ){
 632   if( !builtApply.empty() ){
 633     if( ops[i][j].getKind() != kind::BUILTIN ){
 634       builtTerm = getExprManager()->mkExpr(kind::APPLY, ops[i][j], builtApply);
 635     }else{
 636       builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
 637     }
 638   }else{
 639     builtTerm = ops[i][j];
 640   }
 641   Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
 642   Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
 643   if( !bvl.isNull() ){
 644     Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
 645     pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
 646     assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern);
 647   }
 648   Debug("parser-sygus") << "...made assertion " << assertion << std::endl;
 649
 650   //linearize multiplication if possible
 651   if( builtTerm.getKind()==kind::MULT ){
 652     for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
 653       Type at = SelectorType(ctor[k].getType()).getRangeType();
 654       if( at.isDatatype() ){
 655         DatatypeType atd = (DatatypeType)SelectorType(ctor[k].getType()).getRangeType();
 656         Debug("parser-sygus") << "Argument " << k << " " << atd << std::endl;
 657         std::vector<DatatypeType>::iterator itd = std::find( datatypeTypes.begin(), datatypeTypes.end(), atd );
 658         if( itd!=datatypeTypes.end() ){
 659           Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl;
 660           unsigned index = itd-datatypeTypes.begin();
 661           Debug("parser-sygus2") << "index = " << index << std::endl;
 662           bool isConst = true;
 663           for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
 664             Debug("parser-sygus2") << "ops[" << cc << "]=" << ops[index][cc] << std::endl;
 665             if( ops[index][cc].getKind() != kind::CONST_RATIONAL ){
 666               isConst = false;
 667               break;
 668             }
 669           }
 670           if( isConst ){
 671             Debug("parser-sygus") << "Linearize multiplication " << ctor << " based on argument " << k << std::endl;
 672             const Datatype & atdd = atd.getDatatype();
 673             std::vector<Expr> assertions;
 674             std::vector<Expr> nbvs;
 675             for( unsigned a=0; a<bvl.getNumChildren(); a++ ){
 676               if( a!=k ){
 677                 nbvs.push_back( bvl[a] );
 678               }
 679             }
 680             Expr nbvl = getExprManager()->mkExpr( kind::BOUND_VAR_LIST, nbvs );
 681             for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
 682               //Make new assertion based on partially instantiating existing
 683               applyv[k+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, atdd[cc].getConstructor());
 684               Debug("parser-sygus") << "applyv " << applyv[k+1] << std::endl;
 685               cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
 686               Debug("parser-sygus") << "cpatv " << cpatv << std::endl;
 687               patv[1] = cpatv;
 688               evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
 689               Debug("parser-sygus") << "evalApply " << evalApply << std::endl;
 690               builtApply[k] = ops[index][cc];
 691               Debug("parser-sygus") << "builtApply " << builtApply[k] << std::endl;
 692               builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
 693               Debug("parser-sygus") << "builtTerm " << builtTerm << std::endl;
 694               Expr eassertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
 695               Expr epattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
 696               epattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, epattern);
 697               eassertion = getExprManager()->mkExpr(kind::FORALL, nbvl, eassertion, epattern);
 698               assertions.push_back( eassertion );
 699             }
 700             assertion = assertions.size()==1 ? assertions[0] : getExprManager()->mkExpr( kind::AND, assertions );
 701             Debug("parser-sygus") << "...(linearized) assertion is: " << assertion << std::endl;
 702           }
 703         }
 704       }
 705     }
 706   }
 707   return assertion;
 708 }
 709
 710
 711 }/* CVC4::parser namespace */
 712 }/* CVC4 namespace */