src/parser/smt/smt.cpp

   1 /*********************                                                        */
   2 /*! \file smt.cpp
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): mdeters, dejan
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  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  ** Definitions of SMT constants.
  15  **/
  16
  17 #include <ext/hash_map>
  18 namespace std {
  19 using namespace __gnu_cxx;
  20 }
  21
  22 #include "parser/parser.h"
  23 #include "parser/smt/smt.h"
  24
  25 namespace CVC4 {
  26 namespace parser {
  27
  28 std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newLogicMap() {
  29   std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap;
  30   logicMap["QF_AX"] = QF_AX;
  31   logicMap["QF_BV"] = QF_BV;
  32   logicMap["QF_IDL"] = QF_IDL;
  33   logicMap["QF_LIA"] = QF_LIA;
  34   logicMap["QF_LRA"] = QF_LRA;
  35   logicMap["QF_NIA"] = QF_NIA;
  36   logicMap["QF_RDL"] = QF_RDL;
  37   logicMap["QF_SAT"] = QF_SAT;
  38   logicMap["QF_UF"] = QF_UF;
  39   logicMap["QF_UFIDL"] = QF_UFIDL;
  40   return logicMap;
  41 }
  42
  43 Smt::Logic Smt::toLogic(const std::string& name) {
  44   static std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap = newLogicMap();
  45   return logicMap[name];
  46 }
  47
  48 Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode) :
  49   Parser(exprManager,input,strictMode),
  50   d_logicSet(false) {
  51
  52   // Boolean symbols are always defined
  53   addOperator(kind::AND);
  54   addOperator(kind::EQUAL);
  55   addOperator(kind::IFF);
  56   addOperator(kind::IMPLIES);
  57   addOperator(kind::ITE);
  58   addOperator(kind::NOT);
  59   addOperator(kind::OR);
  60   addOperator(kind::XOR);
  61
  62 }
  63
  64 void Smt::addArithmeticOperators() {
  65   addOperator(kind::PLUS);
  66   addOperator(kind::MINUS);
  67   addOperator(kind::UMINUS);
  68   addOperator(kind::MULT);
  69   addOperator(kind::LT);
  70   addOperator(kind::LEQ);
  71   addOperator(kind::GT);
  72   addOperator(kind::GEQ);
  73 }
  74
  75 /**
  76  * Add theory symbols to the parser state.
  77  *
  78  * @param parser the CVC4 Parser object
  79  * @param theory the theory to open (e.g., Core, Ints)
  80  */
  81 void Smt::addTheory(Theory theory) {
  82   switch(theory) {
  83   case THEORY_ARRAYS:
  84   case THEORY_ARRAYS_EX: {
  85     Type indexType = mkSort("Index");
  86     Type elementType = mkSort("Element");
  87
  88     defineType("Array",getExprManager()->mkArrayType(indexType,elementType));
  89
  90     addOperator(kind::SELECT);
  91     addOperator(kind::STORE);
  92     break;
  93   }
  94
  95   case THEORY_EMPTY:
  96     mkSort("U");
  97     break;
  98
  99   case THEORY_REALS_INTS:
 100     defineType("Real", getExprManager()->realType());
 101     // falling-through on purpose, to add Ints part of RealsInts
 102
 103   case THEORY_INTS:
 104     defineType("Int", getExprManager()->integerType());
 105     addArithmeticOperators();
 106     break;
 107
 108   case THEORY_REALS:
 109     defineType("Real", getExprManager()->realType());
 110     addArithmeticOperators();
 111     break;
 112
 113   case THEORY_BITVECTORS:
 114     break;
 115
 116   default:
 117     Unhandled(theory);
 118   }
 119 }
 120
 121 bool Smt::logicIsSet() {
 122   return d_logicSet;
 123 }
 124
 125 inline void Smt::addUf() {
 126   addTheory(Smt::THEORY_EMPTY);
 127   addOperator(kind::APPLY_UF);
 128 }
 129
 130 /**
 131  * Sets the logic for the current benchmark. Declares any logic and theory symbols.
 132  *
 133  * @param parser the CVC4 Parser object
 134  * @param name the name of the logic (e.g., QF_UF, AUFLIA)
 135  */
 136 void Smt::setLogic(const std::string& name) {
 137   d_logicSet = true;
 138   d_logic = toLogic(name);
 139
 140   switch(d_logic) {
 141   case QF_AX:
 142     addTheory(THEORY_ARRAYS_EX);
 143     break;
 144
 145   case QF_IDL:
 146   case QF_LIA:
 147   case QF_NIA:
 148     addTheory(THEORY_INTS);
 149     break;
 150
 151   case QF_LRA:
 152   case QF_RDL:
 153     addTheory(THEORY_REALS);
 154     break;
 155
 156   case QF_SAT:
 157     /* no extra symbols needed */
 158     break;
 159
 160   case QF_UFIDL:
 161   case QF_UFLIA:
 162     addTheory(THEORY_INTS);
 163     addUf();
 164     break;
 165
 166   case QF_UFLRA:
 167   case QF_UFNRA:
 168     addTheory(THEORY_REALS);
 169     addUf();
 170     break;
 171
 172   case QF_UF:
 173     addUf();
 174     break;
 175
 176   case QF_BV:
 177     addTheory(THEORY_BITVECTORS);
 178     break;
 179
 180   case AUFLIA:
 181   case AUFLIRA:
 182   case AUFNIRA:
 183   case LRA:
 184   case UFNIA:
 185   case QF_AUFBV:
 186   case QF_AUFLIA:
 187     Unhandled(name);
 188   }
 189 }
 190
 191 }/* CVC4::parser namespace */
 192 }/* CVC4 namespace */