src/parser/smt2/smt2.cpp

   1 /*********************                                                        */
   2 /*! \file smt2.cpp
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Definitions of SMT2 constants.
  15  **
  16  ** Definitions of SMT2 constants.
  17  **/
  18
  19 #include "expr/type.h"
  20 #include "expr/command.h"
  21 #include "parser/parser.h"
  22 #include "parser/smt1/smt1.h"
  23 #include "parser/smt2/smt2.h"
  24
  25 namespace CVC4 {
  26 namespace parser {
  27
  28 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
  29   Parser(exprManager,input,strictMode,parseOnly),
  30   d_logicSet(false) {
  31   if( !strictModeEnabled() ) {
  32     addTheory(Smt2::THEORY_CORE);
  33   }
  34 }
  35
  36 void Smt2::addArithmeticOperators() {
  37   addOperator(kind::PLUS);
  38   addOperator(kind::MINUS);
  39   addOperator(kind::UMINUS);
  40   addOperator(kind::MULT);
  41   addOperator(kind::DIVISION);
  42   addOperator(kind::LT);
  43   addOperator(kind::LEQ);
  44   addOperator(kind::GT);
  45   addOperator(kind::GEQ);
  46 }
  47
  48 void Smt2::addBitvectorOperators() {
  49   addOperator(kind::BITVECTOR_CONCAT);
  50   addOperator(kind::BITVECTOR_AND);
  51   addOperator(kind::BITVECTOR_OR);
  52   addOperator(kind::BITVECTOR_XOR);
  53   addOperator(kind::BITVECTOR_NOT);
  54   addOperator(kind::BITVECTOR_NAND);
  55   addOperator(kind::BITVECTOR_NOR);
  56   addOperator(kind::BITVECTOR_XNOR);
  57   addOperator(kind::BITVECTOR_COMP);
  58   addOperator(kind::BITVECTOR_MULT);
  59   addOperator(kind::BITVECTOR_PLUS);
  60   addOperator(kind::BITVECTOR_SUB);
  61   addOperator(kind::BITVECTOR_NEG);
  62   addOperator(kind::BITVECTOR_UDIV);
  63   addOperator(kind::BITVECTOR_UREM);
  64   addOperator(kind::BITVECTOR_SDIV);
  65   addOperator(kind::BITVECTOR_SREM);
  66   addOperator(kind::BITVECTOR_SMOD);
  67   addOperator(kind::BITVECTOR_SHL);
  68   addOperator(kind::BITVECTOR_LSHR);
  69   addOperator(kind::BITVECTOR_ASHR);
  70   addOperator(kind::BITVECTOR_ULT);
  71   addOperator(kind::BITVECTOR_ULE);
  72   addOperator(kind::BITVECTOR_UGT);
  73   addOperator(kind::BITVECTOR_UGE);
  74   addOperator(kind::BITVECTOR_SLT);
  75   addOperator(kind::BITVECTOR_SLE);
  76   addOperator(kind::BITVECTOR_SGT);
  77   addOperator(kind::BITVECTOR_SGE);
  78   addOperator(kind::BITVECTOR_BITOF);
  79   addOperator(kind::BITVECTOR_EXTRACT);
  80   addOperator(kind::BITVECTOR_REPEAT);
  81   addOperator(kind::BITVECTOR_ZERO_EXTEND);
  82   addOperator(kind::BITVECTOR_SIGN_EXTEND);
  83   addOperator(kind::BITVECTOR_ROTATE_LEFT);
  84   addOperator(kind::BITVECTOR_ROTATE_RIGHT);
  85 }
  86
  87 void Smt2::addTheory(Theory theory) {
  88   switch(theory) {
  89   case THEORY_CORE:
  90     defineType("Bool", getExprManager()->booleanType());
  91     defineVar("true", getExprManager()->mkConst(true));
  92     defineVar("false", getExprManager()->mkConst(false));
  93     addOperator(kind::AND);
  94     addOperator(kind::DISTINCT);
  95     addOperator(kind::EQUAL);
  96     addOperator(kind::IFF);
  97     addOperator(kind::IMPLIES);
  98     addOperator(kind::ITE);
  99     addOperator(kind::NOT);
 100     addOperator(kind::OR);
 101     addOperator(kind::XOR);
 102     break;
 103
 104   case THEORY_ARRAYS:
 105     addOperator(kind::SELECT);
 106     addOperator(kind::STORE);
 107     break;
 108
 109   case THEORY_REALS_INTS:
 110     defineType("Real", getExprManager()->realType());
 111     // falling-through on purpose, to add Ints part of RealsInts
 112
 113   case THEORY_INTS:
 114     defineType("Int", getExprManager()->integerType());
 115     addArithmeticOperators();
 116     break;
 117
 118   case THEORY_REALS:
 119     defineType("Real", getExprManager()->realType());
 120     addArithmeticOperators();
 121     break;
 122
 123   case THEORY_BITVECTORS:
 124     addBitvectorOperators();
 125     break;
 126
 127   case THEORY_QUANTIFIERS:
 128     break;
 129
 130   default:
 131     std::stringstream ss;
 132     ss << "internal error: unsupported theory " << theory;
 133     throw ParserException(ss.str());
 134   }
 135 }
 136
 137 bool Smt2::logicIsSet() {
 138   return d_logicSet;
 139 }
 140
 141 void Smt2::setLogic(const std::string& name) {
 142   d_logicSet = true;
 143   d_logic = Smt1::toLogic(name);
 144
 145   // Core theory belongs to every logic
 146   addTheory(THEORY_CORE);
 147
 148   switch(d_logic) {
 149   case Smt1::QF_SAT:
 150     /* No extra symbols necessary */
 151     break;
 152
 153   case Smt1::QF_AX:
 154     addTheory(THEORY_ARRAYS);
 155     break;
 156
 157   case Smt1::QF_IDL:
 158   case Smt1::QF_LIA:
 159   case Smt1::QF_NIA:
 160     addTheory(THEORY_INTS);
 161     break;
 162
 163   case Smt1::QF_RDL:
 164   case Smt1::QF_LRA:
 165   case Smt1::QF_NRA:
 166     addTheory(THEORY_REALS);
 167     break;
 168
 169   case Smt1::QF_UF:
 170     addOperator(kind::APPLY_UF);
 171     break;
 172
 173   case Smt1::QF_UFIDL:
 174   case Smt1::QF_UFLIA:
 175   case Smt1::QF_UFNIA:// nonstandard logic
 176     addTheory(THEORY_INTS);
 177     addOperator(kind::APPLY_UF);
 178     break;
 179
 180   case Smt1::QF_UFLRA:
 181   case Smt1::QF_UFNRA:
 182     addTheory(THEORY_REALS);
 183     addOperator(kind::APPLY_UF);
 184     break;
 185
 186   case Smt1::QF_UFLIRA:// nonstandard logic
 187   case Smt1::QF_UFNIRA:// nonstandard logic
 188     addOperator(kind::APPLY_UF);
 189     addTheory(THEORY_INTS);
 190     addTheory(THEORY_REALS);
 191     break;
 192
 193   case Smt1::QF_BV:
 194     addTheory(THEORY_BITVECTORS);
 195     break;
 196
 197   case Smt1::QF_ABV:
 198     addTheory(THEORY_ARRAYS);
 199     addTheory(THEORY_BITVECTORS);
 200     break;
 201
 202   case Smt1::QF_UFBV:
 203     addOperator(kind::APPLY_UF);
 204     addTheory(THEORY_BITVECTORS);
 205     break;
 206
 207   case Smt1::QF_AUFBV:
 208     addOperator(kind::APPLY_UF);
 209     addTheory(THEORY_ARRAYS);
 210     addTheory(THEORY_BITVECTORS);
 211     break;
 212
 213   case Smt1::QF_AUFBVLIA:
 214     addOperator(kind::APPLY_UF);
 215     addTheory(THEORY_ARRAYS);
 216     addTheory(THEORY_BITVECTORS);
 217     addTheory(THEORY_INTS);
 218     break;
 219
 220   case Smt1::QF_AUFBVLRA:
 221     addOperator(kind::APPLY_UF);
 222     addTheory(THEORY_ARRAYS);
 223     addTheory(THEORY_BITVECTORS);
 224     addTheory(THEORY_REALS);
 225     break;
 226
 227   case Smt1::QF_AUFLIA:
 228     addTheory(THEORY_ARRAYS);
 229     addOperator(kind::APPLY_UF);
 230     addTheory(THEORY_INTS);
 231     break;
 232
 233   case Smt1::QF_AUFLIRA:
 234     addTheory(THEORY_ARRAYS);
 235     addOperator(kind::APPLY_UF);
 236     addTheory(THEORY_INTS);
 237     addTheory(THEORY_REALS);
 238     break;
 239
 240   case Smt1::ALL_SUPPORTED:
 241     addTheory(THEORY_QUANTIFIERS);
 242     /* fall through */
 243   case Smt1::QF_ALL_SUPPORTED:
 244     addTheory(THEORY_ARRAYS);
 245     addOperator(kind::APPLY_UF);
 246     addTheory(THEORY_INTS);
 247     addTheory(THEORY_REALS);
 248     addTheory(THEORY_BITVECTORS);
 249     break;
 250
 251   case Smt1::AUFLIA:
 252   case Smt1::AUFLIRA:
 253   case Smt1::AUFNIRA:
 254   case Smt1::LRA:
 255   case Smt1::UFNIA:
 256   case Smt1::UFNIRA:
 257   case Smt1::UFLRA:
 258     if(d_logic != Smt1::AUFLIA && d_logic != Smt1::UFNIA) {
 259       addTheory(THEORY_REALS);
 260     }
 261     if(d_logic != Smt1::LRA) {
 262       addOperator(kind::APPLY_UF);
 263       if(d_logic != Smt1::UFLRA) {
 264         addTheory(THEORY_INTS);
 265         if(d_logic != Smt1::UFNIA && d_logic != Smt1::UFNIRA) {
 266           addTheory(THEORY_ARRAYS);
 267         }
 268       }
 269     }
 270     addTheory(THEORY_QUANTIFIERS);
 271     break;
 272   }
 273 }/* Smt2::setLogic() */
 274
 275 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 276   // TODO: ???
 277 }
 278
 279 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 280   // TODO: ???
 281 }
 282
 283 void Smt2::checkThatLogicIsSet() {
 284   if( ! logicIsSet() ) {
 285     if( strictModeEnabled() ) {
 286       parseError("set-logic must appear before this point.");
 287     } else {
 288       warning("No set-logic command was given before this point.");
 289       warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
 290       warning("Consider setting a stricter logic for (likely) better performance.");
 291       warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 292
 293       setLogic("ALL_SUPPORTED");
 294
 295       preemptCommand(new SetBenchmarkLogicCommand("ALL_SUPPORTED"));
 296     }
 297   }
 298 }
 299
 300 }/* CVC4::parser namespace */
 301 }/* CVC4 namespace */