src/parser/smt2/smt2.cpp

   1 /*********************                                                        */
   2 /*! \file smt2.cpp
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): none
   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  ** \brief Definitions of SMT2 constants.
  15  **
  16  ** Definitions of SMT2 constants.
  17  **/
  18
  19 #include "expr/type.h"
  20 #include "parser/parser.h"
  21 #include "parser/smt/smt.h"
  22 #include "parser/smt2/smt2.h"
  23
  24 namespace CVC4 {
  25 namespace parser {
  26
  27 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
  28   Parser(exprManager,input,strictMode,parseOnly),
  29   d_logicSet(false) {
  30   if( !strictModeEnabled() ) {
  31     addTheory(Smt2::THEORY_CORE);
  32   }
  33 }
  34
  35 void Smt2::addArithmeticOperators() {
  36   addOperator(kind::PLUS);
  37   addOperator(kind::MINUS);
  38   addOperator(kind::UMINUS);
  39   addOperator(kind::MULT);
  40   addOperator(kind::DIVISION);
  41   addOperator(kind::LT);
  42   addOperator(kind::LEQ);
  43   addOperator(kind::GT);
  44   addOperator(kind::GEQ);
  45 }
  46
  47 void Smt2::addTheory(Theory theory) {
  48   switch(theory) {
  49   case THEORY_CORE:
  50     defineType("Bool", getExprManager()->booleanType());
  51     defineVar("true", getExprManager()->mkConst(true));
  52     defineVar("false", getExprManager()->mkConst(false));
  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     break;
  62
  63   case THEORY_ARRAYS:
  64     // FIXME: should define a paramterized type 'Array' with 2 arguments
  65     mkSort("Array");
  66
  67     addOperator(kind::SELECT);
  68     addOperator(kind::STORE);
  69     break;
  70
  71   case THEORY_REALS_INTS:
  72     defineType("Real", getExprManager()->realType());
  73     // falling-through on purpose, to add Ints part of RealsInts
  74
  75   case THEORY_INTS:
  76     defineType("Int", getExprManager()->integerType());
  77     addArithmeticOperators();
  78     break;
  79
  80   case THEORY_REALS:
  81     defineType("Real", getExprManager()->realType());
  82     addArithmeticOperators();
  83     break;
  84
  85   case THEORY_BITVECTORS:
  86     break;
  87
  88   default:
  89     Unhandled(theory);
  90   }
  91 }
  92
  93 bool Smt2::logicIsSet() {
  94   return d_logicSet;
  95 }
  96
  97 void Smt2::setLogic(const std::string& name) {
  98   d_logicSet = true;
  99   d_logic = Smt::toLogic(name);
 100
 101   // Core theory belongs to every logic
 102   addTheory(THEORY_CORE);
 103
 104   switch(d_logic) {
 105   case Smt::QF_SAT:
 106     /* No extra symbols necessary */
 107     break;
 108
 109   case Smt::QF_AX:
 110     addTheory(THEORY_ARRAYS);
 111     break;
 112
 113   case Smt::QF_IDL:
 114   case Smt::QF_LIA:
 115   case Smt::QF_NIA:
 116     addTheory(THEORY_INTS);
 117     break;
 118
 119   case Smt::QF_RDL:
 120   case Smt::QF_LRA:
 121   case Smt::QF_NRA:
 122     addTheory(THEORY_REALS);
 123     break;
 124
 125   case Smt::QF_UF:
 126     addOperator(kind::APPLY_UF);
 127     break;
 128
 129   case Smt::QF_UFIDL:
 130   case Smt::QF_UFLIA:
 131   case Smt::QF_UFNIA:// nonstandard logic
 132     addTheory(THEORY_INTS);
 133     addOperator(kind::APPLY_UF);
 134     break;
 135
 136   case Smt::QF_UFLRA:
 137   case Smt::QF_UFNRA:
 138     addTheory(THEORY_REALS);
 139     addOperator(kind::APPLY_UF);
 140     break;
 141
 142   case Smt::QF_UFLIRA:// nonstandard logic
 143   case Smt::QF_UFNIRA:// nonstandard logic
 144     addOperator(kind::APPLY_UF);
 145     addTheory(THEORY_INTS);
 146     addTheory(THEORY_REALS);
 147     break;
 148
 149   case Smt::QF_BV:
 150     addTheory(THEORY_BITVECTORS);
 151     break;
 152
 153   case Smt::QF_ABV:
 154     addTheory(THEORY_ARRAYS);
 155     addTheory(THEORY_BITVECTORS);
 156     break;
 157
 158   case Smt::QF_UFBV:
 159     addOperator(kind::APPLY_UF);
 160     addTheory(THEORY_BITVECTORS);
 161     break;
 162
 163   case Smt::QF_AUFBV:
 164     addOperator(kind::APPLY_UF);
 165     addTheory(THEORY_ARRAYS);
 166     addTheory(THEORY_BITVECTORS);
 167     break;
 168
 169   case Smt::QF_AUFLIA:
 170     addTheory(THEORY_ARRAYS);
 171     addOperator(kind::APPLY_UF);
 172     addTheory(THEORY_INTS);
 173     break;
 174
 175   case Smt::QF_AUFLIRA:
 176     addTheory(THEORY_ARRAYS);
 177     addOperator(kind::APPLY_UF);
 178     addTheory(THEORY_INTS);
 179     addTheory(THEORY_REALS);
 180     break;
 181
 182   case Smt::AUFLIA:
 183   case Smt::AUFLIRA:
 184   case Smt::AUFNIRA:
 185   case Smt::LRA:
 186   case Smt::UFLRA:
 187   case Smt::UFNIA:
 188     Unhandled(name);
 189   }
 190 }
 191
 192 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 193   // TODO: ???
 194 }
 195
 196 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 197   // TODO: ???
 198 }
 199
 200 }/* CVC4::parser namespace */
 201 }/* CVC4 namespace */