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   Parser::addOperator(kind::STRING_CONCAT);
  97   Parser::addOperator(kind::STRING_LENGTH);
  98 }
  99
 100 void Smt2::addFloatingPointOperators() {
 101   Parser::addOperator(kind::FLOATINGPOINT_FP);
 102   Parser::addOperator(kind::FLOATINGPOINT_EQ);
 103   Parser::addOperator(kind::FLOATINGPOINT_ABS);
 104   Parser::addOperator(kind::FLOATINGPOINT_NEG);
 105   Parser::addOperator(kind::FLOATINGPOINT_PLUS);
 106   Parser::addOperator(kind::FLOATINGPOINT_SUB);
 107   Parser::addOperator(kind::FLOATINGPOINT_MULT);
 108   Parser::addOperator(kind::FLOATINGPOINT_DIV);
 109   Parser::addOperator(kind::FLOATINGPOINT_FMA);
 110   Parser::addOperator(kind::FLOATINGPOINT_SQRT);
 111   Parser::addOperator(kind::FLOATINGPOINT_REM);
 112   Parser::addOperator(kind::FLOATINGPOINT_RTI);
 113   Parser::addOperator(kind::FLOATINGPOINT_MIN);
 114   Parser::addOperator(kind::FLOATINGPOINT_MAX);
 115   Parser::addOperator(kind::FLOATINGPOINT_LEQ);
 116   Parser::addOperator(kind::FLOATINGPOINT_LT);
 117   Parser::addOperator(kind::FLOATINGPOINT_GEQ);
 118   Parser::addOperator(kind::FLOATINGPOINT_GT);
 119   Parser::addOperator(kind::FLOATINGPOINT_ISN);
 120   Parser::addOperator(kind::FLOATINGPOINT_ISSN);
 121   Parser::addOperator(kind::FLOATINGPOINT_ISZ);
 122   Parser::addOperator(kind::FLOATINGPOINT_ISINF);
 123   Parser::addOperator(kind::FLOATINGPOINT_ISNAN);
 124   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
 125   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
 126   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL);
 127   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
 128   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
 129   Parser::addOperator(kind::FLOATINGPOINT_TO_UBV);
 130   Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
 131   Parser::addOperator(kind::FLOATINGPOINT_TO_REAL);
 132 }
 133
 134
 135 void Smt2::addTheory(Theory theory) {
 136   switch(theory) {
 137   case THEORY_ARRAYS:
 138     addOperator(kind::SELECT, "select");
 139     addOperator(kind::STORE, "store");
 140     break;
 141
 142   case THEORY_BITVECTORS:
 143     addBitvectorOperators();
 144     break;
 145
 146   case THEORY_CORE:
 147     defineType("Bool", getExprManager()->booleanType());
 148     defineVar("true", getExprManager()->mkConst(true));
 149     defineVar("false", getExprManager()->mkConst(false));
 150     Parser::addOperator(kind::AND);
 151     Parser::addOperator(kind::DISTINCT);
 152     Parser::addOperator(kind::EQUAL);
 153     Parser::addOperator(kind::IFF);
 154     Parser::addOperator(kind::IMPLIES);
 155     Parser::addOperator(kind::ITE);
 156     Parser::addOperator(kind::NOT);
 157     Parser::addOperator(kind::OR);
 158     Parser::addOperator(kind::XOR);
 159     break;
 160
 161   case THEORY_REALS_INTS:
 162     defineType("Real", getExprManager()->realType());
 163     Parser::addOperator(kind::DIVISION);
 164     addOperator(kind::TO_INTEGER, "to_int");
 165     addOperator(kind::IS_INTEGER, "is_int");
 166     addOperator(kind::TO_REAL, "to_real");
 167     // falling through on purpose, to add Ints part of Reals_Ints
 168   case THEORY_INTS:
 169     defineType("Int", getExprManager()->integerType());
 170     addArithmeticOperators();
 171     addOperator(kind::INTS_DIVISION, "div");
 172     addOperator(kind::INTS_MODULUS, "mod");
 173     addOperator(kind::ABS, "abs");
 174     Parser::addOperator(kind::DIVISIBLE);
 175     break;
 176
 177   case THEORY_REALS:
 178     defineType("Real", getExprManager()->realType());
 179     addArithmeticOperators();
 180     Parser::addOperator(kind::DIVISION);
 181     break;
 182
 183   case THEORY_QUANTIFIERS:
 184     break;
 185
 186   case THEORY_SETS:
 187     addOperator(kind::UNION, "union");
 188     addOperator(kind::INTERSECTION, "intersection");
 189     addOperator(kind::SETMINUS, "setminus");
 190     addOperator(kind::SUBSET, "subset");
 191     addOperator(kind::MEMBER, "member");
 192     addOperator(kind::SINGLETON, "singleton");
 193     addOperator(kind::INSERT, "insert");
 194     break;
 195
 196   case THEORY_DATATYPES:
 197     Parser::addOperator(kind::APPLY_CONSTRUCTOR);
 198     Parser::addOperator(kind::APPLY_TESTER);
 199     Parser::addOperator(kind::APPLY_SELECTOR);
 200     Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
 201     break;
 202
 203   case THEORY_STRINGS:
 204     defineType("String", getExprManager()->stringType());
 205     addStringOperators();
 206     break;
 207
 208   case THEORY_UF:
 209     Parser::addOperator(kind::APPLY_UF);
 210     break;
 211
 212   case THEORY_FP:
 213     defineType("RoundingMode", getExprManager()->roundingModeType());
 214     defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
 215     defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
 216     defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
 217     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
 218     addFloatingPointOperators();
 219     break;
 220
 221   default:
 222     std::stringstream ss;
 223     ss << "internal error: unsupported theory " << theory;
 224     throw ParserException(ss.str());
 225   }
 226 }
 227
 228 void Smt2::addOperator(Kind kind, const std::string& name) {
 229   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 230                   << std::endl;
 231   Parser::addOperator(kind);
 232   operatorKindMap[name] = kind;
 233 }
 234
 235 Kind Smt2::getOperatorKind(const std::string& name) const {
 236   // precondition: isOperatorEnabled(name)
 237   return operatorKindMap.find(name)->second;
 238 }
 239
 240 bool Smt2::isOperatorEnabled(const std::string& name) const {
 241   return operatorKindMap.find(name) != operatorKindMap.end();
 242 }
 243
 244 bool Smt2::isTheoryEnabled(Theory theory) const {
 245   switch(theory) {
 246   case THEORY_ARRAYS:
 247     return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
 248   case THEORY_BITVECTORS:
 249     return d_logic.isTheoryEnabled(theory::THEORY_BV);
 250   case THEORY_CORE:
 251     return true;
 252   case THEORY_DATATYPES:
 253     return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
 254   case THEORY_INTS:
 255     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 256       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
 257   case THEORY_REALS:
 258     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 259       ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
 260   case THEORY_REALS_INTS:
 261     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 262       d_logic.areIntegersUsed() && d_logic.areRealsUsed();
 263   case THEORY_QUANTIFIERS:
 264     return d_logic.isQuantified();
 265   case THEORY_SETS:
 266     return d_logic.isTheoryEnabled(theory::THEORY_SETS);
 267   case THEORY_STRINGS:
 268     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
 269   case THEORY_UF:
 270     return d_logic.isTheoryEnabled(theory::THEORY_UF);
 271   case THEORY_FP:
 272     return d_logic.isTheoryEnabled(theory::THEORY_FP);
 273   default:
 274     std::stringstream ss;
 275     ss << "internal error: unsupported theory " << theory;
 276     throw ParserException(ss.str());
 277   }
 278 }
 279
 280 bool Smt2::logicIsSet() {
 281   return d_logicSet;
 282 }
 283
 284 void Smt2::reset() {
 285   d_logicSet = false;
 286   d_logic = LogicInfo();
 287   operatorKindMap.clear();
 288   d_lastNamedTerm = std::pair<Expr, std::string>();
 289   d_unsatCoreNames = std::stack< std::map<Expr, std::string> >();
 290   this->Parser::reset();
 291
 292   d_unsatCoreNames.push(std::map<Expr, std::string>());
 293   if( !strictModeEnabled() ) {
 294     addTheory(Smt2::THEORY_CORE);
 295   }
 296 }
 297
 298 void Smt2::resetAssertions() {
 299   this->Parser::reset();
 300 }
 301
 302 void Smt2::setLogic(std::string name) {
 303   if(sygus()) {
 304     if(name == "Arrays") {
 305       name = "AUF";
 306     } else if(name == "Reals") {
 307       name = "UFLRA";
 308     } else if(name == "LIA") {
 309       name = "UFLIA";
 310     } else if(name == "LRA") {
 311       name = "UFLRA";
 312     } else if(name == "LIRA") {
 313       name = "UFLIRA";
 314     } else if(name == "BV") {
 315       name = "UFBV";
 316     } else {
 317       std::stringstream ss;
 318       ss << "Unknown SyGuS background logic `" << name << "'";
 319       parseError(ss.str());
 320     }
 321   }
 322
 323   d_logicSet = true;
 324   if(logicIsForced()) {
 325     d_logic = getForcedLogic();
 326   } else {
 327     d_logic = name;
 328   }
 329
 330   // Core theory belongs to every logic
 331   addTheory(THEORY_CORE);
 332
 333   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 334     addTheory(THEORY_UF);
 335   }
 336
 337   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 338     if(d_logic.areIntegersUsed()) {
 339       if(d_logic.areRealsUsed()) {
 340         addTheory(THEORY_REALS_INTS);
 341       } else {
 342         addTheory(THEORY_INTS);
 343       }
 344     } else if(d_logic.areRealsUsed()) {
 345       addTheory(THEORY_REALS);
 346     }
 347   }
 348
 349   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
 350     addTheory(THEORY_ARRAYS);
 351   }
 352
 353   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 354     addTheory(THEORY_BITVECTORS);
 355   }
 356
 357   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
 358     addTheory(THEORY_DATATYPES);
 359   }
 360
 361   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 362     addTheory(THEORY_SETS);
 363   }
 364
 365   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 366     addTheory(THEORY_STRINGS);
 367   }
 368
 369   if(d_logic.isQuantified()) {
 370     addTheory(THEORY_QUANTIFIERS);
 371   }
 372
 373   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
 374     addTheory(THEORY_FP);
 375   }
 376
 377 }/* Smt2::setLogic() */
 378
 379 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 380   // TODO: ???
 381 }
 382
 383 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 384   // TODO: ???
 385 }
 386
 387 void Smt2::checkThatLogicIsSet() {
 388   if( ! logicIsSet() ) {
 389     if(strictModeEnabled()) {
 390       parseError("set-logic must appear before this point.");
 391     } else {
 392       if(sygus()) {
 393         setLogic("LIA");
 394       } else {
 395         warning("No set-logic command was given before this point.");
 396         warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
 397         warning("Consider setting a stricter logic for (likely) better performance.");
 398         warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 399
 400         setLogic("ALL_SUPPORTED");
 401       }
 402
 403       Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
 404       c->setMuted(true);
 405       preemptCommand(c);
 406     }
 407   }
 408 }
 409
 410 /* The include are managed in the lexer but called in the parser */
 411 // Inspired by http://www.antlr3.org/api/C/interop.html
 412
 413 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 414   Debug("parser") << "Including " << filename << std::endl;
 415   // Create a new input stream and take advantage of built in stream stacking
 416   // in C target runtime.
 417   //
 418   pANTLR3_INPUT_STREAM    in;
 419 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 420   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 421 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 422   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 423 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 424   if( in == NULL ) {
 425     Debug("parser") << "Can't open " << filename << std::endl;
 426     return false;
 427   }
 428   // Same thing as the predefined PUSHSTREAM(in);
 429   lexer->pushCharStream(lexer, in);
 430   // restart it
 431   //lexer->rec->state->tokenStartCharIndex      = -10;
 432   //lexer->emit(lexer);
 433
 434   // Note that the input stream is not closed when it EOFs, I don't bother
 435   // to do it here, but it is up to you to track streams created like this
 436   // and destroy them when the whole parse session is complete. Remember that you
 437   // don't want to do this until all tokens have been manipulated all the way through
 438   // your tree parsers etc as the token does not store the text it just refers
 439   // back to the input stream and trying to get the text for it will abort if you
 440   // close the input stream too early.
 441
 442   //TODO what said before
 443   return true;
 444 }
 445
 446 void Smt2::includeFile(const std::string& filename) {
 447   // security for online version
 448   if(!canIncludeFile()) {
 449     parseError("include-file feature was disabled for this run.");
 450   }
 451
 452   // Get the lexer
 453   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 454   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 455   // get the name of the current stream "Does it work inside an include?"
 456   const std::string inputName = ai->getInputStreamName();
 457
 458   // Find the directory of the current input file
 459   std::string path;
 460   size_t pos = inputName.rfind('/');
 461   if(pos != std::string::npos) {
 462     path = std::string(inputName, 0, pos + 1);
 463   }
 464   path.append(filename);
 465   if(!newInputStream(path, lexer)) {
 466     parseError("Couldn't open include file `" + path + "'");
 467   }
 468 }
 469
 470
 471
 472  void Smt2::defineSygusFuns() {
 473   // only define each one once
 474   while(d_nextSygusFun < d_sygusFuns.size()) {
 475     std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun];
 476     std::string fun = p.first;
 477     Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl;
 478     Expr eval = p.second;
 479     FunctionType evalType = eval.getType();
 480     std::vector<Type> argTypes = evalType.getArgTypes();
 481     Type rangeType = evalType.getRangeType();
 482     Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl;
 483
 484     // first make the function type
 485     std::vector<Expr> sygusVars;
 486     std::vector<Type> funType;
 487     for(size_t j = 1; j < argTypes.size(); ++j) {
 488       funType.push_back(argTypes[j]);
 489       std::stringstream ss;
 490       ss << fun << "_v_" << j;
 491       sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), argTypes[j]));
 492     }
 493     Type funt = getExprManager()->mkFunctionType(funType, rangeType);
 494     Debug("parser-sygus") << "...eval function type : " << funt << std::endl;
 495
 496     // copy the bound vars
 497     /*
 498     std::vector<Expr> sygusVars;
 499     //std::vector<Type> types;
 500     for(size_t i = 0; i < d_sygusVars.size(); ++i) {
 501       std::stringstream ss;
 502       ss << d_sygusVars[i];
 503       Type type = d_sygusVars[i].getType();
 504       sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
 505       //types.push_back(type);
 506     }
 507     Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
 508     */
 509
 510     //Type t = getExprManager()->mkFunctionType(types, rangeType);
 511     //Debug("parser-sygus") << "...function type : " << t << std::endl;
 512
 513     Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED);
 514     Debug("parser-sygus") << "...made function : " << lambda << std::endl;
 515     std::vector<Expr> applyv;
 516     Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]);
 517     d_sygusFunSymbols.push_back(funbv);
 518     applyv.push_back(eval);
 519     applyv.push_back(funbv);
 520     for(size_t i = 0; i < sygusVars.size(); ++i) {
 521       applyv.push_back(sygusVars[i]);
 522     }
 523     Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv);
 524     Debug("parser-sygus") << "...made apply " << apply << std::endl;
 525     Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply);
 526     preemptCommand(cmd);
 527
 528     ++d_nextSygusFun;
 529   }
 530 }
 531
 532 void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
 533                             std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ) {
 534   for( unsigned i=0; i<cnames.size(); i++ ){
 535     std::string name = dt.getName() + "_" + cnames[i];
 536     std::string testerId("is-");
 537     testerId.append(name);
 538     checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
 539     checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
 540     CVC4::DatatypeConstructor c(name, testerId, ops[i] );
 541     for( unsigned j=0; j<cargs[i].size(); j++ ){
 542       std::stringstream sname;
 543       sname << name << "_" << j;
 544       c.addArg(sname.str(), cargs[i][j]);
 545     }
 546     dt.addConstructor(c);
 547   }
 548 }
 549
 550 // i is index in datatypes/ops
 551 // j is index is datatype
 552 Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
 553                               std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
 554                               Expr eval, const Datatype& dt, size_t i, size_t j ) {
 555   const DatatypeConstructor& ctor = dt[j];
 556   Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl;
 557   std::vector<Expr> bvs, extraArgs;
 558   for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
 559     std::string vname = "v_" + ctor[k].getName();
 560     Expr bv = getExprManager()->mkBoundVar(vname, SelectorType(ctor[k].getType()).getRangeType());
 561     bvs.push_back(bv);
 562     extraArgs.push_back(bv);
 563   }
 564   bvs.insert(bvs.end(), terms[0].begin(), terms[0].end());
 565   Expr bvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, bvs);
 566   Debug("parser-sygus") << "...made bv list " << bvl << std::endl;
 567   std::vector<Expr> patv;
 568   patv.push_back(eval);
 569   std::vector<Expr> applyv;
 570   applyv.push_back(ctor.getConstructor());
 571   applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end());
 572   for(size_t k = 0; k < applyv.size(); ++k) {
 573   }
 574   Expr cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
 575   Debug("parser-sygus") << "...made eval ctor apply " << cpatv << std::endl;
 576   patv.push_back(cpatv);
 577   patv.insert(patv.end(), terms[0].begin(), terms[0].end());
 578   Expr evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
 579   Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl;
 580   std::vector<Expr> builtApply;
 581   for(size_t k = 0; k < extraArgs.size(); ++k) {
 582     std::vector<Expr> patvb;
 583     patvb.push_back(evals[DatatypeType(extraArgs[k].getType())]);
 584     patvb.push_back(extraArgs[k]);
 585     patvb.insert(patvb.end(), terms[0].begin(), terms[0].end());
 586     builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb));
 587   }
 588   for(size_t k = 0; k < builtApply.size(); ++k) {
 589   }
 590   Expr builtTerm;
 591   //if( ops[i][j].getKind() == kind::BUILTIN ){
 592   if( !builtApply.empty() ){
 593     if( ops[i][j].getKind() != kind::BUILTIN ){
 594       builtTerm = getExprManager()->mkExpr(kind::APPLY, ops[i][j], builtApply);
 595     }else{
 596       builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
 597     }
 598   }else{
 599     builtTerm = ops[i][j];
 600   }
 601   Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
 602   Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
 603   Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
 604   pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
 605   assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern);
 606   Debug("parser-sygus") << "...made assertion " << assertion << std::endl;
 607
 608   //linearize multiplication if possible
 609   if( builtTerm.getKind()==kind::MULT ){
 610     for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
 611       Type at = SelectorType(ctor[k].getType()).getRangeType();
 612       if( at.isDatatype() ){
 613         DatatypeType atd = (DatatypeType)SelectorType(ctor[k].getType()).getRangeType();
 614         Debug("parser-sygus") << "Argument " << k << " " << atd << std::endl;
 615         std::vector<DatatypeType>::iterator itd = std::find( datatypeTypes.begin(), datatypeTypes.end(), atd );
 616         if( itd!=datatypeTypes.end() ){
 617           Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl;
 618           unsigned index = itd-datatypeTypes.begin();
 619           Debug("parser-sygus2") << "index = " << index << std::endl;
 620           bool isConst = true;
 621           for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
 622             Debug("parser-sygus2") << "ops[" << cc << "]=" << ops[index][cc] << std::endl;
 623             if( ops[index][cc].getKind() != kind::CONST_RATIONAL ){
 624               isConst = false;
 625               break;
 626             }
 627           }
 628           if( isConst ){
 629             Debug("parser-sygus") << "Linearize multiplication " << ctor << " based on argument " << k << std::endl;
 630             const Datatype & atdd = atd.getDatatype();
 631             std::vector<Expr> assertions;
 632             std::vector<Expr> nbvs;
 633             for( unsigned a=0; a<bvl.getNumChildren(); a++ ){
 634               if( a!=k ){
 635                 nbvs.push_back( bvl[a] );
 636               }
 637             }
 638             Expr nbvl = getExprManager()->mkExpr( kind::BOUND_VAR_LIST, nbvs );
 639             for( unsigned cc = 0; cc < ops[index].size(); cc++ ){
 640               //Make new assertion based on partially instantiating existing
 641               applyv[k+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, atdd[cc].getConstructor());
 642               Debug("parser-sygus") << "applyv " << applyv[k+1] << std::endl;
 643               cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
 644               Debug("parser-sygus") << "cpatv " << cpatv << std::endl;
 645               patv[1] = cpatv;
 646               evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
 647               Debug("parser-sygus") << "evalApply " << evalApply << std::endl;
 648               builtApply[k] = ops[index][cc];
 649               Debug("parser-sygus") << "builtApply " << builtApply[k] << std::endl;
 650               builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
 651               Debug("parser-sygus") << "builtTerm " << builtTerm << std::endl;
 652               Expr eassertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
 653               Expr epattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
 654               epattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, epattern);
 655               eassertion = getExprManager()->mkExpr(kind::FORALL, nbvl, eassertion, epattern);
 656               assertions.push_back( eassertion );
 657             }
 658             assertion = assertions.size()==1 ? assertions[0] : getExprManager()->mkExpr( kind::AND, assertions );
 659             Debug("parser-sygus") << "...(linearized) assertion is: " << assertion << std::endl;
 660           }
 661         }
 662       }
 663     }
 664   }
 665   return assertion;
 666 }
 667
 668
 669 }/* CVC4::parser namespace */
 670 }/* CVC4 namespace */