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_unsatCoreNames.push(std::map<Expr, std::string>());
  35   if( !strictModeEnabled() ) {
  36     addTheory(Smt2::THEORY_CORE);
  37   }
  38 }
  39
  40 void Smt2::addArithmeticOperators() {
  41   Parser::addOperator(kind::PLUS);
  42   Parser::addOperator(kind::MINUS);
  43   Parser::addOperator(kind::UMINUS);
  44   Parser::addOperator(kind::MULT);
  45   Parser::addOperator(kind::LT);
  46   Parser::addOperator(kind::LEQ);
  47   Parser::addOperator(kind::GT);
  48   Parser::addOperator(kind::GEQ);
  49 }
  50
  51 void Smt2::addBitvectorOperators() {
  52   Parser::addOperator(kind::BITVECTOR_CONCAT);
  53   Parser::addOperator(kind::BITVECTOR_AND);
  54   Parser::addOperator(kind::BITVECTOR_OR);
  55   Parser::addOperator(kind::BITVECTOR_XOR);
  56   Parser::addOperator(kind::BITVECTOR_NOT);
  57   Parser::addOperator(kind::BITVECTOR_NAND);
  58   Parser::addOperator(kind::BITVECTOR_NOR);
  59   Parser::addOperator(kind::BITVECTOR_XNOR);
  60   Parser::addOperator(kind::BITVECTOR_COMP);
  61   Parser::addOperator(kind::BITVECTOR_MULT);
  62   Parser::addOperator(kind::BITVECTOR_PLUS);
  63   Parser::addOperator(kind::BITVECTOR_SUB);
  64   Parser::addOperator(kind::BITVECTOR_NEG);
  65   Parser::addOperator(kind::BITVECTOR_UDIV);
  66   Parser::addOperator(kind::BITVECTOR_UREM);
  67   Parser::addOperator(kind::BITVECTOR_SDIV);
  68   Parser::addOperator(kind::BITVECTOR_SREM);
  69   Parser::addOperator(kind::BITVECTOR_SMOD);
  70   Parser::addOperator(kind::BITVECTOR_SHL);
  71   Parser::addOperator(kind::BITVECTOR_LSHR);
  72   Parser::addOperator(kind::BITVECTOR_ASHR);
  73   Parser::addOperator(kind::BITVECTOR_ULT);
  74   Parser::addOperator(kind::BITVECTOR_ULE);
  75   Parser::addOperator(kind::BITVECTOR_UGT);
  76   Parser::addOperator(kind::BITVECTOR_UGE);
  77   Parser::addOperator(kind::BITVECTOR_SLT);
  78   Parser::addOperator(kind::BITVECTOR_SLE);
  79   Parser::addOperator(kind::BITVECTOR_SGT);
  80   Parser::addOperator(kind::BITVECTOR_SGE);
  81   Parser::addOperator(kind::BITVECTOR_BITOF);
  82   Parser::addOperator(kind::BITVECTOR_EXTRACT);
  83   Parser::addOperator(kind::BITVECTOR_REPEAT);
  84   Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND);
  85   Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND);
  86   Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT);
  87   Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT);
  88
  89   Parser::addOperator(kind::INT_TO_BITVECTOR);
  90   Parser::addOperator(kind::BITVECTOR_TO_NAT);
  91 }
  92
  93 void Smt2::addStringOperators() {
  94   Parser::addOperator(kind::STRING_CONCAT);
  95   Parser::addOperator(kind::STRING_LENGTH);
  96 }
  97
  98 void Smt2::addFloatingPointOperators() {
  99   Parser::addOperator(kind::FLOATINGPOINT_FP);
 100   Parser::addOperator(kind::FLOATINGPOINT_EQ);
 101   Parser::addOperator(kind::FLOATINGPOINT_ABS);
 102   Parser::addOperator(kind::FLOATINGPOINT_NEG);
 103   Parser::addOperator(kind::FLOATINGPOINT_PLUS);
 104   Parser::addOperator(kind::FLOATINGPOINT_SUB);
 105   Parser::addOperator(kind::FLOATINGPOINT_MULT);
 106   Parser::addOperator(kind::FLOATINGPOINT_DIV);
 107   Parser::addOperator(kind::FLOATINGPOINT_FMA);
 108   Parser::addOperator(kind::FLOATINGPOINT_SQRT);
 109   Parser::addOperator(kind::FLOATINGPOINT_REM);
 110   Parser::addOperator(kind::FLOATINGPOINT_RTI);
 111   Parser::addOperator(kind::FLOATINGPOINT_MIN);
 112   Parser::addOperator(kind::FLOATINGPOINT_MAX);
 113   Parser::addOperator(kind::FLOATINGPOINT_LEQ);
 114   Parser::addOperator(kind::FLOATINGPOINT_LT);
 115   Parser::addOperator(kind::FLOATINGPOINT_GEQ);
 116   Parser::addOperator(kind::FLOATINGPOINT_GT);
 117   Parser::addOperator(kind::FLOATINGPOINT_ISN);
 118   Parser::addOperator(kind::FLOATINGPOINT_ISSN);
 119   Parser::addOperator(kind::FLOATINGPOINT_ISZ);
 120   Parser::addOperator(kind::FLOATINGPOINT_ISINF);
 121   Parser::addOperator(kind::FLOATINGPOINT_ISNAN);
 122   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
 123   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
 124   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL);
 125   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
 126   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
 127   Parser::addOperator(kind::FLOATINGPOINT_TO_UBV);
 128   Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
 129   Parser::addOperator(kind::FLOATINGPOINT_TO_REAL);
 130 }
 131
 132
 133 void Smt2::addTheory(Theory theory) {
 134   switch(theory) {
 135   case THEORY_ARRAYS:
 136     Parser::addOperator(kind::SELECT);
 137     Parser::addOperator(kind::STORE);
 138     break;
 139
 140   case THEORY_BITVECTORS:
 141     addBitvectorOperators();
 142     break;
 143
 144   case THEORY_CORE:
 145     defineType("Bool", getExprManager()->booleanType());
 146     defineVar("true", getExprManager()->mkConst(true));
 147     defineVar("false", getExprManager()->mkConst(false));
 148     Parser::addOperator(kind::AND);
 149     Parser::addOperator(kind::DISTINCT);
 150     Parser::addOperator(kind::EQUAL);
 151     Parser::addOperator(kind::IFF);
 152     Parser::addOperator(kind::IMPLIES);
 153     Parser::addOperator(kind::ITE);
 154     Parser::addOperator(kind::NOT);
 155     Parser::addOperator(kind::OR);
 156     Parser::addOperator(kind::XOR);
 157     break;
 158
 159   case THEORY_REALS_INTS:
 160     defineType("Real", getExprManager()->realType());
 161     Parser::addOperator(kind::DIVISION);
 162     Parser::addOperator(kind::TO_INTEGER);
 163     Parser::addOperator(kind::IS_INTEGER);
 164     Parser::addOperator(kind::TO_REAL);
 165     // falling through on purpose, to add Ints part of Reals_Ints
 166   case THEORY_INTS:
 167     defineType("Int", getExprManager()->integerType());
 168     addArithmeticOperators();
 169     Parser::addOperator(kind::INTS_DIVISION);
 170     Parser::addOperator(kind::INTS_MODULUS);
 171     Parser::addOperator(kind::ABS);
 172     Parser::addOperator(kind::DIVISIBLE);
 173     break;
 174
 175   case THEORY_REALS:
 176     defineType("Real", getExprManager()->realType());
 177     addArithmeticOperators();
 178     Parser::addOperator(kind::DIVISION);
 179     break;
 180
 181   case THEORY_QUANTIFIERS:
 182     break;
 183
 184   case THEORY_SETS:
 185     addOperator(kind::UNION, "union");
 186     addOperator(kind::INTERSECTION, "intersection");
 187     addOperator(kind::SETMINUS, "setminus");
 188     addOperator(kind::SUBSET, "subset");
 189     addOperator(kind::MEMBER, "member");
 190     addOperator(kind::SINGLETON, "singleton");
 191     addOperator(kind::INSERT, "insert");
 192     break;
 193
 194   case THEORY_DATATYPES:
 195     Parser::addOperator(kind::APPLY_CONSTRUCTOR);
 196     Parser::addOperator(kind::APPLY_TESTER);
 197     Parser::addOperator(kind::APPLY_SELECTOR);
 198     Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
 199     break;
 200
 201   case THEORY_STRINGS:
 202     defineType("String", getExprManager()->stringType());
 203     addStringOperators();
 204     break;
 205
 206   case THEORY_UF:
 207     Parser::addOperator(kind::APPLY_UF);
 208     break;
 209
 210   case THEORY_FP:
 211     defineType("RoundingMode", getExprManager()->roundingModeType());
 212     defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
 213     defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
 214     defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
 215     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
 216     addFloatingPointOperators();
 217     break;
 218
 219   default:
 220     std::stringstream ss;
 221     ss << "internal error: unsupported theory " << theory;
 222     throw ParserException(ss.str());
 223   }
 224 }
 225
 226 void Smt2::addOperator(Kind kind, const std::string& name) {
 227   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 228                   << std::endl;
 229   Parser::addOperator(kind);
 230   operatorKindMap[name] = kind;
 231 }
 232
 233 Kind Smt2::getOperatorKind(const std::string& name) const {
 234   // precondition: isOperatorEnabled(name)
 235   return operatorKindMap.find(name)->second;
 236 }
 237
 238 bool Smt2::isOperatorEnabled(const std::string& name) const {
 239   return operatorKindMap.find(name) != operatorKindMap.end();
 240 }
 241
 242 bool Smt2::isTheoryEnabled(Theory theory) const {
 243   switch(theory) {
 244   case THEORY_ARRAYS:
 245     return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
 246   case THEORY_BITVECTORS:
 247     return d_logic.isTheoryEnabled(theory::THEORY_BV);
 248   case THEORY_CORE:
 249     return true;
 250   case THEORY_DATATYPES:
 251     return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
 252   case THEORY_INTS:
 253     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 254       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
 255   case THEORY_REALS:
 256     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 257       ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
 258   case THEORY_REALS_INTS:
 259     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 260       d_logic.areIntegersUsed() && d_logic.areRealsUsed();
 261   case THEORY_QUANTIFIERS:
 262     return d_logic.isQuantified();
 263   case THEORY_SETS:
 264     return d_logic.isTheoryEnabled(theory::THEORY_SETS);
 265   case THEORY_STRINGS:
 266     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
 267   case THEORY_UF:
 268     return d_logic.isTheoryEnabled(theory::THEORY_UF);
 269   case THEORY_FP:
 270     return d_logic.isTheoryEnabled(theory::THEORY_FP);
 271   default:
 272     std::stringstream ss;
 273     ss << "internal error: unsupported theory " << theory;
 274     throw ParserException(ss.str());
 275   }
 276 }
 277
 278 bool Smt2::logicIsSet() {
 279   return d_logicSet;
 280 }
 281
 282 void Smt2::reset() {
 283   d_logicSet = false;
 284   d_logic = LogicInfo();
 285   operatorKindMap.clear();
 286   d_lastNamedTerm = std::pair<Expr, std::string>();
 287   d_unsatCoreNames = std::stack< std::map<Expr, std::string> >();
 288   this->Parser::reset();
 289
 290   d_unsatCoreNames.push(std::map<Expr, std::string>());
 291   if( !strictModeEnabled() ) {
 292     addTheory(Smt2::THEORY_CORE);
 293   }
 294 }
 295
 296 void Smt2::resetAssertions() {
 297   this->Parser::reset();
 298 }
 299
 300 void Smt2::setLogic(const std::string& name) {
 301   d_logicSet = true;
 302   if(logicIsForced()) {
 303     d_logic = getForcedLogic();
 304   } else {
 305     d_logic = name;
 306   }
 307
 308   // Core theory belongs to every logic
 309   addTheory(THEORY_CORE);
 310
 311   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 312     addTheory(THEORY_UF);
 313   }
 314
 315   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 316     if(d_logic.areIntegersUsed()) {
 317       if(d_logic.areRealsUsed()) {
 318         addTheory(THEORY_REALS_INTS);
 319       } else {
 320         addTheory(THEORY_INTS);
 321       }
 322     } else if(d_logic.areRealsUsed()) {
 323       addTheory(THEORY_REALS);
 324     }
 325   }
 326
 327   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
 328     addTheory(THEORY_ARRAYS);
 329   }
 330
 331   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 332     addTheory(THEORY_BITVECTORS);
 333   }
 334
 335   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
 336     addTheory(THEORY_DATATYPES);
 337   }
 338
 339   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 340     addTheory(THEORY_SETS);
 341   }
 342
 343   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 344     addTheory(THEORY_STRINGS);
 345   }
 346
 347   if(d_logic.isQuantified()) {
 348     addTheory(THEORY_QUANTIFIERS);
 349   }
 350
 351   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
 352     addTheory(THEORY_FP);
 353   }
 354
 355 }/* Smt2::setLogic() */
 356
 357 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 358   // TODO: ???
 359 }
 360
 361 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 362   // TODO: ???
 363 }
 364
 365 void Smt2::checkThatLogicIsSet() {
 366   if( ! logicIsSet() ) {
 367     if( strictModeEnabled() ) {
 368       parseError("set-logic must appear before this point.");
 369     } else {
 370       warning("No set-logic command was given before this point.");
 371       warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
 372       warning("Consider setting a stricter logic for (likely) better performance.");
 373       warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 374
 375       setLogic("ALL_SUPPORTED");
 376
 377       Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
 378       c->setMuted(true);
 379       preemptCommand(c);
 380     }
 381   }
 382 }
 383
 384 /* The include are managed in the lexer but called in the parser */
 385 // Inspired by http://www.antlr3.org/api/C/interop.html
 386
 387 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 388   Debug("parser") << "Including " << filename << std::endl;
 389   // Create a new input stream and take advantage of built in stream stacking
 390   // in C target runtime.
 391   //
 392   pANTLR3_INPUT_STREAM    in;
 393 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 394   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 395 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 396   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 397 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 398   if( in == NULL ) {
 399     Debug("parser") << "Can't open " << filename << std::endl;
 400     return false;
 401   }
 402   // Same thing as the predefined PUSHSTREAM(in);
 403   lexer->pushCharStream(lexer, in);
 404   // restart it
 405   //lexer->rec->state->tokenStartCharIndex      = -10;
 406   //lexer->emit(lexer);
 407
 408   // Note that the input stream is not closed when it EOFs, I don't bother
 409   // to do it here, but it is up to you to track streams created like this
 410   // and destroy them when the whole parse session is complete. Remember that you
 411   // don't want to do this until all tokens have been manipulated all the way through
 412   // your tree parsers etc as the token does not store the text it just refers
 413   // back to the input stream and trying to get the text for it will abort if you
 414   // close the input stream too early.
 415
 416   //TODO what said before
 417   return true;
 418 }
 419
 420 void Smt2::includeFile(const std::string& filename) {
 421   // security for online version
 422   if(!canIncludeFile()) {
 423     parseError("include-file feature was disabled for this run.");
 424   }
 425
 426   // Get the lexer
 427   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 428   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 429   // get the name of the current stream "Does it work inside an include?"
 430   const std::string inputName = ai->getInputStreamName();
 431
 432   // Find the directory of the current input file
 433   std::string path;
 434   size_t pos = inputName.rfind('/');
 435   if(pos != std::string::npos) {
 436     path = std::string(inputName, 0, pos + 1);
 437   }
 438   path.append(filename);
 439   if(!newInputStream(path, lexer)) {
 440     parseError("Couldn't open include file `" + path + "'");
 441   }
 442 }
 443
 444 }/* CVC4::parser namespace */
 445 }/* CVC4 namespace */