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