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