src/parser/smt/smt.cpp

   1 /*********************                                                        */
   2 /** smt.h
   3  ** Original author: cconway
   4  ** Major contributors:
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** Definitions of SMT constants.
  14  **/
  15
  16 #include <ext/hash_map>
  17 namespace std {
  18 using namespace __gnu_cxx;
  19 }
  20
  21 #include "parser/parser.h"
  22 #include "parser/smt/smt.h"
  23
  24 namespace CVC4 {
  25 namespace parser {
  26
  27 std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newLogicMap() {
  28   std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap;
  29   logicMap["QF_AX"] = QF_AX;
  30   logicMap["QF_BV"] = QF_BV;
  31   logicMap["QF_IDL"] = QF_IDL;
  32   logicMap["QF_LIA"] = QF_LIA;
  33   logicMap["QF_LRA"] = QF_LRA;
  34   logicMap["QF_NIA"] = QF_NIA;
  35   logicMap["QF_RDL"] = QF_RDL;
  36   logicMap["QF_SAT"] = QF_SAT;
  37   logicMap["QF_UF"] = QF_UF;
  38   logicMap["QF_UFIDL"] = QF_UFIDL;
  39   return logicMap;
  40 }
  41
  42 Smt::Logic Smt::toLogic(const std::string& name) {
  43   static std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap = newLogicMap();
  44   return logicMap[name];
  45 }
  46
  47 Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode) :
  48   Parser(exprManager,input,strictMode),
  49   d_logicSet(false) {
  50
  51   // Boolean symbols are always defined
  52   addOperator(kind::AND);
  53   addOperator(kind::EQUAL);
  54   addOperator(kind::IFF);
  55   addOperator(kind::IMPLIES);
  56   addOperator(kind::ITE);
  57   addOperator(kind::NOT);
  58   addOperator(kind::OR);
  59   addOperator(kind::XOR);
  60
  61 }
  62
  63 void Smt::addArithmeticOperators() {
  64   addOperator(kind::PLUS);
  65   addOperator(kind::MINUS);
  66   addOperator(kind::UMINUS);
  67   addOperator(kind::MULT);
  68   addOperator(kind::LT);
  69   addOperator(kind::LEQ);
  70   addOperator(kind::GT);
  71   addOperator(kind::GEQ);
  72 }
  73
  74 /**
  75  * Add theory symbols to the parser state.
  76  *
  77  * @param parser the CVC4 Parser object
  78  * @param theory the theory to open (e.g., Core, Ints)
  79  */
  80 void Smt::addTheory(Theory theory) {
  81   switch(theory) {
  82   case THEORY_EMPTY:
  83     mkSort("U");
  84     break;
  85
  86   case THEORY_REALS_INTS:
  87     defineType("Real", getExprManager()->realType());
  88     // falling-through on purpose, to add Ints part of RealsInts
  89
  90   case THEORY_INTS:
  91     defineType("Int", getExprManager()->integerType());
  92     addArithmeticOperators();
  93     break;
  94
  95   case THEORY_REALS:
  96     defineType("Real", getExprManager()->realType());
  97     addArithmeticOperators();
  98     break;
  99
 100   default:
 101     Unhandled(theory);
 102   }
 103 }
 104
 105 bool Smt::logicIsSet() {
 106   return d_logicSet;
 107 }
 108
 109 /**
 110  * Sets the logic for the current benchmark. Declares any logic and theory symbols.
 111  *
 112  * @param parser the CVC4 Parser object
 113  * @param name the name of the logic (e.g., QF_UF, AUFLIA)
 114  */
 115 void Smt::setLogic(const std::string& name) {
 116   d_logicSet = true;
 117   d_logic = toLogic(name);
 118
 119   switch(d_logic) {
 120   case QF_IDL:
 121   case QF_LIA:
 122   case QF_NIA:
 123     addTheory(THEORY_INTS);
 124     break;
 125
 126   case QF_LRA:
 127   case QF_RDL:
 128     addTheory(THEORY_REALS);
 129     break;
 130
 131   case QF_SAT:
 132     /* no extra symbols needed */
 133     break;
 134
 135   case QF_UFIDL:
 136     addTheory(THEORY_INTS);
 137     // falling-through on purpose, to add UF part of UFIDL
 138
 139   case QF_UF:
 140     addTheory(THEORY_EMPTY);
 141     addOperator(kind::APPLY_UF);
 142     break;
 143
 144   case AUFLIA:
 145   case AUFLIRA:
 146   case AUFNIRA:
 147   case QF_AUFBV:
 148   case QF_AUFLIA:
 149   case QF_AX:
 150   case QF_BV:
 151     Unhandled(name);
 152   }
 153 }
 154
 155 }/* CVC4::parser namespace */
 156 }/* CVC4 namespace */