src/parser/smt/smt.cpp

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