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_DATATYPES:
 158     Parser::addOperator(kind::APPLY_CONSTRUCTOR);
 159     Parser::addOperator(kind::APPLY_TESTER);
 160     Parser::addOperator(kind::APPLY_SELECTOR);
 161     break;
 162
 163   case THEORY_STRINGS:
 164     defineType("String", getExprManager()->stringType());
 165     addStringOperators();
 166     break;
 167
 168   case THEORY_UF:
 169     Parser::addOperator(kind::APPLY_UF);
 170     break;
 171
 172   default:
 173     std::stringstream ss;
 174     ss << "internal error: unsupported theory " << theory;
 175     throw ParserException(ss.str());
 176   }
 177 }
 178
 179 void Smt2::addOperator(Kind kind, const std::string& name) {
 180   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
 181                   << std::endl;
 182   Parser::addOperator(kind);
 183   operatorKindMap[name] = kind;
 184 }
 185
 186 Kind Smt2::getOperatorKind(const std::string& name) const {
 187   // precondition: isOperatorEnabled(name)
 188   return operatorKindMap.find(name)->second;
 189 }
 190
 191 bool Smt2::isOperatorEnabled(const std::string& name) const {
 192   return operatorKindMap.find(name) != operatorKindMap.end();
 193 }
 194
 195 bool Smt2::isTheoryEnabled(Theory theory) const {
 196   switch(theory) {
 197   case THEORY_ARRAYS:
 198     return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
 199   case THEORY_BITVECTORS:
 200     return d_logic.isTheoryEnabled(theory::THEORY_BV);
 201   case THEORY_CORE:
 202     return true;
 203   case THEORY_DATATYPES:
 204     return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
 205   case THEORY_INTS:
 206     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 207       d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
 208   case THEORY_REALS:
 209     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 210       ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
 211   case THEORY_REALS_INTS:
 212     return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
 213       d_logic.areIntegersUsed() && d_logic.areRealsUsed();
 214   case THEORY_QUANTIFIERS:
 215     return d_logic.isQuantified();
 216   case THEORY_SETS:
 217     return d_logic.isTheoryEnabled(theory::THEORY_SETS);
 218   case THEORY_STRINGS:
 219     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
 220   case THEORY_UF:
 221     return d_logic.isTheoryEnabled(theory::THEORY_UF);
 222   default:
 223     std::stringstream ss;
 224     ss << "internal error: unsupported theory " << theory;
 225     throw ParserException(ss.str());
 226   }
 227 }
 228
 229 bool Smt2::logicIsSet() {
 230   return d_logicSet;
 231 }
 232
 233 void Smt2::setLogic(const std::string& name) {
 234   d_logicSet = true;
 235   d_logic = name;
 236
 237   // Core theory belongs to every logic
 238   addTheory(THEORY_CORE);
 239
 240   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 241     addTheory(THEORY_UF);
 242   }
 243
 244   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 245     if(d_logic.areIntegersUsed()) {
 246       if(d_logic.areRealsUsed()) {
 247         addTheory(THEORY_REALS_INTS);
 248       } else {
 249         addTheory(THEORY_INTS);
 250       }
 251     } else if(d_logic.areRealsUsed()) {
 252       addTheory(THEORY_REALS);
 253     }
 254   }
 255
 256   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
 257     addTheory(THEORY_ARRAYS);
 258   }
 259
 260   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 261     addTheory(THEORY_BITVECTORS);
 262   }
 263
 264   if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
 265     addTheory(THEORY_DATATYPES);
 266   }
 267
 268   if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
 269     addTheory(THEORY_SETS);
 270   }
 271
 272   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
 273     addTheory(THEORY_STRINGS);
 274   }
 275
 276   if(d_logic.isQuantified()) {
 277     addTheory(THEORY_QUANTIFIERS);
 278   }
 279 }/* Smt2::setLogic() */
 280
 281 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 282   // TODO: ???
 283 }
 284
 285 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 286   // TODO: ???
 287 }
 288
 289 void Smt2::checkThatLogicIsSet() {
 290   if( ! logicIsSet() ) {
 291     if( strictModeEnabled() ) {
 292       parseError("set-logic must appear before this point.");
 293     } else {
 294       warning("No set-logic command was given before this point.");
 295       warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
 296       warning("Consider setting a stricter logic for (likely) better performance.");
 297       warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 298
 299       setLogic("ALL_SUPPORTED");
 300
 301       Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
 302       c->setMuted(true);
 303       preemptCommand(c);
 304     }
 305   }
 306 }
 307
 308 /* The include are managed in the lexer but called in the parser */
 309 // Inspired by http://www.antlr3.org/api/C/interop.html
 310
 311 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 312   Debug("parser") << "Including " << filename << std::endl;
 313   // Create a new input stream and take advantage of built in stream stacking
 314   // in C target runtime.
 315   //
 316   pANTLR3_INPUT_STREAM    in;
 317 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 318   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 319 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 320   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 321 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 322   if( in == NULL ) {
 323     Debug("parser") << "Can't open " << filename << std::endl;
 324     return false;
 325   }
 326   // Same thing as the predefined PUSHSTREAM(in);
 327   lexer->pushCharStream(lexer, in);
 328   // restart it
 329   //lexer->rec->state->tokenStartCharIndex      = -10;
 330   //lexer->emit(lexer);
 331
 332   // Note that the input stream is not closed when it EOFs, I don't bother
 333   // to do it here, but it is up to you to track streams created like this
 334   // and destroy them when the whole parse session is complete. Remember that you
 335   // don't want to do this until all tokens have been manipulated all the way through
 336   // your tree parsers etc as the token does not store the text it just refers
 337   // back to the input stream and trying to get the text for it will abort if you
 338   // close the input stream too early.
 339
 340   //TODO what said before
 341   return true;
 342 }
 343
 344 void Smt2::includeFile(const std::string& filename) {
 345   // security for online version
 346   if(!canIncludeFile()) {
 347     parseError("include-file feature was disabled for this run.");
 348   }
 349
 350   // Get the lexer
 351   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 352   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 353   // get the name of the current stream "Does it work inside an include?"
 354   const std::string inputName = ai->getInputStreamName();
 355
 356   // Find the directory of the current input file
 357   std::string path;
 358   size_t pos = inputName.rfind('/');
 359   if(pos != std::string::npos) {
 360     path = std::string(inputName, 0, pos + 1);
 361   }
 362   path.append(filename);
 363   if(!newInputStream(path, lexer)) {
 364     parseError("Couldn't open include file `" + path + "'");
 365   }
 366 }
 367
 368 }/* CVC4::parser namespace */
 369 }/* CVC4 namespace */