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 "expr/command.h"
  21 #include "parser/parser.h"
  22 #include "parser/smt/smt.h"
  23 #include "parser/smt2/smt2.h"
  24
  25 namespace CVC4 {
  26 namespace parser {
  27
  28 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
  29   Parser(exprManager,input,strictMode,parseOnly),
  30   d_logicSet(false) {
  31   if( !strictModeEnabled() ) {
  32     addTheory(Smt2::THEORY_CORE);
  33   }
  34 }
  35
  36 void Smt2::addArithmeticOperators() {
  37   addOperator(kind::PLUS);
  38   addOperator(kind::MINUS);
  39   addOperator(kind::UMINUS);
  40   addOperator(kind::MULT);
  41   addOperator(kind::DIVISION);
  42   addOperator(kind::LT);
  43   addOperator(kind::LEQ);
  44   addOperator(kind::GT);
  45   addOperator(kind::GEQ);
  46 }
  47
  48 void Smt2::addTheory(Theory theory) {
  49   switch(theory) {
  50   case THEORY_CORE:
  51     defineType("Bool", getExprManager()->booleanType());
  52     defineVar("true", getExprManager()->mkConst(true));
  53     defineVar("false", getExprManager()->mkConst(false));
  54     addOperator(kind::AND);
  55     addOperator(kind::DISTINCT);
  56     addOperator(kind::EQUAL);
  57     addOperator(kind::IFF);
  58     addOperator(kind::IMPLIES);
  59     addOperator(kind::ITE);
  60     addOperator(kind::NOT);
  61     addOperator(kind::OR);
  62     addOperator(kind::XOR);
  63     break;
  64
  65   case THEORY_ARRAYS:
  66     // FIXME: should define a paramterized type 'Array' with 2 arguments
  67     mkSort("Array");
  68
  69     addOperator(kind::SELECT);
  70     addOperator(kind::STORE);
  71     break;
  72
  73   case THEORY_REALS_INTS:
  74     defineType("Real", getExprManager()->realType());
  75     // falling-through on purpose, to add Ints part of RealsInts
  76
  77   case THEORY_INTS:
  78     defineType("Int", getExprManager()->integerType());
  79     addArithmeticOperators();
  80     break;
  81
  82   case THEORY_REALS:
  83     defineType("Real", getExprManager()->realType());
  84     addArithmeticOperators();
  85     break;
  86
  87   case THEORY_BITVECTORS:
  88     break;
  89
  90   case THEORY_QUANTIFIERS:
  91     break;
  92
  93   default:
  94     Unhandled(theory);
  95   }
  96 }
  97
  98 bool Smt2::logicIsSet() {
  99   return d_logicSet;
 100 }
 101
 102 void Smt2::setLogic(const std::string& name) {
 103   d_logicSet = true;
 104   d_logic = Smt::toLogic(name);
 105
 106   // Core theory belongs to every logic
 107   addTheory(THEORY_CORE);
 108
 109   switch(d_logic) {
 110   case Smt::QF_SAT:
 111     /* No extra symbols necessary */
 112     break;
 113
 114   case Smt::QF_AX:
 115     addTheory(THEORY_ARRAYS);
 116     break;
 117
 118   case Smt::QF_IDL:
 119   case Smt::QF_LIA:
 120   case Smt::QF_NIA:
 121     addTheory(THEORY_INTS);
 122     break;
 123
 124   case Smt::QF_RDL:
 125   case Smt::QF_LRA:
 126   case Smt::QF_NRA:
 127     addTheory(THEORY_REALS);
 128     break;
 129
 130   case Smt::QF_UF:
 131     addOperator(kind::APPLY_UF);
 132     break;
 133
 134   case Smt::QF_UFIDL:
 135   case Smt::QF_UFLIA:
 136   case Smt::QF_UFNIA:// nonstandard logic
 137     addTheory(THEORY_INTS);
 138     addOperator(kind::APPLY_UF);
 139     break;
 140
 141   case Smt::QF_UFLRA:
 142   case Smt::QF_UFNRA:
 143     addTheory(THEORY_REALS);
 144     addOperator(kind::APPLY_UF);
 145     break;
 146
 147   case Smt::QF_UFLIRA:// nonstandard logic
 148   case Smt::QF_UFNIRA:// nonstandard logic
 149     addOperator(kind::APPLY_UF);
 150     addTheory(THEORY_INTS);
 151     addTheory(THEORY_REALS);
 152     break;
 153
 154   case Smt::QF_BV:
 155     addTheory(THEORY_BITVECTORS);
 156     break;
 157
 158   case Smt::QF_ABV:
 159     addTheory(THEORY_ARRAYS);
 160     addTheory(THEORY_BITVECTORS);
 161     break;
 162
 163   case Smt::QF_UFBV:
 164     addOperator(kind::APPLY_UF);
 165     addTheory(THEORY_BITVECTORS);
 166     break;
 167
 168   case Smt::QF_AUFBV:
 169     addOperator(kind::APPLY_UF);
 170     addTheory(THEORY_ARRAYS);
 171     addTheory(THEORY_BITVECTORS);
 172     break;
 173
 174   case Smt::QF_AUFBVLIA:
 175     addOperator(kind::APPLY_UF);
 176     addTheory(THEORY_ARRAYS);
 177     addTheory(THEORY_BITVECTORS);
 178     addTheory(THEORY_INTS);
 179     break;
 180
 181   case Smt::QF_AUFBVLRA:
 182     addOperator(kind::APPLY_UF);
 183     addTheory(THEORY_ARRAYS);
 184     addTheory(THEORY_BITVECTORS);
 185     addTheory(THEORY_REALS);
 186     break;
 187
 188   case Smt::QF_AUFLIA:
 189     addTheory(THEORY_ARRAYS);
 190     addOperator(kind::APPLY_UF);
 191     addTheory(THEORY_INTS);
 192     break;
 193
 194   case Smt::QF_AUFLIRA:
 195     addTheory(THEORY_ARRAYS);
 196     addOperator(kind::APPLY_UF);
 197     addTheory(THEORY_INTS);
 198     addTheory(THEORY_REALS);
 199     break;
 200
 201   case Smt::ALL_SUPPORTED:
 202     addTheory(THEORY_QUANTIFIERS);
 203     /* fall through */
 204   case Smt::QF_ALL_SUPPORTED:
 205     addTheory(THEORY_ARRAYS);
 206     addOperator(kind::APPLY_UF);
 207     addTheory(THEORY_INTS);
 208     addTheory(THEORY_REALS);
 209     addTheory(THEORY_BITVECTORS);
 210     break;
 211
 212   case Smt::AUFLIA:
 213   case Smt::AUFLIRA:
 214   case Smt::AUFNIRA:
 215   case Smt::LRA:
 216   case Smt::UFNIA:
 217   case Smt::UFNIRA:
 218   case Smt::UFLRA:
 219     if(d_logic != Smt::AUFLIA && d_logic != Smt::UFNIA) {
 220       addTheory(THEORY_REALS);
 221     }
 222     if(d_logic != Smt::LRA) {
 223       addOperator(kind::APPLY_UF);
 224       if(d_logic != Smt::UFLRA) {
 225         addTheory(THEORY_INTS);
 226         if(d_logic != Smt::UFNIA && d_logic != Smt::UFNIRA) {
 227           addTheory(THEORY_ARRAYS);
 228         }
 229       }
 230     }
 231     addTheory(THEORY_QUANTIFIERS);
 232     break;
 233   }
 234 }/* Smt2::setLogic() */
 235
 236 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
 237   // TODO: ???
 238 }
 239
 240 void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 241   // TODO: ???
 242 }
 243
 244 void Smt2::checkThatLogicIsSet() {
 245   if( ! logicIsSet() ) {
 246     if( strictModeEnabled() ) {
 247       parseError("set-logic must appear before this point.");
 248     } else {
 249       warning("No set-logic command was given before this point.");
 250       warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
 251       warning("Consider setting a stricter logic for (likely) better performance.");
 252       warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 253
 254       setLogic("ALL_SUPPORTED");
 255
 256       preemptCommand(new SetBenchmarkLogicCommand("ALL_SUPPORTED"));
 257     }
 258   }
 259 }
 260
 261 }/* CVC4::parser namespace */
 262 }/* CVC4 namespace */