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_NRA"] = QF_NRA;
  39   logicMap["QF_RDL"] = QF_RDL;
  40   logicMap["QF_SAT"] = QF_SAT;
  41   logicMap["QF_UF"] = QF_UF;
  42   logicMap["QF_UFIDL"] = QF_UFIDL;
  43   logicMap["QF_UFBV"] = QF_UFBV;
  44   logicMap["QF_UFLRA"] = QF_UFLRA;
  45   logicMap["QF_UFLIA"] = QF_UFLIA;
  46   logicMap["QF_UFLIRA"] = QF_UFLIRA;
  47   logicMap["QF_UFNIA"] = QF_UFNIA;
  48   logicMap["QF_UFNIRA"] = QF_UFNIRA;
  49   logicMap["QF_UFNRA"] = QF_UFNRA;
  50   logicMap["QF_ABV"] = QF_ABV;
  51   logicMap["QF_AUFBV"] = QF_AUFBV;
  52   logicMap["QF_AUFBVLIA"] = QF_AUFBVLIA;
  53   logicMap["QF_AUFBVLRA"] = QF_AUFBVLRA;
  54   logicMap["QF_UFNIRA"] = QF_UFNIRA;
  55   logicMap["QF_AUFLIA"] = QF_AUFLIA;
  56   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
  57   logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED;
  58   logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
  59   return logicMap;
  60 }
  61
  62 Smt::Logic Smt::toLogic(const std::string& name) {
  63   static std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap = newLogicMap();
  64   return logicMap[name];
  65 }
  66
  67 Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
  68   Parser(exprManager,input,strictMode,parseOnly),
  69   d_logicSet(false) {
  70
  71   // Boolean symbols are always defined
  72   addOperator(kind::AND);
  73   addOperator(kind::EQUAL);
  74   addOperator(kind::IFF);
  75   addOperator(kind::IMPLIES);
  76   addOperator(kind::ITE);
  77   addOperator(kind::NOT);
  78   addOperator(kind::OR);
  79   addOperator(kind::XOR);
  80
  81 }
  82
  83 void Smt::addArithmeticOperators() {
  84   addOperator(kind::PLUS);
  85   addOperator(kind::MINUS);
  86   addOperator(kind::UMINUS);
  87   addOperator(kind::MULT);
  88   addOperator(kind::LT);
  89   addOperator(kind::LEQ);
  90   addOperator(kind::GT);
  91   addOperator(kind::GEQ);
  92 }
  93
  94 void Smt::addTheory(Theory theory) {
  95   switch(theory) {
  96   case THEORY_ARRAYS:
  97   case THEORY_ARRAYS_EX: {
  98     Type indexType = mkSort("Index");
  99     Type elementType = mkSort("Element");
 100     DeclarationSequence* seq = new DeclarationSequence();
 101     seq->addCommand(new DeclareTypeCommand("Index", 0, indexType));
 102     seq->addCommand(new DeclareTypeCommand("Element", 0, elementType));
 103     preemptCommand(seq);
 104
 105     defineType("Array", getExprManager()->mkArrayType(indexType, elementType));
 106
 107     addOperator(kind::SELECT);
 108     addOperator(kind::STORE);
 109     break;
 110   }
 111
 112   case THEORY_INT_ARRAYS_EX: {
 113     defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
 114
 115     addOperator(kind::SELECT);
 116     addOperator(kind::STORE);
 117     break;
 118   }
 119
 120   case THEORY_EMPTY: {
 121     Type sort = mkSort("U");
 122     preemptCommand(new DeclareTypeCommand("U", 0, sort));
 123     break;
 124   }
 125
 126   case THEORY_REALS_INTS:
 127     defineType("Real", getExprManager()->realType());
 128     // falling-through on purpose, to add Ints part of RealsInts
 129
 130   case THEORY_INTS:
 131     defineType("Int", getExprManager()->integerType());
 132     addArithmeticOperators();
 133     break;
 134
 135   case THEORY_REALS:
 136     defineType("Real", getExprManager()->realType());
 137     addArithmeticOperators();
 138     break;
 139
 140   case THEORY_BITVECTORS:
 141     break;
 142
 143   default:
 144     Unhandled(theory);
 145   }
 146 }
 147
 148 bool Smt::logicIsSet() {
 149   return d_logicSet;
 150 }
 151
 152 inline void Smt::addUf() {
 153   addTheory(Smt::THEORY_EMPTY);
 154   addOperator(kind::APPLY_UF);
 155 }
 156
 157 void Smt::setLogic(const std::string& name) {
 158   d_logicSet = true;
 159   d_logic = toLogic(name);
 160
 161   switch(d_logic) {
 162   case QF_AX:
 163     addTheory(THEORY_ARRAYS_EX);
 164     break;
 165
 166   case QF_IDL:
 167   case QF_LIA:
 168   case QF_NIA:
 169     addTheory(THEORY_INTS);
 170     break;
 171
 172   case QF_RDL:
 173   case QF_LRA:
 174   case QF_NRA:
 175     addTheory(THEORY_REALS);
 176     break;
 177
 178   case QF_SAT:
 179     /* no extra symbols needed */
 180     break;
 181
 182   case QF_UFIDL:
 183   case QF_UFLIA:
 184   case QF_UFNIA:// nonstandard logic
 185     addTheory(THEORY_INTS);
 186     addUf();
 187     break;
 188
 189   case QF_UFLRA:
 190   case QF_UFNRA:
 191     addTheory(THEORY_REALS);
 192     addUf();
 193     break;
 194
 195   case QF_UFLIRA:// nonstandard logic
 196   case QF_UFNIRA:// nonstandard logic
 197     addTheory(THEORY_INTS);
 198     addTheory(THEORY_REALS);
 199     addUf();
 200     break;
 201
 202   case QF_UF:
 203     addUf();
 204     break;
 205
 206   case QF_BV:
 207     addTheory(THEORY_BITVECTORS);
 208     break;
 209
 210   case QF_ABV:
 211     addTheory(THEORY_ARRAYS_EX);
 212     addTheory(THEORY_BITVECTORS);
 213     break;
 214
 215   case QF_UFBV:
 216     addUf();
 217     addTheory(THEORY_BITVECTORS);
 218     break;
 219
 220   case QF_AUFBV:
 221     addUf();
 222     addTheory(THEORY_ARRAYS_EX);
 223     addTheory(THEORY_BITVECTORS);
 224     break;
 225
 226   case QF_AUFBVLIA:
 227     addUf();
 228     addTheory(THEORY_ARRAYS_EX);
 229     addTheory(THEORY_BITVECTORS);
 230     addTheory(THEORY_INTS);
 231     break;
 232
 233   case QF_AUFBVLRA:
 234     addUf();
 235     addTheory(THEORY_ARRAYS_EX);
 236     addTheory(THEORY_BITVECTORS);
 237     addTheory(THEORY_REALS);
 238     break;
 239
 240   case QF_AUFLIA:
 241     addTheory(THEORY_INT_ARRAYS_EX);
 242     addUf();
 243     addTheory(THEORY_INTS);
 244     break;
 245
 246   case QF_AUFLIRA:
 247     addTheory(THEORY_ARRAYS_EX);
 248     addUf();
 249     addTheory(THEORY_INTS);
 250     addTheory(THEORY_REALS);
 251     break;
 252
 253   case ALL_SUPPORTED:
 254     /* fall through */
 255   case QF_ALL_SUPPORTED:
 256     addTheory(THEORY_ARRAYS_EX);
 257     addUf();
 258     addTheory(THEORY_INTS);
 259     addTheory(THEORY_REALS);
 260     addTheory(THEORY_BITVECTORS);
 261     break;
 262
 263   case AUFLIA:
 264   case AUFLIRA:
 265   case AUFNIRA:
 266   case LRA:
 267   case UFLRA:
 268   case UFNIA:
 269     Unhandled(name);
 270   }
 271 }
 272
 273 }/* CVC4::parser namespace */
 274 }/* CVC4 namespace */