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     // falling through on purpose, to add Ints part of Reals_Ints
 115
 116   case THEORY_INTS:
 117     defineType("Int", getExprManager()->integerType());
 118     addArithmeticOperators();
 119     addOperator(kind::INTS_DIVISION);
 120     addOperator(kind::INTS_MODULUS);
 121     break;
 122
 123   case THEORY_REALS:
 124     defineType("Real", getExprManager()->realType());
 125     addArithmeticOperators();
 126     addOperator(kind::DIVISION);
 127     break;
 128
 129   case THEORY_BITVECTORS:
 130     addBitvectorOperators();
 131     break;
 132
 133   case THEORY_QUANTIFIERS:
 134     break;
 135
 136   default:
 137     std::stringstream ss;
 138     ss << "internal error: unsupported theory " << theory;
 139     throw ParserException(ss.str());
 140   }
 141 }
 142
 143 bool Smt2::logicIsSet() {
 144   return d_logicSet;
 145 }
 146
 147 void Smt2::setLogic(const std::string& name) {
 148   d_logicSet = true;
 149   d_logic = name;
 150
 151   // Core theory belongs to every logic
 152   addTheory(THEORY_CORE);
 153
 154   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
 155     addOperator(kind::APPLY_UF);
 156   }
 157
 158   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
 159     if(d_logic.areIntegersUsed()) {
 160       addTheory(THEORY_INTS);
 161     }
 162
 163     if(d_logic.areRealsUsed()) {
 164       addTheory(THEORY_REALS);
 165     }
 166   }
 167
 168   if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
 169     addTheory(THEORY_ARRAYS);
 170   }
 171
 172   if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
 173     addTheory(THEORY_BITVECTORS);
 174   }
 175
 176   if(d_logic.isQuantified()) {
 177     addTheory(THEORY_QUANTIFIERS);
 178   }
 179 }/* Smt2::setLogic() */
 180
 181 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 182   // TODO: ???
 183 }
 184
 185 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 186   // TODO: ???
 187 }
 188
 189 void Smt2::checkThatLogicIsSet() {
 190   if( ! logicIsSet() ) {
 191     if( strictModeEnabled() ) {
 192       parseError("set-logic must appear before this point.");
 193     } else {
 194       warning("No set-logic command was given before this point.");
 195       warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
 196       warning("Consider setting a stricter logic for (likely) better performance.");
 197       warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 198
 199       setLogic("ALL_SUPPORTED");
 200
 201       Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
 202       c->setMuted(true);
 203       preemptCommand(c);
 204     }
 205   }
 206 }
 207
 208 /* The include are managed in the lexer but called in the parser */
 209 // Inspired by http://www.antlr3.org/api/C/interop.html
 210
 211 static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 212   Debug("parser") << "Including " << filename << std::endl;
 213   // Create a new input stream and take advantage of built in stream stacking
 214   // in C target runtime.
 215   //
 216   pANTLR3_INPUT_STREAM    in;
 217 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
 218   in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
 219 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 220   in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
 221 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
 222   if( in == NULL ) {
 223     Debug("parser") << "Can't open " << filename << std::endl;
 224     return false;
 225   }
 226   // Same thing as the predefined PUSHSTREAM(in);
 227   lexer->pushCharStream(lexer, in);
 228   // restart it
 229   //lexer->rec->state->tokenStartCharIndex      = -10;
 230   //lexer->emit(lexer);
 231
 232   // Note that the input stream is not closed when it EOFs, I don't bother
 233   // to do it here, but it is up to you to track streams created like this
 234   // and destroy them when the whole parse session is complete. Remember that you
 235   // don't want to do this until all tokens have been manipulated all the way through
 236   // your tree parsers etc as the token does not store the text it just refers
 237   // back to the input stream and trying to get the text for it will abort if you
 238   // close the input stream too early.
 239
 240   //TODO what said before
 241   return true;
 242 }
 243
 244 void Smt2::includeFile(const std::string& filename) {
 245   // security for online version
 246   if(!canIncludeFile()) {
 247     parseError("include-file feature was disabled for this run.");
 248   }
 249
 250   // Get the lexer
 251   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
 252   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
 253   // get the name of the current stream "Does it work inside an include?"
 254   const std::string inputName = ai->getInputStreamName();
 255
 256   // Find the directory of the current input file
 257   std::string path;
 258   size_t pos = inputName.rfind('/');
 259   if(pos != std::string::npos) {
 260     path = std::string(inputName, 0, pos + 1);
 261   }
 262   path.append(filename);
 263   if(!newInputStream(path, lexer)) {
 264     parseError("Couldn't open include file `" + path + "'");
 265   }
 266 }
 267
 268 }/* CVC4::parser namespace */
 269 }/* CVC4 namespace */