src/parser/smt2/smt2.cpp

   1 /*********************                                                        */
   2 /*! \file smt2.cpp
   3  ** \verbatim
   4  ** Original author: Christopher L. Conway
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): Clark Barrett, Tianyi Liang
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  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   if( !strictModeEnabled() ) {
  35     addTheory(Smt2::THEORY_CORE);
  36   }
  37 }
  38
  39 void Smt2::addArithmeticOperators() {
  40   Parser::addOperator(kind::PLUS);
  41   Parser::addOperator(kind::MINUS);
  42   Parser::addOperator(kind::UMINUS);
  43   Parser::addOperator(kind::MULT);
  44   Parser::addOperator(kind::LT);
  45   Parser::addOperator(kind::LEQ);
  46   Parser::addOperator(kind::GT);
  47   Parser::addOperator(kind::GEQ);
  48 }
  49
  50 void Smt2::addBitvectorOperators() {
  51   Parser::addOperator(kind::BITVECTOR_CONCAT);
  52   Parser::addOperator(kind::BITVECTOR_AND);
  53   Parser::addOperator(kind::BITVECTOR_OR);
  54   Parser::addOperator(kind::BITVECTOR_XOR);
  55   Parser::addOperator(kind::BITVECTOR_NOT);
  56   Parser::addOperator(kind::BITVECTOR_NAND);
  57   Parser::addOperator(kind::BITVECTOR_NOR);
  58   Parser::addOperator(kind::BITVECTOR_XNOR);
  59   Parser::addOperator(kind::BITVECTOR_COMP);
  60   Parser::addOperator(kind::BITVECTOR_MULT);
  61   Parser::addOperator(kind::BITVECTOR_PLUS);
  62   Parser::addOperator(kind::BITVECTOR_SUB);
  63   Parser::addOperator(kind::BITVECTOR_NEG);
  64   Parser::addOperator(kind::BITVECTOR_UDIV);
  65   Parser::addOperator(kind::BITVECTOR_UREM);
  66   Parser::addOperator(kind::BITVECTOR_SDIV);
  67   Parser::addOperator(kind::BITVECTOR_SREM);
  68   Parser::addOperator(kind::BITVECTOR_SMOD);
  69   Parser::addOperator(kind::BITVECTOR_SHL);
  70   Parser::addOperator(kind::BITVECTOR_LSHR);
  71   Parser::addOperator(kind::BITVECTOR_ASHR);
  72   Parser::addOperator(kind::BITVECTOR_ULT);
  73   Parser::addOperator(kind::BITVECTOR_ULE);
  74   Parser::addOperator(kind::BITVECTOR_UGT);
  75   Parser::addOperator(kind::BITVECTOR_UGE);
  76   Parser::addOperator(kind::BITVECTOR_SLT);
  77   Parser::addOperator(kind::BITVECTOR_SLE);
  78   Parser::addOperator(kind::BITVECTOR_SGT);
  79   Parser::addOperator(kind::BITVECTOR_SGE);
  80   Parser::addOperator(kind::BITVECTOR_BITOF);
  81   Parser::addOperator(kind::BITVECTOR_EXTRACT);
  82   Parser::addOperator(kind::BITVECTOR_REPEAT);
  83   Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND);
  84   Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND);
  85   Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT);
  86   Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT);
  87
  88   Parser::addOperator(kind::INT_TO_BITVECTOR);
  89   Parser::addOperator(kind::BITVECTOR_TO_NAT);
  90 }
  91
  92 void Smt2::addStringOperators() {
  93   Parser::addOperator(kind::STRING_CONCAT);
  94   Parser::addOperator(kind::STRING_LENGTH);
  95 }
  96
  97 void Smt2::addTheory(Theory theory) {
  98   switch(theory) {
  99   case THEORY_ARRAYS:
 100     Parser::addOperator(kind::SELECT);
 101     Parser::addOperator(kind::STORE);
 102     break;
 103
 104   case THEORY_BITVECTORS:
 105     addBitvectorOperators();
 106     break;
 107
 108   case THEORY_CORE:
 109     defineType("Bool", getExprManager()->booleanType());
 110     defineVar("true", getExprManager()->mkConst(true));
 111     defineVar("false", getExprManager()->mkConst(false));
 112     Parser::addOperator(kind::AND);
 113     Parser::addOperator(kind::DISTINCT);
 114     Parser::addOperator(kind::EQUAL);
 115     Parser::addOperator(kind::IFF);
 116     Parser::addOperator(kind::IMPLIES);
 117     Parser::addOperator(kind::ITE);
 118     Parser::addOperator(kind::NOT);
 119     Parser::addOperator(kind::OR);
 120     Parser::addOperator(kind::XOR);
 121     break;
 122
 123   case THEORY_REALS_INTS:
 124     defineType("Real", getExprManager()->realType());
 125     Parser::addOperator(kind::DIVISION);
 126     Parser::addOperator(kind::TO_INTEGER);
 127     Parser::addOperator(kind::IS_INTEGER);
 128     Parser::addOperator(kind::TO_REAL);
 129     // falling through on purpose, to add Ints part of Reals_Ints
 130   case THEORY_INTS:
 131     defineType("Int", getExprManager()->integerType());
 132     addArithmeticOperators();
 133     Parser::addOperator(kind::INTS_DIVISION);
 134     Parser::addOperator(kind::INTS_MODULUS);
 135     Parser::addOperator(kind::ABS);
 136     Parser::addOperator(kind::DIVISIBLE);
 137     break;
 138
 139   case THEORY_REALS:
 140     defineType("Real", getExprManager()->realType());
 141     addArithmeticOperators();
 142     Parser::addOperator(kind::DIVISION);
 143     break;
 144
 145   case THEORY_QUANTIFIERS:
 146     break;
 147
 148   case THEORY_SETS:
 149     addOperator(kind::UNION, "union");
 150     addOperator(kind::INTERSECTION, "intersection");
 151     addOperator(kind::SETMINUS, "setminus");
 152     addOperator(kind::SUBSET, "subseteq");
 153     addOperator(kind::MEMBER, "in");
 154     addOperator(kind::SET_SINGLETON, "setenum");
 155     break;
 156
 157   case THEORY_STRINGS:
 158     defineType("String", getExprManager()->stringType());
 159     addStringOperators();
 160     break;
 161
 162   case THEORY_UF:
 163     Parser::addOperator(kind::APPLY_UF);
 164     break;
 165
 166   default:
 167     std::stringstream ss;
 168     ss << "internal error: unsupported theory " << theory;
 169     throw ParserException(ss.str());
 170   }
 171 }
 172
 173 void Smt2::addOperator(Kind kind, const std::string& name) {
 174   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 175                   << std::endl;
 176   Parser::addOperator(kind);
 177   operatorKindMap[name] = kind;
 178 }
 179
 180 Kind Smt2::getOperatorKind(const std::string& name) const {
 181   // precondition: isOperatorEnabled(name)
 182   return operatorKindMap.find(name)->second;
 183 }
 184
 185 bool Smt2::isOperatorEnabled(const std::string& name) const {
 186   return operatorKindMap.find(name) != operatorKindMap.end();
 187 }
 188
 189 bool Smt2::isTheoryEnabled(Theory theory) const {
 190   switch(theory) {
 191   case THEORY_ARRAYS:
 192     return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
 193   case THEORY_BITVECTORS:
 194     return d_logic.isTheoryEnabled(theory::THEORY_BV);
 195   case THEORY_CORE:
 196     return true;
 197   case THEORY_INTS:
 198     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 199       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
 200   case THEORY_REALS:
 201     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 202       ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
 203   case THEORY_REALS_INTS:
 204     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 205       d_logic.areIntegersUsed() && d_logic.areRealsUsed();
 206   case THEORY_QUANTIFIERS:
 207     return d_logic.isQuantified();
 208   case THEORY_SETS:
 209     return d_logic.isTheoryEnabled(theory::THEORY_SETS);
 210   case THEORY_STRINGS:
 211     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
 212   case THEORY_UF:
 213     return d_logic.isTheoryEnabled(theory::THEORY_UF);
 214   default:
 215     std::stringstream ss;
 216     ss << "internal error: unsupported theory " << theory;
 217     throw ParserException(ss.str());
 218   }
 219 }
 220
 221 bool Smt2::logicIsSet() {
 222   return d_logicSet;
 223 }
 224
 225 void Smt2::setLogic(const std::string& name) {
 226   d_logicSet = true;
 227   d_logic = name;
 228
 229   // Core theory belongs to every logic
 230   addTheory(THEORY_CORE);
 231
 232   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 233     addTheory(THEORY_UF);
 234   }
 235
 236   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 237     if(d_logic.areIntegersUsed()) {
 238       if(d_logic.areRealsUsed()) {
 239         addTheory(THEORY_REALS_INTS);
 240       } else {
 241         addTheory(THEORY_INTS);
 242       }
 243     } else if(d_logic.areRealsUsed()) {
 244       addTheory(THEORY_REALS);
 245     }
 246   }
 247
 248   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
 249     addTheory(THEORY_ARRAYS);
 250   }
 251
 252   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 253     addTheory(THEORY_BITVECTORS);
 254   }
 255
 256   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 257     addTheory(THEORY_SETS);
 258   }
 259
 260   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 261     addTheory(THEORY_STRINGS);
 262   }
 263
 264   if(d_logic.isQuantified()) {
 265     addTheory(THEORY_QUANTIFIERS);
 266   }
 267 }/* Smt2::setLogic() */
 268
 269 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 270   // TODO: ???
 271 }
 272
 273 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 274   // TODO: ???
 275 }
 276
 277 void Smt2::checkThatLogicIsSet() {
 278   if( ! logicIsSet() ) {
 279     if( strictModeEnabled() ) {
 280       parseError("set-logic must appear before this point.");
 281     } else {
 282       warning("No set-logic command was given before this point.");
 283       warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
 284       warning("Consider setting a stricter logic for (likely) better performance.");
 285       warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 286
 287       setLogic("ALL_SUPPORTED");
 288
 289       Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
 290       c->setMuted(true);
 291       preemptCommand(c);
 292     }
 293   }
 294 }
 295
 296 /* The include are managed in the lexer but called in the parser */
 297 // Inspired by http://www.antlr3.org/api/C/interop.html
 298
 299 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 300   Debug("parser") << "Including " << filename << std::endl;
 301   // Create a new input stream and take advantage of built in stream stacking
 302   // in C target runtime.
 303   //
 304   pANTLR3_INPUT_STREAM    in;
 305 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 306   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 307 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 308   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 309 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 310   if( in == NULL ) {
 311     Debug("parser") << "Can't open " << filename << std::endl;
 312     return false;
 313   }
 314   // Same thing as the predefined PUSHSTREAM(in);
 315   lexer->pushCharStream(lexer, in);
 316   // restart it
 317   //lexer->rec->state->tokenStartCharIndex      = -10;
 318   //lexer->emit(lexer);
 319
 320   // Note that the input stream is not closed when it EOFs, I don't bother
 321   // to do it here, but it is up to you to track streams created like this
 322   // and destroy them when the whole parse session is complete. Remember that you
 323   // don't want to do this until all tokens have been manipulated all the way through
 324   // your tree parsers etc as the token does not store the text it just refers
 325   // back to the input stream and trying to get the text for it will abort if you
 326   // close the input stream too early.
 327
 328   //TODO what said before
 329   return true;
 330 }
 331
 332 void Smt2::includeFile(const std::string& filename) {
 333   // security for online version
 334   if(!canIncludeFile()) {
 335     parseError("include-file feature was disabled for this run.");
 336   }
 337
 338   // Get the lexer
 339   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 340   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 341   // get the name of the current stream "Does it work inside an include?"
 342   const std::string inputName = ai->getInputStreamName();
 343
 344   // Find the directory of the current input file
 345   std::string path;
 346   size_t pos = inputName.rfind('/');
 347   if(pos != std::string::npos) {
 348     path = std::string(inputName, 0, pos + 1);
 349   }
 350   path.append(filename);
 351   if(!newInputStream(path, lexer)) {
 352     parseError("Couldn't open include file `" + path + "'");
 353   }
 354 }
 355
 356 }/* CVC4::parser namespace */
 357 }/* CVC4 namespace */