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     addStringOperators();
 232     break;
 233
 234   case THEORY_UF:
 235     Parser::addOperator(kind::APPLY_UF);
 236     break;
 237
 238   case THEORY_FP:
 239     defineType("RoundingMode", getExprManager()->roundingModeType());
 240     defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
 241     defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
 242     defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
 243     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
 244     addFloatingPointOperators();
 245     break;
 246
 247   default:
 248     std::stringstream ss;
 249     ss << "internal error: unsupported theory " << theory;
 250     throw ParserException(ss.str());
 251   }
 252 }
 253
 254 void Smt2::addOperator(Kind kind, const std::string& name) {
 255   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 256                   << std::endl;
 257   Parser::addOperator(kind);
 258   operatorKindMap[name] = kind;
 259 }
 260
 261 Kind Smt2::getOperatorKind(const std::string& name) const {
 262   // precondition: isOperatorEnabled(name)
 263   return operatorKindMap.find(name)->second;
 264 }
 265
 266 bool Smt2::isOperatorEnabled(const std::string& name) const {
 267   return operatorKindMap.find(name) != operatorKindMap.end();
 268 }
 269
 270 bool Smt2::isTheoryEnabled(Theory theory) const {
 271   switch(theory) {
 272   case THEORY_ARRAYS:
 273     return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
 274   case THEORY_BITVECTORS:
 275     return d_logic.isTheoryEnabled(theory::THEORY_BV);
 276   case THEORY_CORE:
 277     return true;
 278   case THEORY_DATATYPES:
 279     return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
 280   case THEORY_INTS:
 281     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 282       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
 283   case THEORY_REALS:
 284     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 285       ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
 286   case THEORY_REALS_INTS:
 287     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 288       d_logic.areIntegersUsed() && d_logic.areRealsUsed();
 289   case THEORY_QUANTIFIERS:
 290     return d_logic.isQuantified();
 291   case THEORY_SETS:
 292     return d_logic.isTheoryEnabled(theory::THEORY_SETS);
 293   case THEORY_STRINGS:
 294     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
 295   case THEORY_UF:
 296     return d_logic.isTheoryEnabled(theory::THEORY_UF);
 297   case THEORY_FP:
 298     return d_logic.isTheoryEnabled(theory::THEORY_FP);
 299   default:
 300     std::stringstream ss;
 301     ss << "internal error: unsupported theory " << theory;
 302     throw ParserException(ss.str());
 303   }
 304 }
 305
 306 bool Smt2::logicIsSet() {
 307   return d_logicSet;
 308 }
 309
 310 void Smt2::reset() {
 311   d_logicSet = false;
 312   d_logic = LogicInfo();
 313   operatorKindMap.clear();
 314   d_lastNamedTerm = std::pair<Expr, std::string>();
 315   d_unsatCoreNames = std::stack< std::map<Expr, std::string> >();
 316   this->Parser::reset();
 317
 318   d_unsatCoreNames.push(std::map<Expr, std::string>());
 319   if( !strictModeEnabled() ) {
 320     addTheory(Smt2::THEORY_CORE);
 321   }
 322 }
 323
 324 void Smt2::resetAssertions() {
 325   this->Parser::reset();
 326 }
 327
 328 void Smt2::setLogic(std::string name) {
 329   if(sygus()) {
 330     if(name == "Arrays") {
 331       name = "AUF";
 332     } else if(name == "Reals") {
 333       name = "UFLRA";
 334     } else if(name == "LIA") {
 335       name = "UFLIA";
 336     } else if(name == "LRA") {
 337       name = "UFLRA";
 338     } else if(name == "LIRA") {
 339       name = "UFLIRA";
 340     } else if(name == "BV") {
 341       name = "UFBV";
 342     } else {
 343       std::stringstream ss;
 344       ss << "Unknown SyGuS background logic `" << name << "'";
 345       parseError(ss.str());
 346     }
 347   }
 348
 349   d_logicSet = true;
 350   if(logicIsForced()) {
 351     d_logic = getForcedLogic();
 352   } else {
 353     d_logic = name;
 354   }
 355
 356   // Core theory belongs to every logic
 357   addTheory(THEORY_CORE);
 358
 359   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 360     addTheory(THEORY_UF);
 361   }
 362
 363   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 364     if(d_logic.areIntegersUsed()) {
 365       if(d_logic.areRealsUsed()) {
 366         addTheory(THEORY_REALS_INTS);
 367       } else {
 368         addTheory(THEORY_INTS);
 369       }
 370     } else if(d_logic.areRealsUsed()) {
 371       addTheory(THEORY_REALS);
 372     }
 373   }
 374
 375   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
 376     addTheory(THEORY_ARRAYS);
 377   }
 378
 379   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 380     addTheory(THEORY_BITVECTORS);
 381   }
 382
 383   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
 384     addTheory(THEORY_DATATYPES);
 385   }
 386
 387   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 388     addTheory(THEORY_SETS);
 389   }
 390
 391   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 392     addTheory(THEORY_STRINGS);
 393   }
 394
 395   if(d_logic.isQuantified()) {
 396     addTheory(THEORY_QUANTIFIERS);
 397   }
 398
 399   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
 400     addTheory(THEORY_FP);
 401   }
 402
 403 }/* Smt2::setLogic() */
 404
 405 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 406   // TODO: ???
 407 }
 408
 409 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 410   // TODO: ???
 411 }
 412
 413 void Smt2::checkThatLogicIsSet() {
 414   if( ! logicIsSet() ) {
 415     if(strictModeEnabled()) {
 416       parseError("set-logic must appear before this point.");
 417     } else {
 418       if(sygus()) {
 419         setLogic("LIA");
 420       } else {
 421         warning("No set-logic command was given before this point.");
 422         warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
 423         warning("Consider setting a stricter logic for (likely) better performance.");
 424         warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 425
 426         setLogic("ALL_SUPPORTED");
 427       }
 428
 429       Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
 430       c->setMuted(true);
 431       preemptCommand(c);
 432     }
 433   }
 434 }
 435
 436 /* The include are managed in the lexer but called in the parser */
 437 // Inspired by http://www.antlr3.org/api/C/interop.html
 438
 439 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 440   Debug("parser") << "Including " << filename << std::endl;
 441   // Create a new input stream and take advantage of built in stream stacking
 442   // in C target runtime.
 443   //
 444   pANTLR3_INPUT_STREAM    in;
 445 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 446   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 447 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 448   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 449 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 450   if( in == NULL ) {
 451     Debug("parser") << "Can't open " << filename << std::endl;
 452     return false;
 453   }
 454   // Same thing as the predefined PUSHSTREAM(in);
 455   lexer->pushCharStream(lexer, in);
 456   // restart it
 457   //lexer->rec->state->tokenStartCharIndex      = -10;
 458   //lexer->emit(lexer);
 459
 460   // Note that the input stream is not closed when it EOFs, I don't bother
 461   // to do it here, but it is up to you to track streams created like this
 462   // and destroy them when the whole parse session is complete. Remember that you
 463   // don't want to do this until all tokens have been manipulated all the way through
 464   // your tree parsers etc as the token does not store the text it just refers
 465   // back to the input stream and trying to get the text for it will abort if you
 466   // close the input stream too early.
 467
 468   //TODO what said before
 469   return true;
 470 }
 471
 472 void Smt2::includeFile(const std::string& filename) {
 473   // security for online version
 474   if(!canIncludeFile()) {
 475     parseError("include-file feature was disabled for this run.");
 476   }
 477
 478   // Get the lexer
 479   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 480   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 481   // get the name of the current stream "Does it work inside an include?"
 482   const std::string inputName = ai->getInputStreamName();
 483
 484   // Find the directory of the current input file
 485   std::string path;
 486   size_t pos = inputName.rfind('/');
 487   if(pos != std::string::npos) {
 488     path = std::string(inputName, 0, pos + 1);
 489   }
 490   path.append(filename);
 491   if(!newInputStream(path, lexer)) {
 492     parseError("Couldn't open include file `" + path + "'");
 493   }
 494 }
 495
 496
 497
 498  void Smt2::defineSygusFuns() {
 499   // only define each one once
 500   while(d_nextSygusFun < d_sygusFuns.size()) {
 501     std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun];
 502     std::string fun = p.first;
 503     Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl;
 504     Expr eval = p.second;
 505     FunctionType evalType = eval.getType();
 506     std::vector<Type> argTypes = evalType.getArgTypes();
 507     Type rangeType = evalType.getRangeType();
 508     Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl;
 509
 510     // first make the function type
 511     std::vector<Expr> sygusVars;
 512     std::vector<Type> funType;
 513     for(size_t j = 1; j < argTypes.size(); ++j) {
 514       funType.push_back(argTypes[j]);
 515       std::stringstream ss;
 516       ss << fun << "_v_" << j;
 517       sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), argTypes[j]));
 518     }
 519     Type funt = getExprManager()->mkFunctionType(funType, rangeType);
 520     Debug("parser-sygus") << "...eval function type : " << funt << std::endl;
 521
 522     // copy the bound vars
 523     /*
 524     std::vector<Expr> sygusVars;
 525     //std::vector<Type> types;
 526     for(size_t i = 0; i < d_sygusVars.size(); ++i) {
 527       std::stringstream ss;
 528       ss << d_sygusVars[i];
 529       Type type = d_sygusVars[i].getType();
 530       sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
 531       //types.push_back(type);
 532     }
 533     Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
 534     */
 535
 536     //Type t = getExprManager()->mkFunctionType(types, rangeType);
 537     //Debug("parser-sygus") << "...function type : " << t << std::endl;
 538
 539     Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED);
 540     Debug("parser-sygus") << "...made function : " << lambda << std::endl;
 541     std::vector<Expr> applyv;
 542     Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]);
 543     d_sygusFunSymbols.push_back(funbv);
 544     applyv.push_back(eval);
 545     applyv.push_back(funbv);
 546     for(size_t i = 0; i < sygusVars.size(); ++i) {
 547       applyv.push_back(sygusVars[i]);
 548     }
 549     Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv);
 550     Debug("parser-sygus") << "...made apply " << apply << std::endl;
 551     Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply);
 552     preemptCommand(cmd);
 553
 554     ++d_nextSygusFun;
 555   }
 556 }
 557
 558 void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
 559                             std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ) {
 560   for( unsigned i=0; i<cnames.size(); i++ ){
 561     std::string name = dt.getName() + "_" + cnames[i];
 562     std::string testerId("is-");
 563     testerId.append(name);
 564     checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
 565     checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
 566     CVC4::DatatypeConstructor c(name, testerId, ops[i] );
 567     for( unsigned j=0; j<cargs[i].size(); j++ ){
 568       std::stringstream sname;
 569       sname << name << "_" << j;
 570       c.addArg(sname.str(), cargs[i][j]);
 571     }
 572     dt.addConstructor(c);
 573   }
 574 }
 575
 576 // i is index in datatypes/ops
 577 // j is index is datatype
 578 Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
 579                               std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
 580                               Expr eval, const Datatype& dt, size_t i, size_t j ) {
 581   const DatatypeConstructor& ctor = dt[j];
 582   Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl;
 583   std::vector<Expr> bvs, extraArgs;
 584   for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
 585     std::string vname = "v_" + ctor[k].getName();
 586     Expr bv = getExprManager()->mkBoundVar(vname, SelectorType(ctor[k].getType()).getRangeType());
 587     bvs.push_back(bv);
 588     extraArgs.push_back(bv);
 589   }
 590   bvs.insert(bvs.end(), terms[0].begin(), terms[0].end());
 591   Expr bvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, bvs);
 592   Debug("parser-sygus") << "...made bv list " << bvl << std::endl;
 593   std::vector<Expr> patv;
 594   patv.push_back(eval);
 595   std::vector<Expr> applyv;
 596   applyv.push_back(ctor.getConstructor());
 597   applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end());
 598   for(size_t k = 0; k < applyv.size(); ++k) {
 599   }
 600   Expr cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
 601   Debug("parser-sygus") << "...made eval ctor apply " << cpatv << std::endl;
 602   patv.push_back(cpatv);
 603   patv.insert(patv.end(), terms[0].begin(), terms[0].end());
 604   Expr evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
 605   Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl;
 606   std::vector<Expr> builtApply;
 607   for(size_t k = 0; k < extraArgs.size(); ++k) {
 608     std::vector<Expr> patvb;
 609     patvb.push_back(evals[DatatypeType(extraArgs[k].getType())]);
 610     patvb.push_back(extraArgs[k]);
 611     patvb.insert(patvb.end(), terms[0].begin(), terms[0].end());
 612     builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb));
 613   }
 614   for(size_t k = 0; k < builtApply.size(); ++k) {
 615   }
 616   Expr builtTerm;
 617   //if( ops[i][j].getKind() == kind::BUILTIN ){
 618   if( !builtApply.empty() ){
 619     if( ops[i][j].getKind() != kind::BUILTIN ){
 620       builtTerm = getExprManager()->mkExpr(kind::APPLY, ops[i][j], builtApply);
 621     }else{
 622       builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
 623     }
 624   }else{
 625     builtTerm = ops[i][j];
 626   }
 627   Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
 628   Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
 629   Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
 630   pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
 631   assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern);
 632   Debug("parser-sygus") << "...made assertion " << assertion << std::endl;
 633
 634   //linearize multiplication if possible
 635   if( builtTerm.getKind()==kind::MULT ){
 636     for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
 637       Type at = SelectorType(ctor[k].getType()).getRangeType();
 638       if( at.isDatatype() ){
 639         DatatypeType atd = (DatatypeType)SelectorType(ctor[k].getType()).getRangeType();
 640         Debug("parser-sygus") << "Argument " << k << " " << atd << std::endl;
 641         std::vector<DatatypeType>::iterator itd = std::find( datatypeTypes.begin(), datatypeTypes.end(), atd );
 642         if( itd!=datatypeTypes.end() ){
 643           Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl;
 644           unsigned index = itd-datatypeTypes.begin();
 645           Debug("parser-sygus2") << "index = " << index << std::endl;
 646           bool isConst = true;
 647           for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
 648             Debug("parser-sygus2") << "ops[" << cc << "]=" << ops[index][cc] << std::endl;
 649             if( ops[index][cc].getKind() != kind::CONST_RATIONAL ){
 650               isConst = false;
 651               break;
 652             }
 653           }
 654           if( isConst ){
 655             Debug("parser-sygus") << "Linearize multiplication " << ctor << " based on argument " << k << std::endl;
 656             const Datatype & atdd = atd.getDatatype();
 657             std::vector<Expr> assertions;
 658             std::vector<Expr> nbvs;
 659             for( unsigned a=0; a<bvl.getNumChildren(); a++ ){
 660               if( a!=k ){
 661                 nbvs.push_back( bvl[a] );
 662               }
 663             }
 664             Expr nbvl = getExprManager()->mkExpr( kind::BOUND_VAR_LIST, nbvs );
 665             for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
 666               //Make new assertion based on partially instantiating existing
 667               applyv[k+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, atdd[cc].getConstructor());
 668               Debug("parser-sygus") << "applyv " << applyv[k+1] << std::endl;
 669               cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
 670               Debug("parser-sygus") << "cpatv " << cpatv << std::endl;
 671               patv[1] = cpatv;
 672               evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
 673               Debug("parser-sygus") << "evalApply " << evalApply << std::endl;
 674               builtApply[k] = ops[index][cc];
 675               Debug("parser-sygus") << "builtApply " << builtApply[k] << std::endl;
 676               builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
 677               Debug("parser-sygus") << "builtTerm " << builtTerm << std::endl;
 678               Expr eassertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
 679               Expr epattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
 680               epattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, epattern);
 681               eassertion = getExprManager()->mkExpr(kind::FORALL, nbvl, eassertion, epattern);
 682               assertions.push_back( eassertion );
 683             }
 684             assertion = assertions.size()==1 ? assertions[0] : getExprManager()->mkExpr( kind::AND, assertions );
 685             Debug("parser-sygus") << "...(linearized) assertion is: " << assertion << std::endl;
 686           }
 687         }
 688       }
 689     }
 690   }
 691   return assertion;
 692 }
 693
 694
 695 }/* CVC4::parser namespace */
 696 }/* CVC4 namespace */