src/parser/smt2/smt2.cpp

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