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