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