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