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